awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
i : ι
s : Finset ι
his : i ∉ s
ih :
  ∀ (h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f)),
    Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ s, f i)) (∏ i ∈ s, radical (f i))
h : (insert i (↑s : Set ι)).Pairwise (Function.onFun IsRelPrime f)
⊢ i ∉ (↑s : Set ι)

Tactic:
simpa
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
i : ι
s : Finset ι
his : i ∉ s
ih :
  ∀ (h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f)),
    Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ s, f i)) (∏ i ∈ s, radical (f i))
h : (↑(Finset.cons i s his) : Set ι).Pairwise (Function.onFun IsRelPrime f)
⊢ (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f) ∧ ∀ b ∈ (↑s : Set ι), Function.onFun IsRelPrime f i b

Tactic:
rw [Finset.coe_cons,
      Set.pairwise_insert_of_symmetric_of_notMem (symmetric_isRelPrime.comap _) (by simpa)] at h

Premises used: Finset.coe_cons, Symmetric.comap, Set.pairwise_insert_of_symmetric_of_notMem, symmetric_isRelPrime
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
i : ι
s : Finset ι
his : i ∉ s
ih :
  ∀ (h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f)),
    Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ s, f i)) (∏ i ∈ s, radical (f i))
h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f) ∧ ∀ b ∈ (↑s : Set ι), Function.onFun IsRelPrime f i b
cons : IsRelPrime (f i) (∏ i ∈ s, f i)
⊢ radical (f i * ∏ i ∈ s, f i) = radical (f i) * ∏ i ∈ s, radical (f i)

Tactic:
rw [radical_mul, ih h.1]

Premises used: And.left, UniqueFactorizationMonoid.radical_mul
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
i : ι
s : Finset ι
his : i ∉ s
ih :
  ∀ (h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f)),
    Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ s, f i)) (∏ i ∈ s, radical (f i))
h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f) ∧ ∀ b ∈ (↑s : Set ι), Function.onFun IsRelPrime f i b
⊢ IsRelPrime (f i) (∏ i ∈ s, f i)

Tactic:
IsRelPrime.prod_right h.2

Premises used: IsRelPrime.prod_right, And.right
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
i : ι
s : Finset ι
his : i ∉ s
ih :
  ∀ (h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f)),
    Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ s, f i)) (∏ i ∈ s, radical (f i))
h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f) ∧ ∀ b ∈ (↑s : Set ι), Function.onFun IsRelPrime f i b
⊢ IsRelPrime (f i) (∏ i ∈ s, f i)

Tactic:
exact IsRelPrime.prod_right h.2

Premises used: IsRelPrime.prod_right, And.right
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
s : Finset ι
h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f)
empty :
  ∀ (h : (↑∅ : Set ι).Pairwise (Function.onFun IsRelPrime f)),
    Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ ∅, f i)) (∏ i ∈ ∅, radical (f i))
cons :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
    (ih :
      ∀ (h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f)),
        Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ s, f i)) (∏ i ∈ s, radical (f i)))
    (h : (↑(Finset.cons i s his) : Set ι).Pairwise (Function.onFun IsRelPrime f)),
    Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ Finset.cons i s his, f i)) (∏ i ∈ Finset.cons i s his, radical (f i))
⊢ Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ s, f i)) (∏ i ∈ s, radical (f i))

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons i s his ih =>
    simp only [Finset.prod_cons]
    rw [Finset.coe_cons,
      Set.pairwise_insert_of_symmetric_of_notMem (symmetric_isRelPrime.comap _) (by simpa)] at h
    rw [radical_mul, ih h.1]
    exact IsRelPrime.prod_right h.2

Premises used: Finset.coe_cons, Symmetric.comap, Set.pairwise_insert_of_symmetric_of_notMem, Finset.prod_cons, UniqueFactorizationMonoid.radical_mul, symmetric_isRelPrime
-- Module: Mathlib.RingTheory.Radical.Basic
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 : ∀ (ha : a ≠ 0), radical (a * b) ∣ radical a * radical b
⊢ radical (a * b) ∣ radical a * radical b

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
b : M
⊢ radical (0 * b) ∣ radical 0 * radical b

