awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ 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} (α := G) (β := 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) :
        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) sorry) :
                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)
Tactic: simp_rw [smul_div₀', subgroup_smul_def, ← algebraMap.smul', ← subgroup_smul_def,
      inertiaEquiv_symm_apply_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (hypothesis)
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 ≠ ⊥
⊢ Module.finrank D L = p.ramificationIdxIn B * p.inertiaDegIn B
have this : p.IsMaximal
Tactic: have : p.IsMaximal := over_def P p ▸ Ideal.IsMaximal.under A P
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (hypothesis)
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
⊢ Module.finrank D L = p.ramificationIdxIn B * p.inertiaDegIn B
have this₁ : Finite.{u_1 + 1} (A ⧸ p)
Tactic: have : Finite (A ⧸ p) := Ring.HasFiniteQuotients.finiteQuotient hp
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (goal)
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)
⊢ Module.finrank D L = p.ramificationIdxIn B * p.inertiaDegIn B
have rw : Nat.card.{u_3} ↥(stabilizer Gal(L/K) P) = p.ramificationIdxIn B * p.inertiaDegIn B
Tactic: rw [← IsGaloisGroup.card_eq_finrank (stabilizer Gal(L/K) P) D L, card_stabilizer_eq p hp]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (goal)
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
⊢ Module.finrank D L = p.ramificationIdxIn B * p.inertiaDegIn B
have rw₁ : p.ramificationIdxIn B * p.inertiaDegIn B = p.ramificationIdxIn B * p.inertiaDegIn B
Tactic: rw [← IsGaloisGroup.card_eq_finrank (stabilizer Gal(L/K) P) D L, card_stabilizer_eq p hp]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (hypothesis)
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 ≠ ⊥
⊢ Module.finrank K D = Set.ncard (α := Ideal B) (p.primesOver B)
have this : p.IsMaximal
Tactic: have : p.IsMaximal := over_def P p ▸ Ideal.IsMaximal.under A P
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (hypothesis)
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
⊢ Module.finrank K D = Set.ncard (α := Ideal B) (p.primesOver B)
have this₁ : FiniteDimensional D L
Tactic: have : FiniteDimensional D L := FiniteDimensional.right K D L
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (goal)
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_1 : p.IsMaximal
this : FiniteDimensional D L
⊢ Module.finrank K D = Set.ncard (α := Ideal B) (p.primesOver B)
have refine : Eq (α := ℕ) ((fun (a : ℕ) ↦ a * Module.finrank D L) (Module.finrank K D))
  ((fun (a : ℕ) ↦ a * Module.finrank D L) (Set.ncard (α := Ideal B) (p.primesOver B)))
