awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
hz : z ≠ 0
p : ℤ
h : Prime p ∧ 0 ≤ p ∧ p ∣ z
pp : Prime p
nnp : 0 ≤ p
dp : p ∣ z
inr :
  ∀ (p : ℕ),
    Prime (M := ℤ) (↑p : ℤ) ∧ LE.le (α := ℤ) 0 (↑p : ℤ) ∧ (↑p : ℤ) ∣ z →
      ∀ (pp : Prime (M := ℤ) (↑p : ℤ)) (dp : (↑p : ℤ) ∣ z),
        ∃ a ∈ z.natAbs.primeFactors, Eq (α := ℤ) (Function.Embedding.toFun Nat.castEmbedding a) (↑p : ℤ)
⊢ ∃ a ∈ z.natAbs.primeFactors, Function.Embedding.toFun Nat.castEmbedding a = p

Tactic:
lift p to ℕ using nnp
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
hz : z ≠ 0
p : ℕ
h : Prime (M := ℤ) (↑p : ℤ) ∧ LE.le (α := ℤ) 0 (↑p : ℤ) ∧ (↑p : ℤ) ∣ z
pp : Prime (M := ℤ) (↑p : ℤ)
dp : (↑p : ℤ) ∣ z
⊢ Nat.Prime p

Tactic:
rw [← Nat.prime_iff_prime_int] at pp

Premises used: Nat.prime_iff_prime_int
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
hz : z ≠ 0
p : ℕ
h : Prime (M := ℤ) (↑p : ℤ) ∧ LE.le (α := ℤ) 0 (↑p : ℤ) ∧ (↑p : ℤ) ∣ z
pp : Prime (M := ℤ) (↑p : ℤ)
dp : (↑p : ℤ) ∣ z
pp₁ : Nat.Prime p
⊢ (↑p : ℤ) ∣ z

Tactic:
rw [← Nat.prime_iff_prime_int] at pp

Premises used: Nat.prime_iff_prime_int
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
hz : z ≠ 0
p : ℕ
h : Prime (M := ℤ) (↑p : ℤ) ∧ LE.le (α := ℤ) 0 (↑p : ℤ) ∧ (↑p : ℤ) ∣ z
pp : Nat.Prime p
dp : (↑p : ℤ) ∣ z
⊢ p ∣ z.natAbs

Tactic:
rw [Int.natCast_dvd] at dp

Premises used: Int.natCast_dvd
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
hz : z ≠ 0
p : ℕ
h : Prime (M := ℤ) (↑p : ℤ) ∧ LE.le (α := ℤ) 0 (↑p : ℤ) ∧ (↑p : ℤ) ∣ z
pp : Nat.Prime p
dp : p ∣ z.natAbs
⊢ p ∈ z.natAbs.primeFactors

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
hz : z ≠ 0
p : ℕ
h : Prime (M := ℤ) (↑p : ℤ) ∧ LE.le (α := ℤ) 0 (↑p : ℤ) ∧ (↑p : ℤ) ∣ z
pp : Nat.Prime p
dp : p ∣ z.natAbs
⊢ ∃ a ∈ z.natAbs.primeFactors, Eq (α := ℤ) (Function.Embedding.toFun Nat.castEmbedding a) (↑p : ℤ)

Tactic:
exact ⟨p, by simp_all, rfl⟩
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
hz : z ≠ 0
p : ℤ
h : ∃ a ∈ z.natAbs.primeFactors, Function.Embedding.toFun Nat.castEmbedding a = p
⊢ ∃ (a : ℕ), (Nat.Prime a ∧ a ∣ z.natAbs ∧ z.natAbs ≠ 0) ∧ (↑a : ℤ) = p

Tactic:
simp_rw [Nat.mem_primeFactors, Function.Embedding.toFun_eq_coe, Nat.castEmbedding_apply] at h

Premises used: Nat.castEmbedding_apply, Function.Embedding.toFun_eq_coe, Nat.mem_primeFactors
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
hz : z ≠ 0
p : ℤ
h : ∃ (a : ℕ), (Nat.Prime a ∧ a ∣ z.natAbs ∧ z.natAbs ≠ 0) ∧ (↑a : ℤ) = p
inr :
  ∀ (n : ℕ) (pn : Nat.Prime n) (dn : n ∣ z.natAbs), Prime (M := ℤ) (↑n : ℤ) ∧ LE.le (α := ℤ) 0 (↑n : ℤ) ∧ (↑n : ℤ) ∣ z
