-- Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory
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
E : Type u_6
inst_4 : Field E
inst_5 : Algebra E 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_6, u_3} (↥(inertia G P)) E L
x : ↥(inertia 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} (α := ↥(inertia G P)) (β := L)
        (((MulEquiv.symm (P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯) :
                MulEquiv.{u_3, u_7} ↥(inertia Gal(L/K) P) ↥(inertia G P)) :
              (a : ↥(inertia Gal(L/K) P)) → ↥(inertia G P))
            x :
          ↥(inertia G P))
        ((algebraMap B L : (a : B) → L) y : L) /
      HSMul.hSMul.{u_7, u_3, u_3} (α := ↥(inertia G P)) (β := L)
        (((MulEquiv.symm (P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯) :
                MulEquiv.{u_3, u_7} ↥(inertia Gal(L/K) P) ↥(inertia G P)) :
              (a : ↥(inertia Gal(L/K) P)) → ↥(inertia G P))
            x :
          ↥(inertia 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)
refine_2₁ :
  HSMul.hSMul.{u_7, u_3, u_3} (α := G) (β := L)
        (↑(((MulEquiv.symm (P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯) :
                  MulEquiv.{u_3, u_7} ↥(inertia Gal(L/K) P) ↥(inertia G P)) :
                (a : ↥(inertia Gal(L/K) P)) → ↥(inertia 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.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯) :
                  MulEquiv.{u_3, u_7} ↥(inertia Gal(L/K) P) ↥(inertia G P)) :
                (a : ↥(inertia Gal(L/K) P)) → ↥(inertia 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)
refine_2₂ :
  HDiv.hDiv (α := L) (β := L)
      ((algebraMap B L : (a : B) → L)
          (HSMul.hSMul.{u_7, u_4, u_4} (α := G)
            (↑(((MulEquiv.symm (P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯) :
                      MulEquiv.{u_3, u_7} ↥(inertia Gal(L/K) P) ↥(inertia G P)) :
                    (a : ↥(inertia Gal(L/K) P)) → ↥(inertia G P))
                  x) :
              G)
            y) :
        L)
      ((algebraMap B L : (a : B) → L)
          (HSMul.hSMul.{u_7, u_4, u_4} (α := G)
            (↑(((MulEquiv.symm (P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯) :
                      MulEquiv.{u_3, u_7} ↥(inertia Gal(L/K) P) ↥(inertia G P)) :
                    (a : ↥(inertia Gal(L/K) P)) → ↥(inertia G P))
                  x) :
              G)
            z) :
        L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) ((↑x : Gal(L/K)) • y) : L)
      ((algebraMap B L : (a : B) → L) ((↑x : Gal(L/K)) • z) : L)
refine_2₃ :
  HDiv.hDiv (α := L) (β := L)
      ((algebraMap B L : (a : B) → L)
          (HSMul.hSMul.{u_7, u_4, u_4} (α := ↥(inertia G P))
            (((MulEquiv.symm (P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯) :
                    MulEquiv.{u_3, u_7} ↥(inertia Gal(L/K) P) ↥(inertia G P)) :
                  (a : ↥(inertia Gal(L/K) P)) → ↥(inertia G P))
                x :
              ↥(inertia G P))
            y) :
        L)
      ((algebraMap B L : (a : B) → L)
          (HSMul.hSMul.{u_7, u_4, u_4} (α := ↥(inertia G P))
            (((MulEquiv.symm (P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯) :
                    MulEquiv.{u_3, u_7} ↥(inertia Gal(L/K) P) ↥(inertia G P)) :
                  (a : ↥(inertia Gal(L/K) P)) → ↥(inertia G P))
                x :
              ↥(inertia G P))
            z) :
        L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) (x • y) : L)
      ((algebraMap B L : (a : B) → L) (x • z) : L)
⊢ HSMul.hSMul.{u_7, u_3, u_3} (α := ↥(inertia G P))
      (((MulEquiv.symm (P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯) :
              MulEquiv.{u_3, u_7} ↥(inertia Gal(L/K) P) ↥(inertia G P)) :
            (a : ↥(inertia Gal(L/K) P)) → ↥(inertia G P))
          x :
        ↥(inertia 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)

Tactic:
simp_rw [smul_div₀', subgroup_smul_def, ← algebraMap.smul', ← subgroup_smul_def,
      inertiaEquiv_symm_apply_smul]

Premises used: Ideal.inertiaEquiv_symm_apply_smul, smul_div₀', algebraMap.smul', MulAction.subgroup_smul_def