-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (goal)
Goal:
K : Type u_2
L : Type u_3
B : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : CommRing B
P : Ideal B
D : Type u_5
inst_4 : Field D
inst_5 : Algebra D L
inst_6 : MulSemiringAction.{u_3, u_4} Gal(L/K) B
G : Type u_7
inst_7 : Group G
inst_8 : Finite G
inst_9 : MulSemiringAction G L
inst_10 : IsGaloisGroup G K L
inst_11 : MulSemiringAction G B
inst_12 : Algebra B L
inst_13 : IsFractionRing B L
inst_14 : SMulDistribClass Gal(L/K) B L
inst_15 : SMulDistribClass G B L
h : IsGaloisGroup.{u_7, u_5, u_3} (↥(stabilizer G P)) D L
x : ↥(stabilizer Gal(L/K) P)
y z : B
left : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) z
refine_2 :
  HSMul.hSMul.{u_7, u_3, u_3} (α := ↥(stabilizer G P)) (β := L)
        (((MulEquiv.symm (P.stabilizerEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯) :
                MulEquiv.{u_3, u_7} ↥(stabilizer Gal(L/K) P) ↥(stabilizer G P)) :
              (a : ↥(stabilizer Gal(L/K) P)) → ↥(stabilizer G P))
            x :
          ↥(stabilizer G P))
        ((algebraMap B L : (a : B) → L) y : L) /
      HSMul.hSMul.{u_7, u_3, u_3} (α := ↥(stabilizer G P)) (β := L)
        (((MulEquiv.symm (P.stabilizerEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯) :
                MulEquiv.{u_3, u_7} ↥(stabilizer Gal(L/K) P) ↥(stabilizer G P)) :
              (a : ↥(stabilizer Gal(L/K) P)) → ↥(stabilizer G P))
            x :
          ↥(stabilizer G P))
        ((algebraMap B L : (a : B) → L) z : L) =
    HSMul.hSMul (β := L) x ((algebraMap B L : (a : B) → L) y : L) /
      HSMul.hSMul (β := L) x ((algebraMap B L : (a : B) → L) z : L)
⊢ HSMul.hSMul.{u_7, u_3, u_3} (α := ↥(stabilizer G P))
      (((MulEquiv.symm (P.stabilizerEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯) :
              MulEquiv.{u_3, u_7} ↥(stabilizer Gal(L/K) P) ↥(stabilizer G P)) :
            (a : ↥(stabilizer Gal(L/K) P)) → ↥(stabilizer G P))
          x :
        ↥(stabilizer G P))
      (HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) y : L) ((algebraMap B L : (a : B) → L) z : L)) =
    x • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) y : L) ((algebraMap B L : (a : B) → L) z : L)
have refine_2₁ : HSMul.hSMul.{u_7, u_3, u_3} (α := G) (β := L)
      (↑(((MulEquiv.symm (P.stabilizerEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) sorry) :
                MulEquiv.{u_3, u_7} ↥(stabilizer Gal(L/K) P) ↥(stabilizer G P)) :
              (a : ↥(stabilizer Gal(L/K) P)) → ↥(stabilizer G P))
            x) :
        G)
      ((algebraMap B L : (a : B) → L) y : L) /
    HSMul.hSMul.{u_7, u_3, u_3} (α := G) (β := L)
      (↑(((MulEquiv.symm (P.stabilizerEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) sorry) :
                MulEquiv.{u_3, u_7} ↥(stabilizer Gal(L/K) P) ↥(stabilizer G P)) :
              (a : ↥(stabilizer Gal(L/K) P)) → ↥(stabilizer G P))
            x) :
        G)
      ((algebraMap B L : (a : B) → L) z : L) =
  HSMul.hSMul (β := L) (↑x : Gal(L/K)) ((algebraMap B L : (a : B) → L) y : L) /
    HSMul.hSMul (β := L) (↑x : Gal(L/K)) ((algebraMap B L : (a : B) → L) z : L)
Tactic: simp_rw [smul_div₀', subgroup_smul_def, ← algebraMap.smul', ← subgroup_smul_def,
      stabilizerEquiv_symm_apply_smul]