awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.LiesOver p
inst_4 : p.IsMaximal
inst_5 : q.IsMaximal
this_1 : Field (R ⧸ p) := Quotient.field p
this_2 : Field (S ⧸ q) := Quotient.field q
this_3 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ (S ⧸ q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⧸ q) q.ResidueField)
    (algebraMap (R ⧸ p) (S ⧸ q))
g : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ p.ResidueField _ _ Semiring.toNonAssocSemiring _ (algebraMap p.ResidueField q.ResidueField)
    (algebraMap (R ⧸ p) p.ResidueField)
h : f = g
this : Algebra.{u_1, u_2} (R ⧸ p) q.ResidueField := f.toAlgebra
⊢ Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
have this₁ : IsScalarTower.{u_1, u_2, u_2} (R ⧸ p) (S ⧸ q) q.ResidueField
Tactic: have : IsScalarTower (R ⧸ p) (S ⧸ q) q.ResidueField := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.LiesOver p
inst_4 : p.IsMaximal
inst_5 : q.IsMaximal
this_1 : Field (R ⧸ p) := Quotient.field p
this_2 : Field (S ⧸ q) := Quotient.field q
this_3 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ (S ⧸ q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⧸ q) q.ResidueField)
    (algebraMap (R ⧸ p) (S ⧸ q))
g : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ p.ResidueField _ _ Semiring.toNonAssocSemiring _ (algebraMap p.ResidueField q.ResidueField)
    (algebraMap (R ⧸ p) p.ResidueField)
h : f = g
this_4 : Algebra.{u_1, u_2} (R ⧸ p) q.ResidueField := f.toAlgebra
this : IsScalarTower.{u_1, u_2, u_2} (R ⧸ p) (S ⧸ q) q.ResidueField
⊢ Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
have this₁ : IsScalarTower.{u_1, u_1, u_2} (R ⧸ p) p.ResidueField q.ResidueField
Tactic: have : IsScalarTower (R ⧸ p) p.ResidueField q.ResidueField := IsScalarTower.of_algebraMap_eq' h
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.LiesOver p
inst_4 : p.IsMaximal
inst_5 : q.IsMaximal
this_1 : Field (R ⧸ p) := Quotient.field p
this_2 : Field (S ⧸ q) := Quotient.field q
this_3 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ (S ⧸ q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⧸ q) q.ResidueField)
    (algebraMap (R ⧸ p) (S ⧸ q))
g : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ p.ResidueField _ _ Semiring.toNonAssocSemiring _ (algebraMap p.ResidueField q.ResidueField)
    (algebraMap (R ⧸ p) p.ResidueField)
h : f = g
this_4 : Algebra.{u_1, u_2} (R ⧸ p) q.ResidueField := f.toAlgebra
this_5 : IsScalarTower.{u_1, u_2, u_2} (R ⧸ p) (S ⧸ q) q.ResidueField
this : IsScalarTower.{u_1, u_1, u_2} (R ⧸ p) p.ResidueField q.ResidueField
⊢ Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
have rw : Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) * 1 = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
Tactic: rw [← mul_one (Module.finrank (R ⧸ p) (S ⧸ q)),
    ← Module.finrank_of_bijective_algebraMap (bijective_algebraMap_quotient_residueField q),
    Module.finrank_mul_finrank, ← Module.finrank_mul_finrank (R ⧸ p) p.ResidueField q.ResidueField,
    Module.finrank_of_bijective_algebraMap (bijective_algebraMap_quotient_residueField p), one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.LiesOver p
inst_4 : p.IsMaximal
inst_5 : q.IsMaximal
this_1 : Field (R ⧸ p) := Quotient.field p
this_2 : Field (S ⧸ q) := Quotient.field q
this_3 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ (S ⧸ q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⧸ q) q.ResidueField)
    (algebraMap (R ⧸ p) (S ⧸ q))
g : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ p.ResidueField _ _ Semiring.toNonAssocSemiring _ (algebraMap p.ResidueField q.ResidueField)
    (algebraMap (R ⧸ p) p.ResidueField)
h : f = g
this_4 : Algebra.{u_1, u_2} (R ⧸ p) q.ResidueField := f.toAlgebra
this_5 : IsScalarTower.{u_1, u_2, u_2} (R ⧸ p) (S ⧸ q) q.ResidueField
this : IsScalarTower.{u_1, u_1, u_2} (R ⧸ p) p.ResidueField q.ResidueField
rw : Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) * 1 = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
⊢ Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
have rw₁ : Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) * Module.finrank.{u_2, u_2} (S ⧸ q) q.ResidueField =
  Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
