Commonize proof by macro or somehow

Stream: lean4

[SnO2WMaN]

Currently I'm working on formalizing modal logic, and refactoring my proof.

I have the following proof (↓), but these proof have almost exactly the same structure.
So I want to commonize these proofs by using macros or such means (If I were to implement all logics in normal modal logic cube, I would have to write about 10 more proofs exactly like these), but I don't know how to do because I'm not familiar with Lean4 metaprogramming. How can I do?

abbrev LogicK.CanonicalModel {β} := Normal.CanonicalModel (𝐊 : AxiomSet β)
theorem LogicK.Hilbert.completes : Completeness (𝐊 : AxiomSet β) (𝔽((𝐊 : AxiomSet β)) : FrameClass (MaximalConsistentTheory (𝐊 : AxiomSet β))) := by
  apply completeness_def.mpr;
  intro Γ hConsisΓ;
  let ⟨Ω, hΩ⟩ := exists_maximal_consistent_theory hConsisΓ;
  existsi CanonicalModel.frame;
  constructor;
  . apply FrameClassDefinability.mp; simp_all;
  . existsi CanonicalModel.val, Ω;
    apply truthlemma' (by simp) |>.mpr;
    assumption;

abbrev LogicS4.CanonicalModel {β} := Normal.CanonicalModel (𝐒𝟒 : AxiomSet β)
theorem LogicS4.Hilbert.completes : Completeness (𝐒𝟒 : AxiomSet β) (𝔽((𝐒𝟒 : AxiomSet β)) : FrameClass (MaximalConsistentTheory (𝐒𝟒 : AxiomSet β))) := by
  apply completeness_def.mpr;
  intro Γ hConsisΓ;
  let ⟨Ω, hΩ⟩ := exists_maximal_consistent_theory hConsisΓ;
  existsi CanonicalModel.frame;
  constructor;
  . apply FrameClassDefinability.mp; simp_all;
  . existsi CanonicalModel.val, Ω;
    apply truthlemma' (by simp) |>.mpr;
    assumption;

https://github.com/SnO2WMaN/lean4-logic/blob/943ecf84381b3445b0d6f6ee8a1d7cdb7c9e72dc/Logic/Modal/Normal/Completeness.lean#L509-L543