awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : p.IsMaximal
this : FiniteDimensional D L
⊢ Module.finrank K D = Set.ncard (α := Ideal B) (p.primesOver B)

Tactic:
mul_left_injective₀ (b := Module.finrank D L) Module.finrank_pos.ne' ?_

Premises used: mul_left_injective₀, LT.lt.ne', Module.finrank_pos
-- 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_1 : p.IsMaximal
this : FiniteDimensional D L
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)))
⊢ Module.finrank K D = Set.ncard (α := Ideal B) (p.primesOver B)

Tactic:
refine mul_left_injective₀ (b := Module.finrank D L) Module.finrank_pos.ne' ?_

Premises used: mul_left_injective₀, LT.lt.ne', Module.finrank_pos
-- 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_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)
rw₃ rw₄ : Module.finrank K L = Module.finrank K L
⊢ Module.finrank K D * Module.finrank D 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]

Premises used: Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn, IsDecompositionField.rank_left, AlgEquiv, Module.finrank_mul_finrank, 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
E : Type u_6
inst_16 : Field E
inst_17 : Algebra E L
inst_18 : IsInertiaField K L P E
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
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
⊢ 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
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
rw₁ rw₂ : p.ramificationIdxIn B = p.ramificationIdxIn B
⊢ Module.finrank E L = p.ramificationIdxIn B

Tactic:
rw [← IsGaloisGroup.card_eq_finrank (inertia Gal(L/K) P) E L,
    card_inertia_eq_ramificationIdxIn p hp]

Premises used: Membership.mem, Ideal.inertia, Subtype, AlgEquiv, Ideal.card_inertia_eq_ramificationIdxIn, 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
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 ≠ ⊥
⊢ 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
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
⊢ FiniteDimensional E L

Tactic:
have : FiniteDimensional E L := FiniteDimensional.right K E L
-- 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
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

Tactic:
mul_left_injective₀ (b := Module.finrank E L) Module.finrank_pos.ne' ?_

Premises used: mul_left_injective₀, LT.lt.ne', Module.finrank_pos
-- 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
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
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))
⊢ Module.finrank K E = Set.ncard (α := Ideal B) (p.primesOver B) * p.inertiaDegIn B

Tactic:
refine mul_left_injective₀ (b := Module.finrank E L) Module.finrank_pos.ne' ?_

Premises used: mul_left_injective₀, LT.lt.ne', Module.finrank_pos
-- 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
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
rw : Module.finrank K L = Set.ncard (α := Ideal B) (p.primesOver B) * p.inertiaDegIn B * Module.finrank E L
rw₁ : Module.finrank K L = Set.ncard (α := Ideal B) (p.primesOver B) * p.inertiaDegIn B * p.ramificationIdxIn B
rw₂ : Module.finrank K L = Set.ncard (α := Ideal B) (p.primesOver B) * (p.inertiaDegIn B * p.ramificationIdxIn B)
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)
rw₅ rw₆ : Module.finrank K L = Module.finrank K L
⊢ Module.finrank K E * Module.finrank E 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]

Premises used: IsInertiaField.rank_left, mul_assoc, Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn, Ideal.inertiaDegIn, AlgEquiv, Module.finrank_mul_finrank, mul_comm, 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
E : Type u_6
inst_19 : Field E
inst_20 : Algebra E L
inst_21 : IsInertiaField K L P E
inst_22 : IsGalois K L
inst_23 : Algebra K D
inst_24 : Algebra K E
inst_25 : Algebra D E
inst_26 : IsScalarTower K D E
inst_27 : IsScalarTower K E L
inst_28 : 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
E : Type u_6
inst_19 : Field E
inst_20 : Algebra E L
inst_21 : IsInertiaField K L P E
inst_22 : IsGalois K L
inst_23 : Algebra K D
inst_24 : Algebra K E
inst_25 : Algebra D E
inst_26 : IsScalarTower K D E
inst_27 : IsScalarTower K E L
inst_28 : IsScalarTower K D L
hp : p ≠ ⊥
this : p.IsMaximal
⊢ Module.finrank K D * Module.finrank D E = Module.finrank K E