Tactic: refine mul_left_injective₀ (b := Module.finrank D L) Module.finrank_pos.ne' ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (goal)
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_1 : p.IsMaximal
this : FiniteDimensional D L
⊢ Module.finrank K D * Module.finrank D L = Set.ncard (α := Ideal B) (p.primesOver B) * Module.finrank D L
have rw : Module.finrank K L = Set.ncard (α := Ideal B) (p.primesOver B) * Module.finrank D L
Tactic: rw [Module.finrank_mul_finrank, rank_left A K L P D hp,
    ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp B Gal(L/K),
    IsGaloisGroup.card_eq_finrank Gal(L/K) K L]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (goal)
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_1 : p.IsMaximal
this : FiniteDimensional D L
rw : Module.finrank K L = Set.ncard (α := Ideal B) (p.primesOver B) * Module.finrank D L
⊢ Module.finrank K D * Module.finrank D L = Set.ncard (α := Ideal B) (p.primesOver B) * Module.finrank D L
have rw₁ : Module.finrank K L = Set.ncard (α := Ideal B) (p.primesOver B) * (p.ramificationIdxIn B * p.inertiaDegIn B)
Tactic: rw [Module.finrank_mul_finrank, rank_left A K L P D hp,
    ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp B Gal(L/K),
    IsGaloisGroup.card_eq_finrank Gal(L/K) K L]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (goal)
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_1 : p.IsMaximal
this : FiniteDimensional D L
rw : Module.finrank K L = Set.ncard (α := Ideal B) (p.primesOver B) * Module.finrank D L
rw₁ : Module.finrank K L = Set.ncard (α := Ideal B) (p.primesOver B) * (p.ramificationIdxIn B * p.inertiaDegIn B)
⊢ Module.finrank K D * Module.finrank D L = Set.ncard (α := Ideal B) (p.primesOver B) * Module.finrank D L
have rw₂ : Module.finrank K L = Nat.card.{u_3} Gal(L/K)
Tactic: rw [Module.finrank_mul_finrank, rank_left A K L P D hp,
    ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp B Gal(L/K),
    IsGaloisGroup.card_eq_finrank Gal(L/K) K L]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (goal)
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_1 : p.IsMaximal
this : FiniteDimensional D L
rw : Module.finrank K L = Set.ncard (α := Ideal B) (p.primesOver B) * Module.finrank D L
rw₁ : Module.finrank K L = Set.ncard (α := Ideal B) (p.primesOver B) * (p.ramificationIdxIn B * p.inertiaDegIn B)
rw₂ : Module.finrank K L = Nat.card.{u_3} Gal(L/K)
⊢ Module.finrank K D * Module.finrank D L = Set.ncard (α := Ideal B) (p.primesOver B) * Module.finrank D L
have rw₃ : Module.finrank K L = Module.finrank K L
Tactic: rw [Module.finrank_mul_finrank, rank_left A K L P D hp,
    ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp B Gal(L/K),
    IsGaloisGroup.card_eq_finrank Gal(L/K) K L]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (hypothesis)
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
E : Type u_6
inst_16 : Field E
inst_17 : Algebra E L
inst_18 : IsInertiaField K L P E
hp : p ≠ ⊥
⊢ Module.finrank E L = p.ramificationIdxIn B
have this : p.IsMaximal
Tactic: have : p.IsMaximal := over_def P p ▸ Ideal.IsMaximal.under A P
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (hypothesis)
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
E : Type u_6
inst_16 : Field E
inst_17 : Algebra E L
inst_18 : IsInertiaField K L P E
hp : p ≠ ⊥
this : p.IsMaximal
⊢ Module.finrank E L = p.ramificationIdxIn B
have this₁ : Finite.{u_1 + 1} (A ⧸ p)
Tactic: have : Finite (A ⧸ p) := Ring.HasFiniteQuotients.finiteQuotient hp
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (goal)
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
E : Type u_6
inst_16 : Field E
inst_17 : Algebra E L
inst_18 : IsInertiaField K L P E
hp : p ≠ ⊥
this_1 : p.IsMaximal
this : Finite.{u_1 + 1} (A ⧸ p)
⊢ Module.finrank E L = p.ramificationIdxIn B
have rw : Nat.card.{u_3} ↥(inertia Gal(L/K) P) = p.ramificationIdxIn B
Tactic: rw [← IsGaloisGroup.card_eq_finrank (inertia Gal(L/K) P) E L,
    card_inertia_eq_ramificationIdxIn p hp]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (goal)
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
E : Type u_6
inst_16 : Field E
inst_17 : Algebra E L
inst_18 : IsInertiaField K L P E
hp : p ≠ ⊥
this_1 : p.IsMaximal
this : Finite.{u_1 + 1} (A ⧸ p)
rw : Nat.card.{u_3} ↥(inertia Gal(L/K) P) = p.ramificationIdxIn B
⊢ Module.finrank E L = p.ramificationIdxIn B
have rw₁ : p.ramificationIdxIn B = p.ramificationIdxIn B
Tactic: rw [← IsGaloisGroup.card_eq_finrank (inertia Gal(L/K) P) E L,
    card_inertia_eq_ramificationIdxIn p hp]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (hypothesis)
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
E : Type u_6
inst_16 : Field E
inst_17 : Algebra E L
inst_18 : IsInertiaField K L P E
inst_19 : IsGalois K L
inst_20 : Algebra K E
inst_21 : IsScalarTower K E L
hp : p ≠ ⊥
⊢ Module.finrank K E = Set.ncard (α := Ideal B) (p.primesOver B) * p.inertiaDegIn B
have this : p.IsMaximal
Tactic: have : p.IsMaximal := over_def P p ▸ Ideal.IsMaximal.under A P
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (hypothesis)
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
E : Type u_6
inst_16 : Field E
inst_17 : Algebra E L
inst_18 : IsInertiaField K L P E
inst_19 : IsGalois K L
inst_20 : Algebra K E
inst_21 : IsScalarTower K E L
hp : p ≠ ⊥
this : p.IsMaximal
⊢ Module.finrank K E = Set.ncard (α := Ideal B) (p.primesOver B) * p.inertiaDegIn B
have this₁ : FiniteDimensional E L
Tactic: have : FiniteDimensional E L := FiniteDimensional.right K E L
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (goal)
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
E : Type u_6
inst_16 : Field E
inst_17 : Algebra E L
inst_18 : IsInertiaField K L P E
inst_19 : IsGalois K L
inst_20 : Algebra K E
inst_21 : IsScalarTower K E L
hp : p ≠ ⊥
this_1 : p.IsMaximal
this : FiniteDimensional E L
⊢ Module.finrank K E = Set.ncard (α := Ideal B) (p.primesOver B) * p.inertiaDegIn B
have refine : Eq (α := ℕ) ((fun (a : ℕ) ↦ a * Module.finrank E L) (Module.finrank K E))
  ((fun (a : ℕ) ↦ a * Module.finrank E L) (Set.ncard (α := Ideal B) (p.primesOver B) * p.inertiaDegIn B))
Tactic: refine mul_left_injective₀ (b := Module.finrank E L) Module.finrank_pos.ne' ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.HilbertTheory (goal)
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
E : Type u_6
inst_16 : Field E
inst_17 : Algebra E L
inst_18 : IsInertiaField K L P E
inst_19 : IsGalois K L
inst_20 : Algebra K E
inst_21 : IsScalarTower K E L
hp : p ≠ ⊥
this_1 : p.IsMaximal
this : FiniteDimensional E L
⊢ Module.finrank K E * Module.finrank E L =
    Set.ncard (α := Ideal B) (p.primesOver B) * p.inertiaDegIn B * Module.finrank E L
have rw : Module.finrank K L = Set.ncard (α := Ideal B) (p.primesOver B) * p.inertiaDegIn B * Module.finrank E L
Tactic: rw [Module.finrank_mul_finrank, rank_left A K L P E hp, mul_assoc, mul_comm (p.inertiaDegIn B),
    ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp B Gal(L/K),
    IsGaloisGroup.card_eq_finrank Gal(L/K) K L]