awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw : Module.finrank K L = Set.ncard (α := Ideal B) (p.primesOver B) * p.inertiaDegIn B * Module.finrank 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 * p.ramificationIdxIn B
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]
-- 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
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
⊢ 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 * p.ramificationIdxIn B)
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]
-- 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
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)
⊢ 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.ramificationIdxIn B * p.inertiaDegIn B)
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]
-- 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
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)
⊢ 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 = Nat.card.{u_3} Gal(L/K)
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]
-- 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
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)
⊢ 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 = Module.finrank K 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]
-- 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
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 ≠ ⊥
⊢ Module.finrank D E = 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
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 D E = p.inertiaDegIn B
have this₁ : Module.finrank K D * Module.finrank D E = Module.finrank K E
Tactic: have := Module.finrank_mul_finrank K D E
-- 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
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
⊢ Module.finrank D E = p.inertiaDegIn B
have 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
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (hypothesis)
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.inertiaDeg P = 0
have this : P = ⊤
Tactic: have := Ideal.Quotient.subsingleton_iff.mp hQ
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
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 = ⊤
⊢ p.inertiaDeg P = 0
have subst : ∀ [hQ : Subsingleton.{v + 1} (HasQuotient.Quotient S (B := Ideal S) ⊤)], inertiaDeg.{u, v} (S := S) p ⊤ = 0
Tactic: subst this
Cleared hypotheses: P, hQ, this
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
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
⊢ p.inertiaDeg P = finrank.{u, v} (R ⧸ p) (S ⧸ P)
have 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)
Tactic: rw [inertiaDeg, dif_pos (over_def P p).symm]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
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)
⊢ p.inertiaDeg P = finrank.{u, v} (R ⧸ p) (S ⧸ P)
have rw₁ : finrank.{u, v} (R ⧸ p) (S ⧸ P) = finrank.{u, v} (R ⧸ p) (S ⧸ P)
Tactic: rw [inertiaDeg, dif_pos (over_def P p).symm]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
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
have rw : comap (F := R →+* S) f (comap (F := S →+* S₁) (↑e : S →+* S₁) P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
Tactic: rw [← comap_coe e, comap_comap, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
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
⊢ comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
have rw₁ : comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e : S →+* S₁) f) P = p ↔
  comap (F := R →+* S₁) (algebraMap R S₁) P = p
