awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
inl : radical (0 * b) ∣ radical 0 * radical b
⊢ radical (a * b) ∣ radical a * radical b
have inr : ∀ (ha : a ≠ 0), radical (a * b) ∣ radical a * radical b
Tactic: classical
  obtain rfl | ha := eq_or_ne a 0
  · simp
  obtain rfl | hb := eq_or_ne b 0
  · simp
  nontriviality M
  simp [radical_dvd_iff_primeFactors_subset, primeFactors_mul_eq_union,
    primeFactors_mul_eq_union ha hb, primeFactors_radical]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
inl : radical (0 * b) ∣ radical 0 * radical b
inr inr₁ : ∀ (ha : a ≠ 0), radical (a * b) ∣ radical a * radical b
⊢ radical (a * b) ∣ radical a * radical b
have inr₂ : ∀ (ha : a ≠ 0), radical (a * 0) ∣ radical a * radical 0
Tactic: classical
  obtain rfl | ha := eq_or_ne a 0
  · simp
  obtain rfl | hb := eq_or_ne b 0
  · simp
  nontriviality M
  simp [radical_dvd_iff_primeFactors_subset, primeFactors_mul_eq_union,
    primeFactors_mul_eq_union ha hb, primeFactors_radical]
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
inl : radical (0 * b) ∣ radical 0 * radical b
inr inr₁ : ∀ (ha : a ≠ 0), radical (a * b) ∣ radical a * radical b
inr₂ : ∀ (ha : a ≠ 0), radical (a * 0) ∣ radical a * radical 0
⊢ radical (a * b) ∣ radical a * radical b
have inr₃ : ∀ (ha : a ≠ 0) (hb : b ≠ 0), radical (a * b) ∣ radical a * radical b
Tactic: classical
  obtain rfl | ha := eq_or_ne a 0
  · simp
  obtain rfl | hb := eq_or_ne b 0
  · simp
  nontriviality M
  simp [radical_dvd_iff_primeFactors_subset, primeFactors_mul_eq_union,
    primeFactors_mul_eq_union ha hb, primeFactors_radical]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
inl : radical (0 * b) ∣ radical 0 * radical b
inr inr₁ : ∀ (ha : a ≠ 0), radical (a * b) ∣ radical a * radical b
inr₂ : ∀ (ha : a ≠ 0), radical (a * 0) ∣ radical a * radical 0
inr₃ inr₄ : ∀ (ha : a ≠ 0) (hb : b ≠ 0), radical (a * b) ∣ radical a * radical b
⊢ radical (a * b) ∣ radical a * radical b
have obtain : ∀ (ha : a ≠ 0) (hb : b ≠ 0), Nontrivial M → radical (a * b) ∣ radical a * radical b
Tactic: classical
  obtain rfl | ha := eq_or_ne a 0
  · simp
  obtain rfl | hb := eq_or_ne b 0
  · simp
  nontriviality M
  simp [radical_dvd_iff_primeFactors_subset, primeFactors_mul_eq_union,
    primeFactors_mul_eq_union ha hb, primeFactors_radical]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
i : ι
s : Finset ι
h : i ∉ s
ih : Dvd.dvd.{u_1} (α := M) (radical (∏ i ∈ s, f i)) (∏ i ∈ s, radical (f i))
⊢ Dvd.dvd.{u_1} (α := M) (radical (∏ i ∈ Finset.cons i s h, f i)) (∏ i ∈ Finset.cons i s h, radical (f i))
have cons : radical (f i * ∏ i ∈ s, f i) ∣ radical (f i) * ∏ i ∈ s, radical (f i)
Tactic: simp only [Finset.prod_cons]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
ι : Type u_2
s : Finset ι
f : ι → M
⊢ Dvd.dvd.{u_1} (α := M) (radical (∏ i ∈ s, f i)) (∏ i ∈ s, radical (f i))
have empty : Dvd.dvd.{u_1} (α := M) (radical (∏ i ∈ ∅, f i)) (∏ i ∈ ∅, radical (f i))
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons i s h ih =>
    simp only [Finset.prod_cons]
    exact radical_mul_dvd.trans (mul_dvd_mul_left _ ih)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
