-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem gcd_eq_zero_iff : s.gcd f = 0 ↔ ∀ x : β, x ∈ s → f x = 0

Proof state:
case mp
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ Multiset.map f s.val, x = 0
⊢ ∀ x ∈ s, f x = 0

Tactic:
intro b bs

Result:
case mp
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ Multiset.map f s.val, x = 0
b : β
bs : b ∈ s
⊢ f b = 0

Proof state:
case mpr
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ s, f x = 0
a : α
as : a ∈ Multiset.map f s.val
⊢ a = 0

Tactic:
rw [Multiset.mem_map] at as

Result:
case mpr
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ s, f x = 0
a : α
as : ∃ a_1 ∈ s.val, f a_1 = a
⊢ a = 0

Proof state:
case mpr
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ s, f x = 0
a : α
as : ∃ a_1 ∈ s.val, f a_1 = a
⊢ a = 0

Tactic:
rcases as with ⟨b, ⟨bs, rfl⟩⟩

Result:
case mpr.intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ s, f x = 0
b : β
bs : b ∈ s.val
⊢ f b = 0

Proof state:
case mp
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ Multiset.map f s.val, x = 0
b : β
bs : b ∈ s
⊢ f b = 0

Tactic:
apply h (f b)

Result:
case mp
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ Multiset.map f s.val, x = 0
b : β
bs : b ∈ s
⊢ f b ∈ Multiset.map f s.val

Proof state:
case mp
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ Multiset.map f s.val, x = 0
b : β
bs : b ∈ s
⊢ ∃ a ∈ s.val, f a = f b

Tactic:
use b

Result:
case h
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ Multiset.map f s.val, x = 0
b : β
bs : b ∈ s
⊢ b ∈ s.val ∧ f b = f b

Proof state:
case mpr
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ s, f x = 0
⊢ ∀ x ∈ Multiset.map f s.val, x = 0

Tactic:
intro a as

Result:
case mpr
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ s, f x = 0
a : α
as : a ∈ Multiset.map f s.val
⊢ a = 0

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ Multiset.map f s.val, x = 0
b : β
bs : b ∈ s
⊢ b ∈ s.val ∧ f b = f b

Tactic:
simp only [mem_def.1 bs, eq_self_iff_true, and_self]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ s.gcd f = 0 ↔ ∀ x ∈ s, f x = 0

Tactic:
rw [gcd_def, Multiset.gcd_eq_zero_iff]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ (∀ x ∈ Multiset.map f s.val, x = 0) ↔ ∀ x ∈ s, f x = 0

Proof state:
case mpr.intro.intro
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ s, f x = 0
b : β
bs : b ∈ s.val
⊢ f b = 0

Tactic:
apply h b (mem_def.1 bs)

Result:
no goals

Proof state:
case mp
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ Multiset.map f s.val, x = 0
b : β
bs : b ∈ s
⊢ f b ∈ Multiset.map f s.val

Tactic:
simp only [Multiset.mem_map, mem_def.1 bs]

Result:
case mp
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ Multiset.map f s.val, x = 0
b : β
bs : b ∈ s
⊢ ∃ a ∈ s.val, f a = f b

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ (∀ x ∈ Multiset.map f s.val, x = 0) ↔ ∀ x ∈ s, f x = 0

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ Multiset.map f s.val, x = 0
⊢ ∀ x ∈ s, f x = 0

case mpr
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
h : ∀ x ∈ s, f x = 0
⊢ ∀ x ∈ Multiset.map f s.val, x = 0