Tactic: rw [← mul_one (Module.finrank (R ⧸ p) (S ⧸ q)),
    ← Module.finrank_of_bijective_algebraMap (bijective_algebraMap_quotient_residueField q),
    Module.finrank_mul_finrank, ← Module.finrank_mul_finrank (R ⧸ p) p.ResidueField q.ResidueField,
    Module.finrank_of_bijective_algebraMap (bijective_algebraMap_quotient_residueField p), one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.LiesOver p
inst_4 : p.IsMaximal
inst_5 : q.IsMaximal
this_1 : Field (R ⧸ p) := Quotient.field p
this_2 : Field (S ⧸ q) := Quotient.field q
this_3 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ (S ⧸ q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⧸ q) q.ResidueField)
    (algebraMap (R ⧸ p) (S ⧸ q))
g : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ p.ResidueField _ _ Semiring.toNonAssocSemiring _ (algebraMap p.ResidueField q.ResidueField)
    (algebraMap (R ⧸ p) p.ResidueField)
h : f = g
this_4 : Algebra.{u_1, u_2} (R ⧸ p) q.ResidueField := f.toAlgebra
this_5 : IsScalarTower.{u_1, u_2, u_2} (R ⧸ p) (S ⧸ q) q.ResidueField
this : IsScalarTower.{u_1, u_1, u_2} (R ⧸ p) p.ResidueField q.ResidueField
rw : Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) * 1 = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
rw₁ :
  Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) * Module.finrank.{u_2, u_2} (S ⧸ q) q.ResidueField =
    Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
⊢ Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
have rw₂ : Module.finrank.{u_1, u_2} (R ⧸ p) q.ResidueField = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
Tactic: rw [← mul_one (Module.finrank (R ⧸ p) (S ⧸ q)),
    ← Module.finrank_of_bijective_algebraMap (bijective_algebraMap_quotient_residueField q),
    Module.finrank_mul_finrank, ← Module.finrank_mul_finrank (R ⧸ p) p.ResidueField q.ResidueField,
    Module.finrank_of_bijective_algebraMap (bijective_algebraMap_quotient_residueField p), one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.LiesOver p
inst_4 : p.IsMaximal
inst_5 : q.IsMaximal
this_1 : Field (R ⧸ p) := Quotient.field p
this_2 : Field (S ⧸ q) := Quotient.field q
this_3 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ (S ⧸ q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⧸ q) q.ResidueField)
    (algebraMap (R ⧸ p) (S ⧸ q))
g : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ p.ResidueField _ _ Semiring.toNonAssocSemiring _ (algebraMap p.ResidueField q.ResidueField)
    (algebraMap (R ⧸ p) p.ResidueField)
h : f = g
this_4 : Algebra.{u_1, u_2} (R ⧸ p) q.ResidueField := f.toAlgebra
this_5 : IsScalarTower.{u_1, u_2, u_2} (R ⧸ p) (S ⧸ q) q.ResidueField
this : IsScalarTower.{u_1, u_1, u_2} (R ⧸ p) p.ResidueField q.ResidueField
rw : Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) * 1 = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
rw₁ :
  Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) * Module.finrank.{u_2, u_2} (S ⧸ q) q.ResidueField =
    Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
rw₂ : Module.finrank.{u_1, u_2} (R ⧸ p) q.ResidueField = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
⊢ Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
have rw₃ : Module.finrank.{u_1, u_1} (R ⧸ p) p.ResidueField * Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField =
  Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
Tactic: rw [← mul_one (Module.finrank (R ⧸ p) (S ⧸ q)),
    ← Module.finrank_of_bijective_algebraMap (bijective_algebraMap_quotient_residueField q),
    Module.finrank_mul_finrank, ← Module.finrank_mul_finrank (R ⧸ p) p.ResidueField q.ResidueField,
    Module.finrank_of_bijective_algebraMap (bijective_algebraMap_quotient_residueField p), one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.LiesOver p
inst_4 : p.IsMaximal
inst_5 : q.IsMaximal
this_1 : Field (R ⧸ p) := Quotient.field p
this_2 : Field (S ⧸ q) := Quotient.field q
this_3 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ (S ⧸ q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⧸ q) q.ResidueField)
    (algebraMap (R ⧸ p) (S ⧸ q))
g : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ p.ResidueField _ _ Semiring.toNonAssocSemiring _ (algebraMap p.ResidueField q.ResidueField)
    (algebraMap (R ⧸ p) p.ResidueField)
h : f = g
this_4 : Algebra.{u_1, u_2} (R ⧸ p) q.ResidueField := f.toAlgebra
this_5 : IsScalarTower.{u_1, u_2, u_2} (R ⧸ p) (S ⧸ q) q.ResidueField
this : IsScalarTower.{u_1, u_1, u_2} (R ⧸ p) p.ResidueField q.ResidueField
rw : Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) * 1 = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
rw₁ :
  Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) * Module.finrank.{u_2, u_2} (S ⧸ q) q.ResidueField =
    Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
rw₂ : Module.finrank.{u_1, u_2} (R ⧸ p) q.ResidueField = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
rw₃ :
  Module.finrank.{u_1, u_1} (R ⧸ p) p.ResidueField * Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField =
    Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
⊢ Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
have rw₄ : 1 * Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
Tactic: rw [← mul_one (Module.finrank (R ⧸ p) (S ⧸ q)),
    ← Module.finrank_of_bijective_algebraMap (bijective_algebraMap_quotient_residueField q),
    Module.finrank_mul_finrank, ← Module.finrank_mul_finrank (R ⧸ p) p.ResidueField q.ResidueField,
    Module.finrank_of_bijective_algebraMap (bijective_algebraMap_quotient_residueField p), one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.LiesOver p
inst_4 : p.IsMaximal
inst_5 : q.IsMaximal
this_1 : Field (R ⧸ p) := Quotient.field p
this_2 : Field (S ⧸ q) := Quotient.field q
this_3 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ (S ⧸ q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⧸ q) q.ResidueField)
    (algebraMap (R ⧸ p) (S ⧸ q))
g : RingHom.{u_1, u_2} (R ⧸ p) q.ResidueField :=
  @RingHom.comp _ p.ResidueField _ _ Semiring.toNonAssocSemiring _ (algebraMap p.ResidueField q.ResidueField)
    (algebraMap (R ⧸ p) p.ResidueField)
h : f = g
this_4 : Algebra.{u_1, u_2} (R ⧸ p) q.ResidueField := f.toAlgebra
this_5 : IsScalarTower.{u_1, u_2, u_2} (R ⧸ p) (S ⧸ q) q.ResidueField
this : IsScalarTower.{u_1, u_1, u_2} (R ⧸ p) p.ResidueField q.ResidueField
rw : Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) * 1 = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
rw₁ :
  Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) * Module.finrank.{u_2, u_2} (S ⧸ q) q.ResidueField =
    Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
rw₂ : Module.finrank.{u_1, u_2} (R ⧸ p) q.ResidueField = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
rw₃ :
  Module.finrank.{u_1, u_1} (R ⧸ p) p.ResidueField * Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField =
    Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
rw₄ :
  1 * Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