Tactic:
simp
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
inr : radical (a * 0) ∣ radical a * radical 0
inr₁ : ∀ (hb : b ≠ 0), radical (a * b) ∣ radical a * radical b
⊢ radical (a * b) ∣ radical a * radical b

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
⊢ radical (a * 0) ∣ radical a * radical 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
⊢ Nontrivial M

Tactic:
nontriviality M
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
h : Nontrivial M
⊢ radical (a * b) ∣ radical a * radical b

Tactic:
simp [radical_dvd_iff_primeFactors_subset, primeFactors_mul_eq_union,
    primeFactors_mul_eq_union ha hb, primeFactors_radical]

Premises used: UniqueFactorizationMonoid.primeFactors_mul_eq_union, UniqueFactorizationMonoid.primeFactors_radical, UniqueFactorizationMonoid.radical_dvd_iff_primeFactors_subset
-- Module: Mathlib.RingTheory.Radical.Basic
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
obtain : ∀ (ha : a ≠ 0) (hb : b ≠ 0), Nontrivial M → radical (a * b) ∣ radical a * radical b
⊢ 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]

Premises used: UniqueFactorizationMonoid.primeFactors_mul_eq_union, UniqueFactorizationMonoid.primeFactors_radical, eq_or_ne, UniqueFactorizationMonoid.radical_dvd_iff_primeFactors_subset, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
⊢ Dvd.dvd.{u_1} (α := M) (radical (∏ i ∈ ∅, f i)) (∏ i ∈ ∅, radical (f i))

Tactic:
simp
-- Module: Mathlib.RingTheory.Radical.Basic
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))
cons : radical (f i * ∏ i ∈ s, f i) ∣ radical (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:
simp only [Finset.prod_cons]

Premises used: Finset.prod_cons
-- Module: Mathlib.RingTheory.Radical.Basic
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))
⊢ radical (f i * ∏ i ∈ s, f i) ∣ radical (f i) * ∏ i ∈ s, radical (f i)

Tactic:
radical_mul_dvd.trans (mul_dvd_mul_left _ ih)

Premises used: mul_dvd_mul_left, UniqueFactorizationMonoid.radical_mul_dvd, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Radical.Basic
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))
⊢ radical (f i * ∏ i ∈ s, f i) ∣ radical (f i) * ∏ i ∈ s, radical (f i)

Tactic:
exact radical_mul_dvd.trans (mul_dvd_mul_left _ ih)

Premises used: mul_dvd_mul_left, UniqueFactorizationMonoid.radical_mul_dvd, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Radical.Basic
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))
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))
⊢ Dvd.dvd.{u_1} (α := M) (radical (∏ i ∈ s, f i)) (∏ i ∈ s, 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)

Premises used: Finset.prod_cons
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizationMonoid R
inst_2 : UniqueFactorizationMonoid R
a : R
⊢ radical (-a) = radical a

Tactic:
radical_eq_of_associated Associated.rfl.neg_left

Premises used: UniqueFactorizationMonoid.radical_eq_of_associated, Associated.rfl, Associated.neg_left
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizationMonoid R
inst_2 : UniqueFactorizationMonoid R
⊢ Eq.{u_1 + 1} (α := R) (radical (-1)) 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Radical.Basic
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
rw₂ rw₃ : a = a
⊢ radical a * divRadical a = a

Tactic:
rw [divRadical, ← EuclideanDomain.mul_div_assoc _ radical_dvd_self,
    mul_div_cancel_left₀ _ radical_ne_zero]

Premises used: UniqueFactorizationMonoid.radical_ne_zero, mul_div_cancel_left₀, EuclideanDomain.mul_div_assoc, EuclideanDomain.divRadical
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a : E
rw : radical a * divRadical a = a
⊢ divRadical a * radical a = a

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a : E
⊢ radical a * divRadical a = a

Tactic:
radical_mul_divRadical

Premises used: EuclideanDomain.radical_mul_divRadical
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a : E
⊢ radical a * divRadical a = a

Tactic:
exact radical_mul_divRadical

