awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Galois
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₂ : Ideal S
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 : IsFractionRing S L
this_7 : MulSemiringAction.{u_3, u_4} Gal(L/K) S := IsIntegralClosure.MulSemiringAction R K L S
this_8 : IsGaloisGroup.{u_3, u_1, u_4} Gal(L/K) R S
σ : Gal(L/K)
hP₁ : Membership.mem (γ := Set (Ideal S)) (p.primesOver S) (σ • P₂)
this_9 : (σ • 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:
exact ⟨σ, comap_map_of_bijective _ ((galRestrict R K L S σ).bijective)⟩
-- Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory
Goal:
A : Type u_1
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 A
inst_4 : CommRing B
inst_5 : Algebra A B
p : Ideal A
P : Ideal B
inst_6 : P.LiesOver p
D : Type u_5
inst_7 : Field D
inst_8 : Algebra D L
inst_9 : MulSemiringAction.{u_3, u_4} Gal(L/K) B
h : IsGaloisGroup (↥(stabilizer Gal(L/K) P)) D L
⊢ IsDecompositionField K L P D

Tactic:
{ toIsGaloisGroup := h }

Premises used: IsDecompositionField.mk
-- Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory
Goal:
A : Type u_1
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 A
inst_4 : CommRing B
inst_5 : Algebra A B
p : Ideal A
P : Ideal B
inst_6 : P.LiesOver p
D : Type u_5
inst_7 : Field D
inst_8 : Algebra D L
E : Type u_6
inst_9 : Field E
inst_10 : Algebra E L
inst_11 : MulSemiringAction.{u_3, u_4} Gal(L/K) B
h : IsGaloisGroup (↥(inertia Gal(L/K) P)) E L
⊢ IsInertiaField K L P E

Tactic:
{ toIsGaloisGroup := h }

Premises used: IsInertiaField.mk
-- 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
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

Tactic:
(isDecompositionField_iff K L P D).mpr <| .of_mulEquiv (hG := h) ?_ fun _ x ↦ ?_

Premises used: Iff.mpr, IsGaloisGroup.of_mulEquiv, isDecompositionField_iff
-- 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
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)
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) ⋯) :
                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
⊢ IsDecompositionField K L P D

Tactic:
refine (isDecompositionField_iff K L P D).mpr <| .of_mulEquiv (hG := h) ?_ fun _ x ↦ ?_

Premises used: Iff.mpr, isDecompositionField_iff
-- 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
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 :
  ∀ (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
⊢ MulEquiv.{u_3, u_7} ↥(stabilizer Gal(L/K) P) ↥(stabilizer G P)

Tactic:
refine (stabilizerEquiv _ (IsGaloisGroup.mulEquivAlgEquiv G K L) fun _ _ ↦ ?_).symm

Premises used: IsGaloisGroup.mulEquivAlgEquiv, MulEquiv.symm, Ideal.stabilizerEquiv
-- 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
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
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)
⊢ 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:
apply FaithfulSMul.algebraMap_injective B L

Premises used: FaithfulSMul.algebraMap_injective
-- 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
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
⊢ 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:
simp [algebraMap.smul']

Premises used: algebraMap.smul'
-- 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
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
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) ⋯) :
                  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)
⊢ 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

Tactic:
obtain ⟨y, z, _, rfl⟩ := IsFractionRing.div_surjective B x

Premises used: IsFractionRing.div_surjective, rfl
-- 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
⊢ IsInertiaField K L P E

Tactic:
(isInertiaField_iff K L P E).mpr <| .of_mulEquiv (hG := h) ?_ fun _ x ↦ ?_

Premises used: Iff.mpr, IsGaloisGroup.of_mulEquiv, isInertiaField_iff
-- 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
refine_1 : MulEquiv.{u_3, u_7} ↥(inertia Gal(L/K) P) ↥(inertia G P)
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) ⋯) :
                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
⊢ IsInertiaField K L P E

Tactic:
refine (isInertiaField_iff K L P E).mpr <| .of_mulEquiv (hG := h) ?_ fun _ x ↦ ?_

Premises used: Iff.mpr, isInertiaField_iff
-- 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
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
⊢ MulEquiv.{u_3, u_7} ↥(inertia Gal(L/K) P) ↥(inertia G P)

Tactic:
refine (inertiaEquiv _ (IsGaloisGroup.mulEquivAlgEquiv G K L) fun _ _ ↦ ?_).symm

Premises used: IsGaloisGroup.mulEquivAlgEquiv, MulEquiv.symm, Ideal.inertiaEquiv
-- 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 : G
x_1 : B
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)
⊢ 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:
apply FaithfulSMul.algebraMap_injective B L

