awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R S L
inst_11 : IsScalarTower R K L
inst_12 : IsIntegralClosure S R L
inst_13 : FiniteDimensional K L
inst_14 : IsDedekindDomain R
inst_15 : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₁
hP₂ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₂
this_1 : IsDomain S
this_2 : IsDedekindDomain S
this_3 : Module.Finite R S
this_4 : P₁.IsPrime
this_5 : P₁.LiesOver p
this : P₂.IsPrime
⊢ ∃ (σ : Gal(L/K)),
    comap (F := S ≃ₐ[R] S)
        (((galRestrict R K L S : MulEquiv.{u_3, u_4} Gal(L/K) (S ≃ₐ[R] S)) : (a : Gal(L/K)) → S ≃ₐ[R] S) σ : S ≃ₐ[R] S)
        P₁ =
      P₂
have this₁ : P₂.LiesOver p
Tactic: have := hP₂.2
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R S L
inst_11 : IsScalarTower R K L
inst_12 : IsIntegralClosure S R L
inst_13 : FiniteDimensional K L
inst_14 : IsDedekindDomain R
inst_15 : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₁
hP₂ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₂
this_1 : IsDomain S
this_2 : IsDedekindDomain S
this_3 : Module.Finite R S
this_4 : P₁.IsPrime
this_5 : P₁.LiesOver p
this_6 : P₂.IsPrime
this : P₂.LiesOver p
⊢ ∃ (σ : Gal(L/K)),
    comap (F := S ≃ₐ[R] S)
        (((galRestrict R K L S : MulEquiv.{u_3, u_4} Gal(L/K) (S ≃ₐ[R] S)) : (a : Gal(L/K)) → S ≃ₐ[R] S) σ : S ≃ₐ[R] S)
        P₁ =
      P₂
have this₁ : IsFractionRing S L
Tactic: have : IsFractionRing S L := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (hypothesis)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R S L
inst_11 : IsScalarTower R K L
inst_12 : IsIntegralClosure S R L
inst_13 : FiniteDimensional K L
inst_14 : IsDedekindDomain R
inst_15 : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₁
hP₂ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₂
this_1 : IsDomain S
this_2 : IsDedekindDomain S
this_3 : Module.Finite R S
this_4 : P₁.IsPrime
this_5 : P₁.LiesOver p
this_6 : P₂.IsPrime
this_7 : P₂.LiesOver p
this_8 : IsFractionRing S L
this : MulSemiringAction.{u_3, u_4} Gal(L/K) S := IsIntegralClosure.MulSemiringAction R K L S
⊢ ∃ (σ : Gal(L/K)),
    comap (F := S ≃ₐ[R] S)
        (((galRestrict R K L S : MulEquiv.{u_3, u_4} Gal(L/K) (S ≃ₐ[R] S)) : (a : Gal(L/K)) → S ≃ₐ[R] S) σ : S ≃ₐ[R] S)
        P₁ =
      P₂
have this₁ : IsGaloisGroup.{u_3, u_1, u_4} Gal(L/K) R S
Tactic: have : IsGaloisGroup Gal(L/K) R S := IsGaloisGroup.of_isFractionRing _ _ _ K L
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Galois (goal)
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : Algebra R L
inst_10 : IsScalarTower R S L
inst_11 : IsScalarTower R K L
inst_12 : IsIntegralClosure S R L
inst_13 : FiniteDimensional K L
inst_14 : IsDedekindDomain R
inst_15 : IsGalois K L
p : Ideal R
P₁ P₂ : Ideal S
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₁
hP₂ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) P₂
this_1 : IsDomain S
this_2 : IsDedekindDomain S
this_3 : Module.Finite R S
this_4 : P₁.IsPrime
this_5 : P₁.LiesOver p
this_6 : P₂.IsPrime
this_7 : P₂.LiesOver p
this_8 : IsFractionRing S L
this_9 : MulSemiringAction.{u_3, u_4} Gal(L/K) S := IsIntegralClosure.MulSemiringAction R K L S
this : IsGaloisGroup.{u_3, u_1, u_4} Gal(L/K) R S
⊢ ∃ (σ : Gal(L/K)),
    comap (F := S ≃ₐ[R] S)
        (((galRestrict R K L S : MulEquiv.{u_3, u_4} Gal(L/K) (S ≃ₐ[R] S)) : (a : Gal(L/K)) → S ≃ₐ[R] S) σ : S ≃ₐ[R] S)
        P₁ =
      P₂