Premises used: EuclideanDomain.radical_mul_divRadical
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a : E
ha : a ≠ 0
⊢ radical a * divRadical a ≠ 0

Tactic:
rw [← radical_mul_divRadical (a := a)] at ha

Premises used: EuclideanDomain.radical_mul_divRadical
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a : E
ha : radical a * divRadical a ≠ 0
⊢ divRadical a ≠ 0

Tactic:
right_ne_zero_of_mul ha

Premises used: right_ne_zero_of_mul
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a : E
ha : radical a * divRadical a ≠ 0
⊢ divRadical a ≠ 0

Tactic:
exact right_ne_zero_of_mul ha

Premises used: right_ne_zero_of_mul
-- Module: Mathlib.RingTheory.Radical.Basic
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)
rwa₁ : IsUnit (u / 1)
rwa₂ rwa₃ rwa₄ rwa₅ : IsUnit u
⊢ IsUnit (divRadical u)

Tactic:
rwa [divRadical, radical_of_isUnit hu, EuclideanDomain.div_one]

Premises used: UniqueFactorizationMonoid.radical_of_isUnit, EuclideanDomain.div_one, EuclideanDomain.divRadical
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a x : E
h : radical a * x = a
apply : x * radical a = a
⊢ x = divRadical a

Tactic:
apply EuclideanDomain.eq_div_of_mul_eq_left radical_ne_zero

Premises used: EuclideanDomain.eq_div_of_mul_eq_left
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a x : E
h : radical a * x = a
rwa rwa₁ rwa₂ rwa₃ : radical a * x = a
⊢ x * radical a = a

Tactic:
rwa [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
symm : divRadical a * divRadical b = divRadical (a * b)
⊢ divRadical (a * b) = divRadical a * divRadical b

Tactic:
symm
-- Module: Mathlib.RingTheory.Radical.Basic
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 * b) * (divRadical a * divRadical b) = a * b
⊢ divRadical a * divRadical b = divRadical (a * b)

Tactic:
apply eq_divRadical

Premises used: EuclideanDomain.eq_divRadical
-- Module: Mathlib.RingTheory.Radical.Basic
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 * radical b * (divRadical a * divRadical b) = a * b
⊢ radical (a * b) * (divRadical a * divRadical b) = a * b

Tactic:
rw [UniqueFactorizationMonoid.radical_mul hab.isRelPrime]

Premises used: IsCoprime.isRelPrime, UniqueFactorizationMonoid.radical_mul
-- Module: Mathlib.RingTheory.Radical.Basic
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
h₂ h₃ : a * b = a * b
⊢ radical a * radical b * (divRadical a * divRadical b) = a * b

Tactic:
rw [mul_mul_mul_comm, radical_mul_divRadical, radical_mul_divRadical]

Premises used: mul_mul_mul_comm, EuclideanDomain.radical_mul_divRadical
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a : E
⊢ divRadical a ∣ a

Tactic:
⟨radical a, divRadical_mul_radical.symm⟩

Premises used: UniqueFactorizationMonoid.radical, Exists.intro, Eq.symm, EuclideanDomain.divRadical_mul_radical
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a b : E
h : IsCoprime a b
⊢ IsCoprime (radical a * EuclideanDomain.divRadical a) b

Tactic:
rw [← radical_mul_divRadical (a := a)] at h

Premises used: EuclideanDomain.radical_mul_divRadical
-- Module: Mathlib.RingTheory.Radical.Basic
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 (radical a * EuclideanDomain.divRadical a) (radical b * EuclideanDomain.divRadical b)

Tactic:
rw [← radical_mul_divRadical (a := b)] at h

Premises used: EuclideanDomain.radical_mul_divRadical
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
E : Type u_1
inst : EuclideanDomain E
inst_1 : NormalizationMonoid E
inst_2 : UniqueFactorizationMonoid E
a b : E
h : IsCoprime (radical a * divRadical a) (radical b * divRadical b)
⊢ IsCoprime (divRadical a) (divRadical b)

Tactic:
h.of_mul_left_right.of_mul_right_right