Tactic:
have := Module.finrank_mul_finrank K D E
-- 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
E : Type u_6
inst_19 : Field E
inst_20 : Algebra E L
inst_21 : IsInertiaField K L P E
inst_22 : IsGalois K L
inst_23 : Algebra K D
inst_24 : Algebra K E
inst_25 : Algebra D E
inst_26 : IsScalarTower K D E
inst_27 : IsScalarTower K E L
inst_28 : IsScalarTower K D L
hp : p ≠ ⊥
this_1 : p.IsMaximal
this : Module.finrank K D * Module.finrank D E = Module.finrank K E
rwa :
  ∀
    (this :
      Set.ncard (α := Ideal B) (p.primesOver B) * Module.finrank D E =
        Set.ncard (α := Ideal B) (p.primesOver B) * p.inertiaDegIn B),
    Set.ncard (α := Ideal B) (p.primesOver B) ≠ 0
⊢ Module.finrank D E = p.inertiaDegIn B

Tactic:
rwa [IsInertiaField.rank_right A K L P E hp, IsDecompositionField.rank_right A K L P D hp,
    mul_right_inj'] at this

Premises used: IsDecompositionField.rank_right, IsInertiaField.rank_right, mul_right_inj'
-- 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
E : Type u_6
inst_19 : Field E
inst_20 : Algebra E L
inst_21 : IsInertiaField K L P E
inst_22 : IsGalois K L
inst_23 : Algebra K D
inst_24 : Algebra K E
inst_25 : Algebra D E
inst_26 : IsScalarTower K D E
inst_27 : IsScalarTower K E L
inst_28 : IsScalarTower K D L
hp : p ≠ ⊥
this_1 : p.IsMaximal
this :
  Set.ncard (α := Ideal B) (p.primesOver B) * Module.finrank D E =
    Set.ncard (α := Ideal B) (p.primesOver B) * p.inertiaDegIn B
⊢ Set.ncard (α := Ideal B) (p.primesOver B) ≠ 0

Tactic:
IsDedekindDomain.primesOver_ncard_ne_zero p B

Premises used: IsDedekindDomain.primesOver_ncard_ne_zero
-- 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
E : Type u_6
inst_19 : Field E
inst_20 : Algebra E L
inst_21 : IsInertiaField K L P E
inst_22 : IsGalois K L
inst_23 : Algebra K D
inst_24 : Algebra K E
inst_25 : Algebra D E
inst_26 : IsScalarTower K D E
inst_27 : IsScalarTower K E L
inst_28 : IsScalarTower K D L
hp : p ≠ ⊥
this_1 : p.IsMaximal
this :
  Set.ncard (α := Ideal B) (p.primesOver B) * Module.finrank D E =
    Set.ncard (α := Ideal B) (p.primesOver B) * p.inertiaDegIn B
⊢ Set.ncard (α := Ideal B) (p.primesOver B) ≠ 0

Tactic:
exact IsDedekindDomain.primesOver_ncard_ne_zero p B

Premises used: IsDedekindDomain.primesOver_ncard_ne_zero
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : p.IsMaximal
hQ : Subsingleton.{v + 1} (S ⧸ P)
⊢ P = ⊤

Tactic:
have := Ideal.Quotient.subsingleton_iff.mp hQ
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hp : p.IsMaximal
hQ : Subsingleton.{v + 1} (S ⧸ P)
this : P = ⊤
subst : ∀ [hQ : Subsingleton.{v + 1} (HasQuotient.Quotient S (B := Ideal S) ⊤)], inertiaDeg.{u, v} (S := S) p ⊤ = 0
⊢ p.inertiaDeg P = 0

Tactic:
subst this
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
hp : p.IsMaximal
hQ : Subsingleton.{v + 1} (HasQuotient.Quotient S (B := Ideal S) ⊤)
⊢ inertiaDeg.{u, v} (S := S) p ⊤ = 0

Tactic:
dif_neg fun h => hp.ne_top <| h.symm.trans comap_top

Premises used: Ideal.inertiaDeg, dif_neg, Ideal.IsMaximal.ne_top
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
hp : p.IsMaximal
hQ : Subsingleton.{v + 1} (HasQuotient.Quotient S (B := Ideal S) ⊤)
⊢ inertiaDeg.{u, v} (S := S) p ⊤ = 0

Tactic:
exact dif_neg fun h => hp.ne_top <| h.symm.trans comap_top

Premises used: dif_neg, Ideal.IsMaximal.ne_top
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : P.LiesOver p
rw : (if hPp : comap (F := R →+* S) f P = p then finrank.{u, v} (R ⧸ p) (S ⧸ P) else 0) = finrank.{u, v} (R ⧸ p) (S ⧸ P)
rw₁ rw₂ : finrank.{u, v} (R ⧸ p) (S ⧸ P) = finrank.{u, v} (R ⧸ p) (S ⧸ P)
⊢ p.inertiaDeg P = finrank.{u, v} (R ⧸ p) (S ⧸ P)

Tactic:
rw [inertiaDeg, dif_pos (over_def P p).symm]

Premises used: Ideal.inertiaDeg, dif_pos, Ideal.over_def, Eq.symm
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : p.IsMaximal
inst_4 : Module.Finite R S
inst_5 : P.LiesOver p
⊢ 0 < p.inertiaDeg P

Tactic:
have : Nontrivial (S ⧸ P) := Quotient.nontrivial_of_liesOver_of_isPrime P p
  finrank_pos.trans_eq (inertiaDeg_algebraMap p P).symm

Premises used: Ideal.Quotient.nontrivial_of_liesOver_of_isPrime, Ideal.inertiaDeg_algebraMap, LT.lt.trans_eq, Eq.symm, Module.finrank_pos
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : P.IsPrime
inst_4 : Module.Finite R S
inst_5 : P.LiesOver p
⊢ 0 < p.inertiaDeg P

Tactic:
have : p.IsPrime := Ideal.over_def P p ▸ inferInstance
  Module.finrank_pos.trans_eq (inertiaDeg_algebraMap p P).symm

Premises used: Ideal.inertiaDeg_algebraMap, Eq.rec, inferInstance, LT.lt.trans_eq, Ideal.over_def, Eq.symm, Module.finrank_pos
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : p.IsMaximal
inst_4 : Module.Finite R S
inst_5 : P.LiesOver p
⊢ p.inertiaDeg P ≠ 0

Tactic:
(Nat.ne_of_lt (inertiaDeg_pos p P)).symm

Premises used: Ne.symm, Ideal.inertiaDeg_pos, Nat.ne_of_lt
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
rw :
  comap (F := R →+* S) f (comap (F := S →+* S₁) (↑e : S →+* S₁) P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
rw₁ :
  comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e : S →+* S₁) f) P = p ↔
    comap (F := R →+* S₁) (algebraMap R S₁) P = p
rw₂ :
  comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(↑e : S →ₐ[R] S₁) : S →+* S₁) f) P = p ↔
    comap (F := R →+* S₁) (algebraMap R S₁) P = p
rw₃ rw₄ : comap (F := R →+* S₁) (algebraMap R S₁) P = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
⊢ comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p

Tactic:
rw [← comap_coe e, comap_comap, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]

Premises used: AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap, Ideal.comap_coe, Ideal.comap_comap
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
⊢ comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p

Tactic:
have he : (P.comap e).comap (algebraMap R S) = p ↔ P.comap (algebraMap R S₁) = p := by
    rw [← comap_coe e, comap_comap, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]