Premises used: FaithfulSMul.algebraMap_injective
-- 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 : G
x_1 : B
⊢ 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:
simp [algebraMap.smul']

Premises used: algebraMap.smul'
-- 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_1 : ↥(inertia Gal(L/K) P)
x : L
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) ⋯) :
                  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)
⊢ 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

Tactic:
obtain ⟨y, z, _, rfl⟩ := IsFractionRing.div_surjective B x

Premises used: IsFractionRing.div_surjective, rfl
-- 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
D : Type u_5
inst_4 : Field D
inst_5 : Algebra D L
inst_6 : MulSemiringAction.{u_3, u_4} Gal(L/K) B
D' : Type u_8
inst_7 : Field D'
inst_8 : Algebra D' L
inst_9 : IsDecompositionField K L P D
inst_10 : IsDecompositionField K L P D'
x : D
⊢ Eq.{u_3 + 1} (α := L) ((algebraMap D' L : (a : D') → L) ((ringEquiv K L P D D' : (a : D) → D') x : D') : L)
    ((algebraMap D L : (a : D) → L) x : L)

Tactic:
simp [IsDecompositionField.ringEquiv, IsGaloisGroup.ringEquiv]

Premises used: IsDecompositionField.ringEquiv, IsGaloisGroup.ringEquiv
-- 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
D : Type u_5
inst_4 : Field D
inst_5 : Algebra D L
inst_6 : MulSemiringAction.{u_3, u_4} Gal(L/K) B
D' : Type u_8
inst_7 : Field D'
inst_8 : Algebra D' L
inst_9 : IsDecompositionField K L P D
inst_10 : IsDecompositionField K L P D'
x : D'
⊢ Eq.{u_3 + 1} (α := L)
    ((algebraMap D L : (a : D) → L) ((RingEquiv.symm (ringEquiv K L P D D') : (a : D') → D) x : D) : L)
    ((algebraMap D' L : (a : D') → L) x : L)

Tactic:
simp [IsDecompositionField.ringEquiv, IsGaloisGroup.ringEquiv]

Premises used: IsDecompositionField.ringEquiv, IsGaloisGroup.ringEquiv
-- 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
E' : Type u_9
inst_7 : Field E'
inst_8 : Algebra E' L
inst_9 : IsInertiaField K L P E
inst_10 : IsInertiaField K L P E'
x : E
⊢ Eq.{u_3 + 1} (α := L) ((algebraMap E' L : (a : E') → L) ((ringEquiv K L P E E' : (a : E) → E') x : E') : L)
    ((algebraMap E L : (a : E) → L) x : L)

Tactic:
simp [IsInertiaField.ringEquiv, IsGaloisGroup.ringEquiv]

Premises used: IsInertiaField.ringEquiv, IsGaloisGroup.ringEquiv
-- 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
E' : Type u_9
inst_7 : Field E'
inst_8 : Algebra E' L
inst_9 : IsInertiaField K L P E
inst_10 : IsInertiaField K L P E'
x : E'
⊢ Eq.{u_3 + 1} (α := L)
    ((algebraMap E L : (a : E) → L) ((RingEquiv.symm (ringEquiv K L P E E') : (a : E') → E) x : E) : L)
    ((algebraMap E' L : (a : E') → L) x : L)

Tactic:
simp [IsInertiaField.ringEquiv, IsGaloisGroup.ringEquiv]

Premises used: IsInertiaField.ringEquiv, IsGaloisGroup.ringEquiv
-- Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory
Goal:
A : Type u_1
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 A
inst_4 : CommRing B
inst_5 : Algebra A B
p : Ideal A
P : Ideal B
inst_6 : P.LiesOver p
inst_7 : FiniteDimensional K L
inst_8 : MulSemiringAction.{u_3, u_4} Gal(L/K) B
inst_9 : IsGaloisGroup.{u_3, u_1, u_4} Gal(L/K) A B
inst_10 : IsDedekindDomain A
inst_11 : IsDedekindDomain B
inst_12 : Module.Finite A B
inst_13 : Module.IsTorsionFree A B
inst_14 : Ring.HasFiniteQuotients A
inst_15 : P.IsMaximal
D : Type u_5
inst_16 : Field D
inst_17 : Algebra D L
inst_18 : IsDecompositionField K L P D
hp : p ≠ ⊥
⊢ p.IsMaximal