Premises used: IsCoprime.of_mul_right_right, IsCoprime.of_mul_left_right
-- Module: Mathlib.RingTheory.Radical.Basic
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) (radical b * EuclideanDomain.divRadical b)
⊢ IsCoprime (EuclideanDomain.divRadical a) (EuclideanDomain.divRadical b)

Tactic:
exact h.of_mul_left_right.of_mul_right_right

Premises used: IsCoprime.of_mul_right_right, IsCoprime.of_mul_left_right
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
h : ∀ (n : ℕ), primeFactors n = n.primeFactors
⊢ primeFactors = Nat.primeFactors

Tactic:
ext n : 1
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
h : (↑n.primeFactorsList : Multiset ℕ).toFinset = n.primeFactorsList.toFinset
⊢ primeFactors n = n.primeFactors

Tactic:
rw [primeFactors, Nat.factors_eq, Nat.primeFactors]

Premises used: Nat.factors_eq, UniqueFactorizationMonoid.primeFactors, Nat.primeFactors
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
⊢ (↑n.primeFactorsList : Multiset ℕ).toFinset = n.primeFactorsList.toFinset

Tactic:
List.toFinset_coe _

Premises used: List.toFinset_coe
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
⊢ (↑n.primeFactorsList : Multiset ℕ).toFinset = n.primeFactorsList.toFinset

Tactic:
convert! List.toFinset_coe _

Premises used: List.toFinset_coe
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
⊢ radical n = ∏ p ∈ n.primeFactors, p

Tactic:
simp [radical, primeFactors_eq_natPrimeFactors]

Premises used: UniqueFactorizationMonoid.radical, UniqueFactorizationMonoid.primeFactors_eq_natPrimeFactors
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
⊢ 0 < radical n

Tactic:
pos_of_ne_zero radical_ne_zero

Premises used: UniqueFactorizationMonoid.radical_ne_zero, pos_of_ne_zero
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
⊢ ∀ (p : ℕ) (h : p ∈ n.primeFactors), 1 ≤ p

Tactic:
have pp (p) (h : p ∈ n.primeFactors) : 1 ≤ p := pos_of_mem_primeFactors h
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
pp : ∀ (p : ℕ) (h : p ∈ n.primeFactors), 1 ≤ p
rw : (∃ x ∈ n.primeFactors, 1 < x) ↔ n.primeFactors.Nonempty
⊢ 1 < radical n ↔ 1 < n

Tactic:
rw [radical_eq_prod_primeFactors, ← @nonempty_primeFactors n, Finset.one_lt_prod_iff_of_one_le pp]

Premises used: Nat.radical_eq_prod_primeFactors, Finset.one_lt_prod_iff_of_one_le, Nat.nonempty_primeFactors
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
pp : ∀ (p : ℕ) (h : p ∈ n.primeFactors), 1 ≤ p
⊢ (∃ x ∈ n.primeFactors, 1 < x) ↔ n.primeFactors.Nonempty

Tactic:
⟨fun ⟨p, h⟩ ↦ ⟨p, h.1⟩, fun ⟨p, h⟩ ↦ ⟨p, h, (mem_primeFactors.mp h).1.one_lt⟩⟩

Premises used: Nat.Prime.one_lt, Membership.mem, Exists, _private.0.Nat.one_lt_radical_iff.match_2, _private.0.Nat.one_lt_radical_iff.match_1, And, And.left, And.intro, LT.lt, Iff.intro, Exists.intro, Iff.mp, Finset.Nonempty, Nat.primeFactors, OfNat.ofNat, Nat.mem_primeFactors
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
pp : ∀ (p : ℕ) (h : p ∈ n.primeFactors), 1 ≤ p
⊢ (∃ x ∈ n.primeFactors, 1 < x) ↔ n.primeFactors.Nonempty

Tactic:
exact ⟨fun ⟨p, h⟩ ↦ ⟨p, h.1⟩, fun ⟨p, h⟩ ↦ ⟨p, h, (mem_primeFactors.mp h).1.one_lt⟩⟩
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
⊢ 2 ≤ radical n ↔ 2 ≤ n

Tactic:
one_lt_radical_iff

