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

case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ s → x = 0) → gcd s = 0
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ gcd s = 0 ↔ ∀ (x : α), x ∈ s → x = 0
constructor
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : gcd s = 0
x : α
hx : x ∈ s
⊢ x = 0
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ gcd s = 0 → ∀ (x : α), x ∈ s → x = 0
intro h x hx
case mp.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : gcd s = 0
x : α
hx : x ∈ s
⊢ 0 ∣ x
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : gcd s = 0
x : α
hx : x ∈ s
⊢ x = 0
apply eq_zero_of_zero_dvd
case mp.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : gcd s = 0
x : α
hx : x ∈ s
⊢ gcd s ∣ x
case mp.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : gcd s = 0
x : α
hx : x ∈ s
⊢ 0 ∣ x
rw [← h]
no goals
case mp.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : gcd s = 0
x : α
hx : x ∈ s
⊢ gcd s ∣ x
apply gcd_dvd hx
case mpr.refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ 0 → x = 0) → gcd 0 = 0

case mpr.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((∀ (x : α), x ∈ s → x = 0) → gcd s = 0) → (∀ (x : α), x ∈ a ::ₘ s → x = 0) → gcd (a ::ₘ s) = 0
case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ s → x = 0) → gcd s = 0
refine' s.induction_on _ _
case mpr.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
sgcd : (∀ (x : α), x ∈ s → x = 0) → gcd s = 0
h : ∀ (x : α), x ∈ a ::ₘ s → x = 0
⊢ gcd (a ::ₘ s) = 0
case mpr.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((∀ (x : α), x ∈ s → x = 0) → gcd s = 0) → (∀ (x : α), x ∈ a ::ₘ s → x = 0) → gcd (a ::ₘ s) = 0
intro a s sgcd h
no goals
case mpr.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
sgcd : (∀ (x : α), x ∈ s → x = 0) → gcd s = 0
h : ∀ (x : α), x ∈ a ::ₘ s → x = 0
⊢ gcd (a ::ₘ s) = 0
simp [h a (mem_cons_self a s), sgcd fun x hx ↦ h x (mem_cons_of_mem hx)]
no goals
case mpr.refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ 0 → x = 0) → gcd 0 = 0
simp