-- Mathlib/RingTheory/Radical.lean
theorem radical_mul {a b : R} (hc : IsCoprime a b) :
    radical (a * b) = radical a * radical b

Proof state:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
ha : ¬a = 0
hb : ¬b = 0
⊢ ((primeFactors a).disjUnion (primeFactors b) ⋯).prod id = (primeFactors a).prod id * (primeFactors b).prod id

Tactic:
rw [Finset.prod_disjUnion (disjoint_primeFactors hc)]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a : R
ha : ¬a = 0
hc : IsUnit a
⊢ radical (a * 0) = radical a * radical 0

Tactic:
simp only [mul_zero, radical_zero_eq, mul_one, radical_of_isUnit hc]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : R
hc : IsCoprime 0 b
⊢ radical (0 * b) = radical 0 * radical b

Tactic:
rw [isCoprime_zero_left] at hc

Result:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : R
hc : IsUnit b
⊢ radical (0 * b) = radical 0 * radical b

Proof state:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
ha : a = 0
⊢ radical (a * b) = radical a * radical b

Tactic:
subst ha

Result:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : R
hc : IsCoprime 0 b
⊢ radical (0 * b) = radical 0 * radical b

Proof state:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
ha : ¬a = 0
hb : b = 0
⊢ radical (a * b) = radical a * radical b

Tactic:
subst hb

Result:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a : R
ha : ¬a = 0
hc : IsCoprime a 0
⊢ radical (a * 0) = radical a * radical 0

Proof state:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
b : R
hc : IsUnit b
⊢ radical (0 * b) = radical 0 * radical b

Tactic:
simp only [zero_mul, radical_zero_eq, one_mul, radical_of_isUnit hc]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
ha : ¬a = 0
hb : ¬b = 0
⊢ radical (a * b) = radical a * radical b

Tactic:
simp_rw [radical]

Result:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
ha : ¬a = 0
hb : ¬b = 0
⊢ (primeFactors (a * b)).prod id = (primeFactors a).prod id * (primeFactors b).prod id

Proof state:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
ha : ¬a = 0
⊢ radical (a * b) = radical a * radical b

Tactic:
by_cases hb : b = 0

Result:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
ha : ¬a = 0
hb : b = 0
⊢ radical (a * b) = radical a * radical b

case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
ha : ¬a = 0
hb : ¬b = 0
⊢ radical (a * b) = radical a * radical b

Proof state:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
ha : ¬a = 0
hb : ¬b = 0
⊢ (primeFactors (a * b)).prod id = (primeFactors a).prod id * (primeFactors b).prod id

Tactic:
rw [mul_primeFactors_disjUnion ha hb hc]

Result:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
ha : ¬a = 0
hb : ¬b = 0
⊢ ((primeFactors a).disjUnion (primeFactors b) ⋯).prod id = (primeFactors a).prod id * (primeFactors b).prod id

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
⊢ radical (a * b) = radical a * radical b

Tactic:
by_cases ha : a = 0

Result:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
ha : a = 0
⊢ radical (a * b) = radical a * radical b

case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a b : R
hc : IsCoprime a b
ha : ¬a = 0
⊢ radical (a * b) = radical a * radical b

Proof state:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a : R
ha : ¬a = 0
hc : IsCoprime a 0
⊢ radical (a * 0) = radical a * radical 0

Tactic:
rw [isCoprime_zero_right] at hc

Result:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
a : R
ha : ¬a = 0
hc : IsUnit a
⊢ radical (a * 0) = radical a * radical 0