ι : Type u_2
s : Finset ι
f : ι → M
empty : Dvd.dvd.{u_1} (α := M) (radical (∏ i ∈ ∅, f i)) (∏ i ∈ ∅, radical (f i))
⊢ Dvd.dvd.{u_1} (α := M) (radical (∏ i ∈ s, f i)) (∏ i ∈ s, radical (f i))
have cons : ∀ (i : ι) (s : Finset ι) (h : i ∉ s) (ih : Dvd.dvd.{u_1} (α := M) (radical (∏ i ∈ s, f i)) (∏ i ∈ s, radical (f i))),
  Dvd.dvd.{u_1} (α := M) (radical (∏ i ∈ Finset.cons i s h, f i)) (∏ i ∈ Finset.cons i s h, radical (f i))
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons i s h ih =>
    simp only [Finset.prod_cons]
    exact radical_mul_dvd.trans (mul_dvd_mul_left _ ih)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a : E
⊢ radical a * divRadical a = a
have rw : radical a * (a / radical a) = a
Tactic: rw [divRadical, ← EuclideanDomain.mul_div_assoc _ radical_dvd_self,
    mul_div_cancel_left₀ _ radical_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a : E
rw : radical a * (a / radical a) = a
⊢ radical a * divRadical a = a
have rw₁ : radical a * a / radical a = a
Tactic: rw [divRadical, ← EuclideanDomain.mul_div_assoc _ radical_dvd_self,
    mul_div_cancel_left₀ _ radical_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a : E
rw : radical a * (a / radical a) = a
rw₁ : radical a * a / radical a = a
⊢ radical a * divRadical a = a
have rw₂ : a = a
Tactic: rw [divRadical, ← EuclideanDomain.mul_div_assoc _ radical_dvd_self,
    mul_div_cancel_left₀ _ radical_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a : E
⊢ divRadical a * radical a = a
have rw : radical a * divRadical a = a
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (hypothesis)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a : E
ha : a ≠ 0
⊢ divRadical a ≠ 0
have ha₁ : radical a * divRadical a ≠ 0
Tactic: rw [← radical_mul_divRadical (a := a)] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
u : E
hu : IsUnit u
⊢ IsUnit (divRadical u)
have rwa : IsUnit (u / radical u)
Tactic: rwa [divRadical, radical_of_isUnit hu, EuclideanDomain.div_one]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
u : E
hu : IsUnit u
rwa : IsUnit (u / radical u)
⊢ IsUnit (divRadical u)
have rwa₁ : IsUnit (u / 1)
Tactic: rwa [divRadical, radical_of_isUnit hu, EuclideanDomain.div_one]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a x : E
h : radical a * x = a
⊢ x = divRadical a
have apply : x * radical a = a
Tactic: apply EuclideanDomain.eq_div_of_mul_eq_left radical_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ divRadical (a * b) = divRadical a * divRadical b
have symm : divRadical a * divRadical b = divRadical (a * b)
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ divRadical a * divRadical b = divRadical (a * b)
have h : radical (a * b) * (divRadical a * divRadical b) = a * b
Tactic: apply eq_divRadical
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ radical (a * b) * (divRadical a * divRadical b) = a * b
have h : radical a * radical b * (divRadical a * divRadical b) = a * b
Tactic: rw [UniqueFactorizationMonoid.radical_mul hab.isRelPrime]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ radical a * radical b * (divRadical a * divRadical b) = a * b
have h : radical a * divRadical a * (radical b * divRadical b) = a * b
Tactic: rw [mul_mul_mul_comm, radical_mul_divRadical, radical_mul_divRadical]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
h : radical a * divRadical a * (radical b * divRadical b) = a * b
⊢ radical a * radical b * (divRadical a * divRadical b) = a * b
have h₁ : a * (radical b * divRadical b) = a * b
Tactic: rw [mul_mul_mul_comm, radical_mul_divRadical, radical_mul_divRadical]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
h : radical a * divRadical a * (radical b * divRadical b) = a * b
h₁ : a * (radical b * divRadical b) = a * b
⊢ radical a * radical b * (divRadical a * divRadical b) = a * b
have h₂ : a * b = a * b
Tactic: rw [mul_mul_mul_comm, radical_mul_divRadical, radical_mul_divRadical]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (hypothesis)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a b : E
h : IsCoprime a b
⊢ IsCoprime (EuclideanDomain.divRadical a) (EuclideanDomain.divRadical b)
have h₁ : IsCoprime (radical a * EuclideanDomain.divRadical a) b
Tactic: rw [← radical_mul_divRadical (a := a)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (hypothesis)
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a b : E
h : IsCoprime (radical a * EuclideanDomain.divRadical a) b
⊢ IsCoprime (EuclideanDomain.divRadical a) (EuclideanDomain.divRadical b)
have h₁ : IsCoprime (radical a * EuclideanDomain.divRadical a) (radical b * EuclideanDomain.divRadical b)
Tactic: rw [← radical_mul_divRadical (a := b)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
⊢ primeFactors = Nat.primeFactors
have h : ∀ (n : ℕ), primeFactors n = n.primeFactors
Tactic: ext n : 1
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
n : ℕ
⊢ primeFactors n = n.primeFactors
have h : (↑n.primeFactorsList : Multiset ℕ).toFinset = n.primeFactorsList.toFinset
Tactic: rw [primeFactors, Nat.factors_eq, Nat.primeFactors]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (hypothesis)
Goal:
n : ℕ
⊢ 1 < radical n ↔ 1 < n
have pp : ∀ (p : ℕ) (h : p ∈ n.primeFactors), 1 ≤ p
Tactic: have pp (p) (h : p ∈ n.primeFactors) : 1 ≤ p := pos_of_mem_primeFactors h
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
n : ℕ
pp : ∀ (p : ℕ) (h : p ∈ n.primeFactors), 1 ≤ p
⊢ 1 < radical n ↔ 1 < n
have rw : (∃ x ∈ n.primeFactors, 1 < x) ↔ n.primeFactors.Nonempty
Tactic: rw [radical_eq_prod_primeFactors, ← @nonempty_primeFactors n, Finset.one_lt_prod_iff_of_one_le pp]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
n : ℕ
⊢ radical n = 1 ↔ n ≤ 1
have rw : radical n = 1 ↔ radical n ≤ 1
Tactic: rw [← radical_le_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
z : ℤ
⊢ primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors
have inl : Eq (α := Finset ℤ) (primeFactors 0) (Finset.map Nat.castEmbedding (Int.natAbs 0).primeFactors)
Tactic: obtain rfl | hz := eq_or_ne z 0
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
z : ℤ
inl : Eq (α := Finset ℤ) (primeFactors 0) (Finset.map Nat.castEmbedding (Int.natAbs 0).primeFactors)
⊢ primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors
have inr : ∀ (hz : z ≠ 0), primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors
Tactic: obtain rfl | hz := eq_or_ne z 0
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
z : ℤ
hz : z ≠ 0
⊢ primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors
have inr : ∀ (p : ℤ), p ∈ primeFactors z ↔ Membership.mem (γ := Finset ℤ) (Finset.map Nat.castEmbedding z.natAbs.primeFactors) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
z : ℤ
hz : z ≠ 0
p : ℤ
⊢ p ∈ primeFactors z ↔ Membership.mem (γ := Finset ℤ) (Finset.map Nat.castEmbedding z.natAbs.primeFactors) p
have inr : Prime p ∧ 0 ≤ p ∧ p ∣ z ↔ ∃ a ∈ z.natAbs.primeFactors, Function.Embedding.toFun Nat.castEmbedding a = p
Tactic: rw [mem_primeFactors, mem_normalizedFactors_iff' hz, irreducible_iff_prime,
    Int.nonneg_iff_normalize_eq_self, Finset.mem_map, Function.Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
z : ℤ
hz : z ≠ 0
p : ℤ
⊢ Prime p ∧ 0 ≤ p ∧ p ∣ z ↔ ∃ a ∈ z.natAbs.primeFactors, Function.Embedding.toFun Nat.castEmbedding a = p
have inr : Prime p ∧ 0 ≤ p ∧ p ∣ z →
  ∀ (pp : Prime p) (nnp : 0 ≤ p) (dp : p ∣ z),
    ∃ a ∈ z.natAbs.primeFactors, Function.Embedding.toFun Nat.castEmbedding a = p
Tactic: refine ⟨fun ⟨pp, nnp, dp⟩ ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
z : ℤ
hz : z ≠ 0
p : ℤ
inr :
  Prime p ∧ 0 ≤ p ∧ p ∣ z →
    ∀ (pp : Prime p) (nnp : 0 ≤ p) (dp : p ∣ z),
      ∃ a ∈ z.natAbs.primeFactors, Function.Embedding.toFun Nat.castEmbedding a = p
⊢ Prime p ∧ 0 ≤ p ∧ p ∣ z ↔ ∃ a ∈ z.natAbs.primeFactors, Function.Embedding.toFun Nat.castEmbedding a = p
have inr₁ : ∀ (h : ∃ a ∈ z.natAbs.primeFactors, Function.Embedding.toFun Nat.castEmbedding a = p), Prime p ∧ 0 ≤ p ∧ p ∣ z
Tactic: refine ⟨fun ⟨pp, nnp, dp⟩ ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
z : ℤ
hz : z ≠ 0
p : ℤ
h : Prime p ∧ 0 ≤ p ∧ p ∣ z
pp : Prime p
nnp : 0 ≤ p
dp : p ∣ z
⊢ ∃ a ∈ z.natAbs.primeFactors, Function.Embedding.toFun Nat.castEmbedding a = p
have 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 : ℤ)
Tactic: lift p to ℕ using nnp
Cleared hypotheses: p, h, pp, nnp, dp
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (hypothesis)
Goal:
z : ℤ
hz : z ≠ 0
p : ℕ
h : 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 : ℤ)
have pp₁ : Nat.Prime p
Tactic: rw [← Nat.prime_iff_prime_int] at pp
Cleared hypotheses: pp, dp
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (hypothesis)
Goal:
z : ℤ
hz : z ≠ 0
p : ℕ
h : Prime (M := ℤ) (↑p : ℤ) ∧ LE.le (α := ℤ) 0 (↑p : ℤ) ∧ (↑p : ℤ) ∣ z
pp : Nat.Prime p
dp : (↑p : ℤ) ∣ z
⊢ ∃ a ∈ z.natAbs.primeFactors, Eq (α := ℤ) (Function.Embedding.toFun Nat.castEmbedding a) (↑p : ℤ)
have dp₁ : p ∣ z.natAbs
Tactic: rw [Int.natCast_dvd] at dp
Cleared hypotheses: dp
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (hypothesis)
Goal:
z : ℤ
hz : z ≠ 0
p : ℤ
h : ∃ a ∈ z.natAbs.primeFactors, Function.Embedding.toFun Nat.castEmbedding a = p
⊢ Prime p ∧ 0 ≤ p ∧ p ∣ z
have h₁ : ∃ (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
z : ℤ
hz : z ≠ 0
p : ℤ
h : ∃ (a : ℕ), (Nat.Prime a ∧ a ∣ z.natAbs ∧ z.natAbs ≠ 0) ∧ (↑a : ℤ) = p
⊢ Prime p ∧ 0 ≤ p ∧ p ∣ z
have inr : ∀ (n : ℕ) (pn : Nat.Prime n) (dn : n ∣ z.natAbs), Prime (M := ℤ) (↑n : ℤ) ∧ LE.le (α := ℤ) 0 (↑n : ℤ) ∧ (↑n : ℤ) ∣ z
Tactic: obtain ⟨n, ⟨pn, dn, -⟩, rfl⟩ := h
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
z : ℤ
hz : z ≠ 0
n : ℕ
pn : Nat.Prime n
dn : n ∣ z.natAbs
⊢ Prime (M := ℤ) (↑n : ℤ) ∧ LE.le (α := ℤ) 0 (↑n : ℤ) ∧ (↑n : ℤ) ∣ z
have inr : Nat.Prime n ∧ LE.le (α := ℤ) 0 (↑n : ℤ) ∧ n ∣ z.natAbs
Tactic: rw [Int.natCast_dvd, ← Nat.prime_iff_prime_int]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
z : ℤ
⊢ (↑(radical z.natAbs) : ℤ) = radical z
have rw : (↑(∏ p ∈ z.natAbs.primeFactors, p) : ℤ) = (primeFactors z).prod id
Tactic: rw [Nat.radical_eq_prod_primeFactors, radical]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
z : ℤ
⊢ radical z = (↑(∏ p ∈ z.natAbs.primeFactors, p) : ℤ)
have rw : Eq (α := ℤ) (↑(radical z.natAbs) : ℤ) (↑(∏ p ∈ z.natAbs.primeFactors, p) : ℤ)
Tactic: rw [← radical_natAbs_eq_radical, Nat.radical_eq_prod_primeFactors]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
z : ℤ
rw : Eq (α := ℤ) (↑(radical z.natAbs) : ℤ) (↑(∏ p ∈ z.natAbs.primeFactors, p) : ℤ)
⊢ radical z = (↑(∏ p ∈ z.natAbs.primeFactors, p) : ℤ)
have rw₁ : Eq (α := ℤ) (↑(∏ p ∈ z.natAbs.primeFactors, p) : ℤ) (↑(∏ p ∈ z.natAbs.primeFactors, p) : ℤ)
Tactic: rw [← radical_natAbs_eq_radical, Nat.radical_eq_prod_primeFactors]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
z : ℤ
⊢ 0 < radical z
have rw : 0 < radical z.natAbs
Tactic: rw [← radical_natAbs_eq_radical, natCast_pos]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
z : ℤ
⊢ 1 < radical z ↔ 1 < z.natAbs
have rw : 1 < radical z.natAbs ↔ 1 < z.natAbs
Tactic: rw [← radical_natAbs_eq_radical, Nat.one_lt_cast]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.NatInt (goal)
Goal:
z : ℤ
⊢ radical z = 1 ↔ z.natAbs ≤ 1
have rw : radical z = 1 ↔ radical z ≤ 1
Tactic: rw [← radical_le_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (goal)
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
⊢ q.inertiaDeg' R = Module.finrank.{u_2, u_1} (ResidueField (under R q)) q.ResidueField
have h : inst_3 = Localization.AtPrime.algebraOfLiesOver (under R q) q
Tactic: convert! dif_pos hq
-- Lean 4 proof step from Mathlib.RingTheory.RamificationInertia.Inertia (goal)
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 < q.inertiaDeg' R
have rw : 0 < Module.finrank.{u_2, u_1} (ResidueField (under R q)) q.ResidueField
Tactic: rw [inertiaDeg'_def]
-- 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 : 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
⊢ q.inertiaDeg' R = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
have this : p = under R q
Tactic: have := Ideal.over_def q p
-- 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 : 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
⊢ q.inertiaDeg' R = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
have 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
Tactic: subst this
Cleared hypotheses: p, inst_3, inst_5, inst_6, inst_7, this
-- 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 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
⊢ p.inertiaDeg q = q.inertiaDeg' R
have rw : Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
Tactic: rw [inertiaDeg'_eq p q, inertiaDeg_algebraMap]
-- 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 : 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
have 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)
Tactic: ext
-- 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 : 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)
⊢ Module.finrank.{u_1, u_2} (R ⧸ p) (S ⧸ q) = Module.finrank.{u_1, u_2} p.ResidueField q.ResidueField
have h : f = g
Tactic: have h : f = g := by ext; simp [f, g, ← IsScalarTower.algebraMap_apply]