⊢ Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
have rw₅ : Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
Tactic: rw [← mul_one (Module.finrank (R ⧸ p) (S ⧸ q)),
    ← Module.finrank_of_bijective_algebraMap (bijective_algebraMap_quotient_residueField q),
    Module.finrank_mul_finrank, ← Module.finrank_mul_finrank (R ⧸ p) p.ResidueField q.ResidueField,
    Module.finrank_of_bijective_algebraMap (bijective_algebraMap_quotient_residueField p), one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
⊢ r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S
have pos : ∀ (hr : r.IsPrime), r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S
Tactic: by_cases hr : r.IsPrime
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
pos : ∀ (hr : r.IsPrime), r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S
⊢ r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S
have neg : ∀ (hr : ¬r.IsPrime), r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S
Tactic: by_cases hr : r.IsPrime
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
hr : r.IsPrime
⊢ r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S
have this : q.IsPrime
Tactic: have : q.IsPrime := isPrime_of_liesOver r q
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
hr : r.IsPrime
this : q.IsPrime
⊢ r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S
have this₁ : q.LiesOver (under R r)
Tactic: have : q.LiesOver (r.under R) := LiesOver.tower_bot r q (r.under R)
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
hr : r.IsPrime
this_1 : q.IsPrime
this_2 : q.LiesOver (under R r)
this_3 : Algebra.{u_1, u_3} (Localization.AtPrime (under R r)) (Localization.AtPrime r) :=
  Localization.AtPrime.algebraOfLiesOver (under R r) r
this_4 : Algebra.{u_1, u_2} (Localization.AtPrime (under R r)) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver (under R r) q
this : Algebra.{u_2, u_3} (Localization.AtPrime q) (Localization.AtPrime r) :=
  Localization.AtPrime.algebraOfLiesOver q r
⊢ r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S
have pos : Module.finrank.{u_1, u_2} (ResidueField (under R r)) q.ResidueField *
    Module.finrank.{u_2, u_3} q.ResidueField r.ResidueField =
  Module.finrank.{u_1, u_3} (ResidueField (under R r)) r.ResidueField
Tactic: rw [inertiaDeg'_def, inertiaDeg'_eq (r.under R), inertiaDeg'_eq q, eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
hr : ¬r.IsPrime
⊢ r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S
have neg : 0 = q.inertiaDeg' R * r.inertiaDeg' S
Tactic: rw [inertiaDeg'_of_not_isPrime r R hr, inertiaDeg'_of_not_isPrime r S hr, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
hr : ¬r.IsPrime
neg : 0 = q.inertiaDeg' R * r.inertiaDeg' S
⊢ r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S
have neg₁ : 0 = q.inertiaDeg' R * 0
Tactic: rw [inertiaDeg'_of_not_isPrime r R hr, inertiaDeg'_of_not_isPrime r S hr, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : r.LiesOver q
hr : ¬r.IsPrime
neg : 0 = q.inertiaDeg' R * r.inertiaDeg' S
neg₁ : 0 = q.inertiaDeg' R * 0
⊢ r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S
have neg₂ : Eq (α := ℕ) 0 0
Tactic: rw [inertiaDeg'_of_not_isPrime r R hr, inertiaDeg'_of_not_isPrime r S hr, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.LiesOver p
inst_4 : q.IsPrime
⊢ q.ramificationIdx' R =
    (Module.length.{u_2, u_2} (Localization.AtPrime q)
        (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
          (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p))).toNat
have rw : (Module.length.{u_2, u_2} (Localization.AtPrime q)
      (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
        (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
          (under R q)))).toNat =
  (Module.length.{u_2, u_2} (Localization.AtPrime q)
      (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
        (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p))).toNat
Tactic: rw [ramificationIdx'_def, over_def q p]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : q.LiesOver p
inst_4 : q.IsPrime
rw :
  (Module.length.{u_2, u_2} (Localization.AtPrime q)
        (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
          (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
            (under R q)))).toNat =
    (Module.length.{u_2, u_2} (Localization.AtPrime q)
        (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
          (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p))).toNat
⊢ q.ramificationIdx' R =
    (Module.length.{u_2, u_2} (Localization.AtPrime q)
        (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
          (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) p))).toNat
have rw₁ : (Module.length.{u_2, u_2} (Localization.AtPrime q)
      (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
        (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
          (under R q)))).toNat =
  (Module.length.{u_2, u_2} (Localization.AtPrime q)
      (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
        (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
          (under R q)))).toNat
Tactic: rw [ramificationIdx'_def, over_def q p]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
⊢ p.ramificationIdx q = q.ramificationIdx' R
have this : p.IsPrime
Tactic: have : p.IsPrime := isPrime_of_liesOver q p
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this : p.IsPrime
⊢ p.ramificationIdx q = q.ramificationIdx' R
have hq' : q ≠ ⊥
Tactic: have hq' : q ≠ ⊥ := ne_bot_of_liesOver_of_ne_bot hp q
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this : p.IsPrime
hq' : q ≠ ⊥
⊢ p.ramificationIdx q = q.ramificationIdx' R
have this₁ : q.IsMaximal
Tactic: have : q.IsMaximal := hq.isMaximal hq'
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Ramification (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
q : Ideal S
inst_3 : IsDomain R
inst_4 : IsDedekindDomain S
inst_5 : Module.IsTorsionFree R S
inst_6 : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
this_1 : p.IsPrime
hq' : q ≠ ⊥
this : q.IsMaximal
⊢ p.ramificationIdx q = q.ramificationIdx' R
have hpS : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) p) ⊥
Tactic: have hpS : p.map (algebraMap R S) ≠ ⊥ := map_ne_bot_of_ne_bot hp