Tactic: rw [← comap_coe e, comap_comap, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
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
⊢ comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
have 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
Tactic: rw [← comap_coe e, comap_comap, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
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
⊢ comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
have rw₃ : comap (F := R →+* S₁) (algebraMap R S₁) P = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
Tactic: rw [← comap_coe e, comap_comap, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (hypothesis)
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₁
⊢ p.inertiaDeg (comap e P) = p.inertiaDeg P
have he : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
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₁
he : comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
⊢ p.inertiaDeg (comap e P) = p.inertiaDeg P
have pos : ∀ (h : P.LiesOver p), p.inertiaDeg (comap e P) = p.inertiaDeg P
Tactic: by_cases h : P.LiesOver p
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
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₁
he : comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
pos : ∀ (h : P.LiesOver p), p.inertiaDeg (comap e P) = p.inertiaDeg P
⊢ p.inertiaDeg (comap e P) = p.inertiaDeg P
have neg : ∀ (h : ¬P.LiesOver p), p.inertiaDeg (comap e P) = p.inertiaDeg P
Tactic: by_cases h : P.LiesOver p
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
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₁
he : comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
h : P.LiesOver p
⊢ p.inertiaDeg (comap e P) = p.inertiaDeg P
have pos : finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (comap e P)) = finrank.{u, u_1} (R ⧸ p) (S₁ ⧸ P)
Tactic: rw [inertiaDeg_algebraMap, inertiaDeg_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
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₁
he : comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
h : ¬P.LiesOver p
⊢ p.inertiaDeg (comap e P) = p.inertiaDeg P
have neg : 0 = p.inertiaDeg P
Tactic: rw [inertiaDeg, dif_neg (fun eq => h ⟨(he.mp eq).symm⟩)]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
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₁
he : comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
h : ¬P.LiesOver p
⊢ 0 = p.inertiaDeg P
have neg : Eq (α := ℕ) 0 (if hPp : comap (F := R →+* S₁) (algebraMap R S₁) P = p then finrank.{u, u_1} (R ⧸ p) (S₁ ⧸ P) else 0)
Tactic: rw [inertiaDeg, dif_neg (fun eq => h ⟨eq.symm⟩)]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
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₁
he : comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
h : ¬P.LiesOver p
neg :
  Eq (α := ℕ) 0 (if hPp : comap (F := R →+* S₁) (algebraMap R S₁) P = p then finrank.{u, u_1} (R ⧸ p) (S₁ ⧸ P) else 0)
⊢ 0 = p.inertiaDeg P
have neg₁ : Eq (α := ℕ) 0 0
Tactic: rw [inertiaDeg, dif_neg (fun eq => h ⟨eq.symm⟩)]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
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₁
P : Ideal S
E : Type u_2
inst_5 : EquivLike E S S₁
inst_6 : AlgEquivClass E R S S₁
e : E
⊢ inertiaDeg.{u, u_1} (S := S₁) p (map e P) = p.inertiaDeg P
have rw : p.inertiaDeg (comap (F := S₁ ≃+* S) (RingEquiv.symm (↑e : S ≃+* S₁)) P) = p.inertiaDeg P
Tactic: rw [show P.map e = _ from map_comap_of_equiv (RingEquivClass.toRingEquiv e : S ≃+* S₁)]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal S
inst_3 : Nontrivial R
inst_4 : IsDomain S
inst_5 : Algebra.IsIntegral R S
hP : LiesOver.{u, v} (A := R) P ⊥
⊢ inertiaDeg.{u, v} (R := R) ⊥ P = finrank R S
have rw : finrank.{u, v} (HasQuotient.Quotient R (B := Ideal R) ⊥) (S ⧸ P) = finrank R S
Tactic: rw [inertiaDeg, dif_pos (over_def P (⊥ : Ideal R)).symm]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (hypothesis)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal S
inst_3 : Nontrivial R
inst_4 : IsDomain S
inst_5 : Algebra.IsIntegral R S
hP : LiesOver.{u, v} (A := R) P ⊥
⊢ finrank.{u, v} (HasQuotient.Quotient R (B := Ideal R) ⊥) (S ⧸ P) = finrank R S
have hP₁ : P = ⊥
Tactic: replace hP : P = ⊥ := eq_bot_of_liesOver_bot R P
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal S
inst_3 : Nontrivial R
inst_4 : IsDomain S
inst_5 : Algebra.IsIntegral R S
hP_1 : LiesOver.{u, v} (A := R) P ⊥
hP : P = ⊥
⊢ finrank.{u, v} (HasQuotient.Quotient R (B := Ideal R) ⊥) (S ⧸ P) = finrank R S
have rw : Eq (α := RingHom.{u, v} R (S ⧸ P))
  (RingHom.comp (algebraMap (HasQuotient.Quotient R (B := Ideal R) ⊥) (S ⧸ P))
    (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.quotientBot R))))
  ((RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.trans (quotEquivOfEq hP) (RingEquiv.quotientBot S)))).comp f)
Tactic: rw [Algebra.finrank_eq_of_equiv_equiv (RingEquiv.quotientBot R).symm
    ((quotEquivOfEq hP).trans (RingEquiv.quotientBot S)).symm]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (hypothesis)
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
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : Module.Finite R T
Q : Ideal T
inst_8 : P.LiesOver p
inst_9 : Q.LiesOver P
inst_10 : p.IsPrime
⊢ P.inertiaDeg Q ≤ p.inertiaDeg Q
have this : Q.LiesOver p
Tactic: have : Q.LiesOver p := LiesOver.trans Q P p
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Inertia (goal)
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
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : Module.Finite R T
Q : Ideal T
inst_8 : P.LiesOver p
inst_9 : Q.LiesOver P
inst_10 : p.IsPrime
this : Q.LiesOver p
⊢ P.inertiaDeg Q ≤ p.inertiaDeg Q
have rw : finrank.{v, u_2} (S ⧸ P) (T ⧸ Q) ≤ finrank.{u, u_2} (R ⧸ p) (T ⧸ Q)
Tactic: rw [inertiaDeg_algebraMap, inertiaDeg_algebraMap]