Tactic:
have : p.IsMaximal := over_def P p ▸ Ideal.IsMaximal.under A P
-- Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory
Goal:
A : Type u_1
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 A
inst_4 : CommRing B
inst_5 : Algebra A B
p : Ideal A
P : Ideal B
inst_6 : P.LiesOver p
inst_7 : FiniteDimensional K L
inst_8 : MulSemiringAction.{u_3, u_4} Gal(L/K) B
inst_9 : IsGaloisGroup.{u_3, u_1, u_4} Gal(L/K) A B
inst_10 : IsDedekindDomain A
inst_11 : IsDedekindDomain B
inst_12 : Module.Finite A B
inst_13 : Module.IsTorsionFree A B
inst_14 : Ring.HasFiniteQuotients A
inst_15 : P.IsMaximal
D : Type u_5
inst_16 : Field D
inst_17 : Algebra D L
inst_18 : IsDecompositionField K L P D
hp : p ≠ ⊥
this : p.IsMaximal
⊢ Finite.{u_1 + 1} (A ⧸ p)

Tactic:
have : Finite (A ⧸ p) := Ring.HasFiniteQuotients.finiteQuotient hp
-- Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory
Goal:
A : Type u_1
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 A
inst_4 : CommRing B
inst_5 : Algebra A B
p : Ideal A
P : Ideal B
inst_6 : P.LiesOver p
inst_7 : FiniteDimensional K L
inst_8 : MulSemiringAction.{u_3, u_4} Gal(L/K) B
inst_9 : IsGaloisGroup.{u_3, u_1, u_4} Gal(L/K) A B
inst_10 : IsDedekindDomain A
inst_11 : IsDedekindDomain B
inst_12 : Module.Finite A B
inst_13 : Module.IsTorsionFree A B
inst_14 : Ring.HasFiniteQuotients A
inst_15 : P.IsMaximal
D : Type u_5
inst_16 : Field D
inst_17 : Algebra D L
inst_18 : IsDecompositionField K L P D
hp : p ≠ ⊥
this_1 : p.IsMaximal
this : Finite.{u_1 + 1} (A ⧸ p)
rw : Nat.card.{u_3} ↥(stabilizer Gal(L/K) P) = p.ramificationIdxIn B * p.inertiaDegIn B
rw₁ rw₂ : p.ramificationIdxIn B * p.inertiaDegIn B = p.ramificationIdxIn B * p.inertiaDegIn B
⊢ Module.finrank D L = p.ramificationIdxIn B * p.inertiaDegIn B

Tactic:
rw [← IsGaloisGroup.card_eq_finrank (stabilizer Gal(L/K) P) D L, card_stabilizer_eq p hp]

Premises used: Ideal.card_stabilizer_eq, Membership.mem, Subtype, AlgEquiv, MulAction.stabilizer, IsGaloisGroup.card_eq_finrank
-- Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory
Goal:
A : Type u_1
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 A
inst_4 : CommRing B
inst_5 : Algebra A B
p : Ideal A
P : Ideal B
inst_6 : P.LiesOver p
inst_7 : FiniteDimensional K L
inst_8 : MulSemiringAction.{u_3, u_4} Gal(L/K) B
inst_9 : IsGaloisGroup.{u_3, u_1, u_4} Gal(L/K) A B
inst_10 : IsDedekindDomain A
inst_11 : IsDedekindDomain B
inst_12 : Module.Finite A B
inst_13 : Module.IsTorsionFree A B
inst_14 : Ring.HasFiniteQuotients A
inst_15 : P.IsMaximal
D : Type u_5
inst_16 : Field D
inst_17 : Algebra D L
inst_18 : IsDecompositionField K L P D
inst_19 : IsGalois K L
inst_20 : Algebra K D
inst_21 : IsScalarTower K D L
hp : p ≠ ⊥
⊢ p.IsMaximal

Tactic:
have : p.IsMaximal := over_def P p ▸ Ideal.IsMaximal.under A P
-- Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory
Goal:
A : Type u_1
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 A
inst_4 : CommRing B
inst_5 : Algebra A B
p : Ideal A
P : Ideal B
inst_6 : P.LiesOver p
inst_7 : FiniteDimensional K L
inst_8 : MulSemiringAction.{u_3, u_4} Gal(L/K) B
inst_9 : IsGaloisGroup.{u_3, u_1, u_4} Gal(L/K) A B
inst_10 : IsDedekindDomain A
inst_11 : IsDedekindDomain B
inst_12 : Module.Finite A B
inst_13 : Module.IsTorsionFree A B
inst_14 : Ring.HasFiniteQuotients A
inst_15 : P.IsMaximal
D : Type u_5
inst_16 : Field D
inst_17 : Algebra D L
inst_18 : IsDecompositionField K L P D
inst_19 : IsGalois K L
inst_20 : Algebra K D
inst_21 : IsScalarTower K D L
hp : p ≠ ⊥
this : p.IsMaximal
⊢ FiniteDimensional D L

Tactic:
have : FiniteDimensional D L := FiniteDimensional.right K D L