Premises used: Nat.one_lt_radical_iff, Nat.lt
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
⊢ radical n ≤ 1 ↔ n ≤ 1

Tactic:
simpa only [not_lt] using one_lt_radical_iff.not

Premises used: Iff.not, not_lt, Nat.one_lt_radical_iff
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
rw : radical n = 1 ↔ radical n ≤ 1
⊢ radical n = 1 ↔ n ≤ 1

Tactic:
rw [← radical_le_one_iff]

Premises used: Nat.radical_le_one_iff
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
⊢ radical n = 1 ↔ radical n ≤ 1

Tactic:
grind [radical_pos n]

Premises used: Nat.radical_pos
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
⊢ radical n ≤ n → n ≠ 0

Tactic:
aesop
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
h : n ≠ 0
⊢ 0 < n

Tactic:
lia
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
⊢ n < radical n ↔ n = 0

Tactic:
simpa only [not_le, not_not] using radical_le_self_iff.not

Premises used: not_le, Classical.not_not, Iff.not, Nat.radical_le_self_iff
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
n : ℕ
⊢ LT.lt (α := ℕ) 0 (radical 100)

Tactic:
positivity
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
inl : Eq (α := Finset ℤ) (primeFactors 0) (Finset.map Nat.castEmbedding (Int.natAbs 0).primeFactors)
inr : ∀ (hz : z ≠ 0), primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors
⊢ primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors

Tactic:
obtain rfl | hz := eq_or_ne z 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
⊢ Eq (α := Finset ℤ) (primeFactors 0) (Finset.map Nat.castEmbedding (Int.natAbs 0).primeFactors)

Tactic:
simp
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
hz : z ≠ 0
inr :
  ∀ (p : ℤ), p ∈ primeFactors z ↔ Membership.mem (γ := Finset ℤ) (Finset.map Nat.castEmbedding z.natAbs.primeFactors) p
⊢ primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors

Tactic:
ext p
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
hz : z ≠ 0
p : ℤ
inr : Prime p ∧ 0 ≤ p ∧ p ∣ z ↔ ∃ a ∈ z.natAbs.primeFactors, Function.Embedding.toFun Nat.castEmbedding a = p
⊢ p ∈ primeFactors z ↔ Membership.mem (γ := Finset ℤ) (Finset.map Nat.castEmbedding z.natAbs.primeFactors) 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]

Premises used: UniqueFactorizationMonoid.mem_primeFactors, Function.Embedding.coeFn_mk, UniqueFactorizationMonoid.mem_normalizedFactors_iff', Finset.mem_map, irreducible_iff_prime, Int.nonneg_iff_normalize_eq_self
-- Module: Mathlib.RingTheory.Radical.NatInt
Goal:
z : ℤ
hz : z ≠ 0
p : ℤ
⊢ Prime p ∧ 0 ≤ p ∧ p ∣ z ↔ ∃ a ∈ z.natAbs.primeFactors, Function.Embedding.toFun Nat.castEmbedding a = p

Tactic:
⟨fun ⟨pp, nnp, dp⟩ ↦ ?_, fun h ↦ ?_⟩

Premises used: Membership.mem, Exists, And, _private.0.UniqueFactorizationMonoid.primeFactors_eq_primeFactors_natAbs.match_2, Iff.intro, Int.natAbs, Nat.castEmbedding, Function.Embedding.toFun, Nat.primeFactors, Eq
-- Module: Mathlib.RingTheory.Radical.NatInt
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
inr₁ : ∀ (h : ∃ a ∈ z.natAbs.primeFactors, Function.Embedding.toFun Nat.castEmbedding a = p), Prime p ∧ 0 ≤ p ∧ p ∣ z
⊢ Prime p ∧ 0 ≤ p ∧ p ∣ z ↔ ∃ a ∈ z.natAbs.primeFactors, Function.Embedding.toFun Nat.castEmbedding a = p

Tactic:
refine ⟨fun ⟨pp, nnp, dp⟩ ↦ ?_, fun h ↦ ?_⟩
-- 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
⊢ 0 ≤ p

Tactic:
nnp