have obtain : ∀ (σ : Gal(L/K)) (hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) (σ • P₂)) (this : (σ • P₂).IsPrime)
  (this : (σ • P₂).LiesOver p),
  ∃ (σ_1 : Gal(L/K)),
    comap (F := S ≃ₐ[R] S)
        (((galRestrict R K L S : MulEquiv.{u_3, u_4} Gal(L/K) (S ≃ₐ[R] S)) : (a : Gal(L/K)) → S ≃ₐ[R] S) σ_1 :
          S ≃ₐ[R] S)
        (σ • P₂) =
      P₂
Tactic: obtain ⟨σ, rfl⟩ := exists_smul_eq_of_isGaloisGroup p P₂ P₁ Gal(L/K)
Cleared hypotheses: P₁, hP₁, this_4, this_5
-- 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
⊢ IsDecompositionField K L P D
have refine_1 : MulEquiv.{u_3, u_7} ↥(stabilizer Gal(L/K) P) ↥(stabilizer G P)
Tactic: refine (isDecompositionField_iff K L P D).mpr <| .of_mulEquiv (hG := h) ?_ fun _ x ↦ ?_
-- 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
refine_1 : MulEquiv.{u_3, u_7} ↥(stabilizer Gal(L/K) P) ↥(stabilizer G P)
⊢ IsDecompositionField K L P D
have refine_2 : ∀ (x : ↥(stabilizer Gal(L/K) P)) (x_1 : L),
  HSMul.hSMul.{u_7, u_3, u_3} (α := ↥(stabilizer G P))
      (((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 :
        ↥(stabilizer G P))
      x_1 =
    x • x_1
Tactic: refine (isDecompositionField_iff K L P D).mpr <| .of_mulEquiv (hG := h) ?_ fun _ x ↦ ?_
-- 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
⊢ MulEquiv.{u_3, u_7} ↥(stabilizer Gal(L/K) P) ↥(stabilizer G P)
have refine_1 : ∀ (x : G) (x_1 : B),
  HSMul.hSMul.{u_3, u_4, u_4} (α := Gal(L/K))
      (((IsGaloisGroup.mulEquivAlgEquiv G K L : MulEquiv.{u_7, u_3} G Gal(L/K)) : (a : G) → Gal(L/K)) x : Gal(L/K))
      x_1 =
    x • x_1
Tactic: refine (stabilizerEquiv _ (IsGaloisGroup.mulEquivAlgEquiv G K L) fun _ _ ↦ ?_).symm
-- 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 : G
x_1 : B
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := Gal(L/K))
      (((IsGaloisGroup.mulEquivAlgEquiv G K L : MulEquiv.{u_7, u_3} G Gal(L/K)) : (a : G) → Gal(L/K)) x : Gal(L/K))
      x_1 =
    x • x_1
have refine_1 : Eq.{u_3 + 1} (α := L)
  ((algebraMap B L : (a : B) → L)
      (HSMul.hSMul.{u_3, u_4, u_4} (α := Gal(L/K))
        (((IsGaloisGroup.mulEquivAlgEquiv G K L : MulEquiv.{u_7, u_3} G Gal(L/K)) : (a : G) → Gal(L/K)) x : Gal(L/K))
        x_1) :
    L)
  ((algebraMap B L : (a : B) → L) (x • x_1) : L)
Tactic: apply FaithfulSMul.algebraMap_injective B L
-- 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_1 : ↥(stabilizer Gal(L/K) P)
x : 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_1 :
        ↥(stabilizer G P))
      x =
    x_1 • x
have refine_2 : ∀ (y z : B),
  Membership.mem (γ := Submonoid B) (nonZeroDivisors B) z →
    HSMul.hSMul.{u_7, u_3, u_3} (α := ↥(stabilizer G P))
        (((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_1 :
          ↥(stabilizer G P))
        (HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) y : L) ((algebraMap B L : (a : B) → L) z : L)) =
      x_1 • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) y : L) ((algebraMap B L : (a : B) → L) z : L)
Tactic: obtain ⟨y, z, _, rfl⟩ := IsFractionRing.div_surjective B x
Cleared hypotheses: x
-- 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
⊢ 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} (α := ↥(stabilizer G P)) (β := 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 :
        ↥(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) sorry) :
              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)
