-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem gcd_eq_zero_iff (s : Multiset α) : s.gcd = 0 ↔ ∀ x : α, x ∈ s → x = 0

Proof state:
case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ x ∈ s, x = 0) → s.gcd = 0

Tactic:
refine s.induction_on ?_ ?_

Result:
case mpr.refine_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ x ∈ 0, x = 0) → gcd 0 = 0

case mpr.refine_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ ∀ (a : α) (s : Multiset α), ((∀ x ∈ s, x = 0) → s.gcd = 0) → (∀ x ∈ a ::ₘ s, x = 0) → (a ::ₘ s).gcd = 0

Proof state:
case mpr.refine_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
sgcd : (∀ x ∈ s, x = 0) → s.gcd = 0
h : ∀ x ∈ a ::ₘ s, x = 0
⊢ (a ::ₘ s).gcd = 0

Tactic:
simp [h a (mem_cons_self a s), sgcd fun x hx ↦ h x (mem_cons_of_mem hx)]

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd = 0 → ∀ x ∈ s, x = 0

Tactic:
intro h x hx

Result:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
⊢ x = 0

Proof state:
case mp.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
⊢ 0 ∣ x

Tactic:
rw [← h]

Result:
case mp.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
⊢ s.gcd ∣ x

Proof state:
case mpr.refine_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ ∀ (a : α) (s : Multiset α), ((∀ x ∈ s, x = 0) → s.gcd = 0) → (∀ x ∈ a ::ₘ s, x = 0) → (a ::ₘ s).gcd = 0

Tactic:
intro a s sgcd h

Result:
case mpr.refine_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
sgcd : (∀ x ∈ s, x = 0) → s.gcd = 0
h : ∀ x ∈ a ::ₘ s, x = 0
⊢ (a ::ₘ s).gcd = 0

Proof state:
case mpr.refine_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ x ∈ 0, x = 0) → gcd 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case mp.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
⊢ s.gcd ∣ x

Tactic:
apply gcd_dvd hx

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd = 0 ↔ ∀ x ∈ s, x = 0

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd = 0 → ∀ x ∈ s, x = 0

case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ x ∈ s, x = 0) → s.gcd = 0

Proof state:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
⊢ x = 0

Tactic:
apply eq_zero_of_zero_dvd

Result:
case mp.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
⊢ 0 ∣ x