⊢ Prime p ∧ 0 ≤ p ∧ p ∣ z

Tactic:
obtain ⟨n, ⟨pn, dn, -⟩, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
hz : z ≠ 0
n : ℕ
pn : Nat.Prime n
dn : n ∣ z.natAbs
inr : Nat.Prime n ∧ LE.le (α := ℤ) 0 (↑n : ℤ) ∧ n ∣ z.natAbs
⊢ Prime (M := ℤ) (↑n : ℤ) ∧ LE.le (α := ℤ) 0 (↑n : ℤ) ∧ (↑n : ℤ) ∣ z

Tactic:
rw [Int.natCast_dvd, ← Nat.prime_iff_prime_int]

Premises used: Nat.prime_iff_prime_int, Int.natCast_dvd
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
hz : z ≠ 0
n : ℕ
pn : Nat.Prime n
dn : n ∣ z.natAbs
⊢ LE.le (α := ℤ) 0 (↑n : ℤ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
hz : z ≠ 0
n : ℕ
pn : Nat.Prime n
dn : n ∣ z.natAbs
⊢ Nat.Prime n ∧ LE.le (α := ℤ) 0 (↑n : ℤ) ∧ n ∣ z.natAbs

Tactic:
exact ⟨pn, by simp, dn⟩
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
rw : (↑(∏ p ∈ z.natAbs.primeFactors, p) : ℤ) = (primeFactors z).prod id
⊢ (↑(radical z.natAbs) : ℤ) = radical z

Tactic:
rw [Nat.radical_eq_prod_primeFactors, radical]

Premises used: Nat.radical_eq_prod_primeFactors, UniqueFactorizationMonoid.radical
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
⊢ (↑(∏ p ∈ z.natAbs.primeFactors, p) : ℤ) = (primeFactors z).prod id

Tactic:
simp [primeFactors_eq_primeFactors_natAbs]

Premises used: UniqueFactorizationMonoid.primeFactors_eq_primeFactors_natAbs
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
rw : Eq (α := ℤ) (↑(radical z.natAbs) : ℤ) (↑(∏ p ∈ z.natAbs.primeFactors, p) : ℤ)
rw₁ rw₂ : Eq (α := ℤ) (↑(∏ p ∈ z.natAbs.primeFactors, p) : ℤ) (↑(∏ p ∈ z.natAbs.primeFactors, p) : ℤ)
⊢ radical z = (↑(∏ p ∈ z.natAbs.primeFactors, p) : ℤ)

Tactic:
rw [← radical_natAbs_eq_radical, Nat.radical_eq_prod_primeFactors]

Premises used: Nat.radical_eq_prod_primeFactors, Int.radical_natAbs_eq_radical
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
rw : 0 < radical z.natAbs
⊢ 0 < radical z

Tactic:
rw [← radical_natAbs_eq_radical, natCast_pos]

Premises used: Int.radical_natAbs_eq_radical, Int.natCast_pos
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
⊢ 0 < radical z.natAbs

Tactic:
Nat.radical_pos _

Premises used: Nat.radical_pos
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
⊢ 0 < radical z.natAbs

Tactic:
exact Nat.radical_pos _

Premises used: Nat.radical_pos
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
rw : 1 < radical z.natAbs ↔ 1 < z.natAbs
⊢ 1 < radical z ↔ 1 < z.natAbs

Tactic:
rw [← radical_natAbs_eq_radical, Nat.one_lt_cast]

Premises used: Nat.one_lt_cast, Int.radical_natAbs_eq_radical
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
⊢ 1 < radical z.natAbs ↔ 1 < z.natAbs

Tactic:
Nat.one_lt_radical_iff

Premises used: Nat.one_lt_radical_iff
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
⊢ 1 < radical z.natAbs ↔ 1 < z.natAbs

Tactic:
exact Nat.one_lt_radical_iff

Premises used: Nat.one_lt_radical_iff
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
⊢ 2 ≤ radical z ↔ 2 ≤ z.natAbs

Tactic:
one_lt_radical_iff

Premises used: Int.lt, Int.one_lt_radical_iff, Int.add, Nat.lt
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
⊢ radical z ≤ 1 ↔ z.natAbs ≤ 1

Tactic:
simpa only [not_lt] using one_lt_radical_iff.not

Premises used: Iff.not, not_lt, Int.one_lt_radical_iff
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
rw : radical z = 1 ↔ radical z ≤ 1
⊢ radical z = 1 ↔ z.natAbs ≤ 1

Tactic:
rw [← radical_le_one_iff]

Premises used: Int.radical_le_one_iff
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
⊢ radical z = 1 ↔ radical z ≤ 1

Tactic:
grind [radical_pos z]

Premises used: Int.radical_pos
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
⊢ Eq (α := ℤ) (radical (↑n : ℤ)) (↑(radical n) : ℤ)

Tactic:
simp [Int.radical_eq_prod_primeFactors, Nat.radical_eq_prod_primeFactors]

Premises used: Nat.radical_eq_prod_primeFactors, Int.radical_eq_prod_primeFactors
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
Goal:
S : Type u_1
inst : CommRing S
q : Ideal S
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R S
hq : q.IsPrime
inst_3 : Algebra.{u_2, u_1} (Localization.AtPrime (under R q)) (Localization.AtPrime q)
inst_4 : Localization.AtPrime.IsLiesOverAlgebra (under R q) q
⊢ (if x : q.IsPrime then Module.finrank.{u_2, u_1} (ResidueField (under R q)) q.ResidueField else 0) =
    Module.finrank.{u_2, u_1} (ResidueField (under R q)) q.ResidueField

Tactic:
dif_pos hq

Premises used: dif_pos
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
Goal:
S : Type u_1
inst : CommRing S
q : Ideal S
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R S
hq : q.IsPrime
inst_3 : Algebra.{u_2, u_1} (Localization.AtPrime (under R q)) (Localization.AtPrime q)
inst_4 : Localization.AtPrime.IsLiesOverAlgebra (under R q) q
h : inst_3 = Localization.AtPrime.algebraOfLiesOver (under R q) q
⊢ q.inertiaDeg' R = Module.finrank.{u_2, u_1} (ResidueField (under R q)) q.ResidueField

Tactic:
convert! dif_pos hq

Premises used: dif_pos
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
Goal:
S : Type u_1
inst : CommRing S
q : Ideal S
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R S
hq : q.IsPrime
inst_3 : Algebra.{u_2, u_1} (Localization.AtPrime (under R q)) (Localization.AtPrime q)
inst_4 : Localization.AtPrime.IsLiesOverAlgebra (under R q) q
⊢ inst_3 = Localization.AtPrime.algebraOfLiesOver (under R q) q

Tactic:
simp [Algebra.algebra_ext_iff, Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq]

Premises used: Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq, Algebra.algebra_ext_iff
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
Goal:
S : Type u_1
inst : CommRing S
q : Ideal S
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R S
hq : ¬q.IsPrime
⊢ q.inertiaDeg' R = 0

Tactic:
dif_neg hq

Premises used: dif_neg, Ideal.inertiaDeg'
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
Goal:
S : Type u_1
inst : CommRing S
q : Ideal S
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R S
hq : q.IsPrime
inst_3 : Module.Finite R S
this : Algebra.{u_2, u_1} (Localization.AtPrime (under R q)) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver (under R q) q
rw : 0 < Module.finrank.{u_2, u_1} (ResidueField (under R q)) q.ResidueField
⊢ 0 < q.inertiaDeg' R

Tactic:
rw [inertiaDeg'_def]

Premises used: Ideal.inertiaDeg'_def
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
Goal:
S : Type u_1
inst : CommRing S
q : Ideal S
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra R S
hq : q.IsPrime
inst_3 : Module.Finite R S
this : Algebra.{u_2, u_1} (Localization.AtPrime (under R q)) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver (under R q) q
⊢ 0 < Module.finrank.{u_2, u_1} (ResidueField (under R q)) q.ResidueField

Tactic:
apply Module.finrank_pos

Premises used: Module.finrank_pos
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
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
inst_5 : p.IsPrime
inst_6 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra p q
⊢ p = under R q

Tactic:
have := Ideal.over_def q p
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
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
inst_5 : p.IsPrime
inst_6 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra p q
this : p = under R q
subst :
  ∀ [inst_8 : q.LiesOver (under R q)] [inst_9 : IsPrime (under R q)]
    [inst_10 : Algebra.{u_1, u_2} (Localization.AtPrime (under R q)) (Localization.AtPrime q)]
    [inst_11 : Localization.AtPrime.IsLiesOverAlgebra (under R q) q],
    q.inertiaDeg' R = Module.finrank.{u_1, u_2} (ResidueField (under R q)) q.ResidueField
⊢ q.inertiaDeg' R = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField

Tactic:
subst this
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
q : Ideal S
inst_3 : q.IsPrime
inst_4 : q.LiesOver (under R q)
inst_5 : IsPrime (under R q)
inst_6 : Algebra.{u_1, u_2} (Localization.AtPrime (under R q)) (Localization.AtPrime q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra (under R q) q
⊢ q.inertiaDeg' R = Module.finrank.{u_1, u_2} (ResidueField (under R q)) q.ResidueField

Tactic:
inertiaDeg'_def q R

Premises used: Ideal.inertiaDeg'_def
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
q : Ideal S
inst_3 : q.IsPrime
inst_4 : q.LiesOver (under R q)
inst_5 : IsPrime (under R q)
inst_6 : Algebra.{u_1, u_2} (Localization.AtPrime (under R q)) (Localization.AtPrime q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra (under R q) q
⊢ q.inertiaDeg' R = Module.finrank.{u_1, u_2} (ResidueField (under R q)) q.ResidueField

Tactic:
exact inertiaDeg'_def q R

Premises used: Ideal.inertiaDeg'_def
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
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 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
rw : Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
⊢ p.inertiaDeg q = q.inertiaDeg' R

Tactic:
rw [inertiaDeg'_eq p q, inertiaDeg_algebraMap]

Premises used: Ideal.inertiaDeg_algebraMap, Ideal.inertiaDeg'_eq
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
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 : 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 :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := q.ResidueField) ((f.comp (Quotient.mk p) : (a : R) → q.ResidueField) x : q.ResidueField)
      ((g.comp (Quotient.mk p) : (a : R) → q.ResidueField) x : q.ResidueField)
⊢ f = g

Tactic:
ext
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
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 : 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)
x : R
⊢ Eq.{u_2 + 1} (α := q.ResidueField) ((f.comp (Quotient.mk p) : (a : R) → q.ResidueField) x : q.ResidueField)
    ((g.comp (Quotient.mk p) : (a : R) → q.ResidueField) x : q.ResidueField)

Tactic:
simp [f, g, ← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
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 : 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)
⊢ f = g

Tactic:
have h : f = g := by ext; simp [f, g, ← IsScalarTower.algebraMap_apply]
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
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
⊢ 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
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
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
⊢ 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
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
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
rw₅ rw₆ :
  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

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]

Premises used: Ideal.ResidueField, Module.finrank_of_bijective_algebraMap, HasQuotient.Quotient, Module.finrank_mul_finrank, mul_one, Ideal.bijective_algebraMap_quotient_residueField, one_mul, Module.finrank
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
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
neg : ∀ (hr : ¬r.IsPrime), r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S
⊢ r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S

Tactic:
by_cases hr : r.IsPrime

Premises used: Ideal.IsPrime
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
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
⊢ q.IsPrime

Tactic:
have : q.IsPrime := isPrime_of_liesOver r q
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
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
⊢ q.LiesOver (under R r)

Tactic:
have : q.LiesOver (r.under R) := LiesOver.tower_bot r q (r.under R)
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
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
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
⊢ r.inertiaDeg' R = q.inertiaDeg' R * r.inertiaDeg' S

Tactic:
rw [inertiaDeg'_def, inertiaDeg'_eq (r.under R), inertiaDeg'_eq q, eq_comm]

Premises used: eq_comm, Ideal.inertiaDeg'_eq, Ideal.inertiaDeg'_def, Ideal.under
-- Module: Mathlib.RingTheory.RamificationInertia.Inertia
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
⊢ 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:
apply Module.finrank_mul_finrank

Premises used: Module.finrank_mul_finrank