Tactic: simp_rw [smul_div₀', subgroup_smul_def, ← algebraMap.smul', ← subgroup_smul_def,
      stabilizerEquiv_symm_apply_smul]
-- 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
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
⊢ IsInertiaField K L P E
have refine_1 : MulEquiv.{u_3, u_7} ↥(inertia Gal(L/K) P) ↥(inertia G P)
Tactic: refine (isInertiaField_iff K L P E).mpr <| .of_mulEquiv (hG := h) ?_ fun _ x ↦ ?_
-- 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
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
refine_1 : MulEquiv.{u_3, u_7} ↥(inertia Gal(L/K) P) ↥(inertia G P)
⊢ IsInertiaField K L P E
have refine_2 : ∀ (x : ↥(inertia Gal(L/K) P)) (x_1 : L),
  HSMul.hSMul.{u_7, u_3, u_3} (α := ↥(inertia G P))
      (((MulEquiv.symm (P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) sorry) :
              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))
      x_1 =
    x • x_1
Tactic: refine (isInertiaField_iff K L P E).mpr <| .of_mulEquiv (hG := h) ?_ fun _ x ↦ ?_
-- 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
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
⊢ MulEquiv.{u_3, u_7} ↥(inertia Gal(L/K) P) ↥(inertia G P)
have refine_1 : ∀ (x : G) (x_1 : B),
  HSMul.hSMul.{u_3, u_4, u_4} (α := Gal(L/K))
      (((IsGaloisGroup.mulEquivAlgEquiv G K L : MulEquiv.{u_7, u_3} G Gal(L/K)) : (a : G) → Gal(L/K)) x : Gal(L/K))
      x_1 =
    x • x_1
Tactic: refine (inertiaEquiv _ (IsGaloisGroup.mulEquivAlgEquiv G K L) fun _ _ ↦ ?_).symm
-- 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
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 : G
x_1 : B
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := Gal(L/K))
      (((IsGaloisGroup.mulEquivAlgEquiv G K L : MulEquiv.{u_7, u_3} G Gal(L/K)) : (a : G) → Gal(L/K)) x : Gal(L/K))
      x_1 =
    x • x_1
have refine_1 : Eq.{u_3 + 1} (α := L)
  ((algebraMap B L : (a : B) → L)
      (HSMul.hSMul.{u_3, u_4, u_4} (α := Gal(L/K))
        (((IsGaloisGroup.mulEquivAlgEquiv G K L : MulEquiv.{u_7, u_3} G Gal(L/K)) : (a : G) → Gal(L/K)) x : Gal(L/K))
        x_1) :
    L)
  ((algebraMap B L : (a : B) → L) (x • x_1) : L)
Tactic: apply FaithfulSMul.algebraMap_injective B L
-- 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
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_1 : ↥(inertia Gal(L/K) P)
x : 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_1 :
        ↥(inertia G P))
      x =
    x_1 • x
have refine_2 : ∀ (y z : B),
  Membership.mem (γ := Submonoid B) (nonZeroDivisors B) z →
    HSMul.hSMul.{u_7, u_3, u_3} (α := ↥(inertia G P))
        (((MulEquiv.symm (P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) sorry) :
                MulEquiv.{u_3, u_7} ↥(inertia Gal(L/K) P) ↥(inertia G P)) :
              (a : ↥(inertia Gal(L/K) P)) → ↥(inertia G P))
            x_1 :
          ↥(inertia G P))
        (HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) y : L) ((algebraMap B L : (a : B) → L) z : L)) =
      x_1 • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) y : L) ((algebraMap B L : (a : B) → L) z : L)
Tactic: obtain ⟨y, z, _, rfl⟩ := IsFractionRing.div_surjective B x
Cleared hypotheses: x
-- 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
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
⊢ 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)
have refine_2 : HSMul.hSMul.{u_7, u_3, u_3} (α := ↥(inertia G P)) (β := L)
      (((MulEquiv.symm (P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) sorry) :
              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) sorry) :
              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)
Tactic: simp_rw [smul_div₀', subgroup_smul_def, ← algebraMap.smul', ← subgroup_smul_def,
      inertiaEquiv_symm_apply_smul]