α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
⊢ (∀ (x : α), x ∈ Multiset.map f s.val → x = 0) ↔ ∀ (x : β), x ∈ s → f x = 0
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
⊢ gcd s f = 0 ↔ ∀ (x : β), x ∈ s → f x = 0
rw [gcd_def, Multiset.gcd_eq_zero_iff]
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
⊢ ∀ (x : β), x ∈ s → f x = 0

case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
⊢ ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
⊢ (∀ (x : α), x ∈ Multiset.map f s.val → x = 0) ↔ ∀ (x : β), x ∈ s → f x = 0
constructor <;> intro h
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ f b = 0
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
⊢ ∀ (x : β), x ∈ s → f x = 0
intro b bs
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ f b ∈ Multiset.map f s.val
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ f b = 0
apply h (f b)
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ ∃ a, a ∈ s.val ∧ f a = f b
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ f b ∈ Multiset.map f s.val
simp only [Multiset.mem_map, mem_def.1 bs]
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ b ∈ s.val ∧ f b = f b
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ ∃ a, a ∈ s.val ∧ f a = f b
use b
no goals
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
b : β
bs : b ∈ s
⊢ b ∈ s.val ∧ f b = f b
simp only [mem_def.1 bs, eq_self_iff_true, and_self]
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
a : α
as : a ∈ Multiset.map f s.val
⊢ a = 0
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
⊢ ∀ (x : α), x ∈ Multiset.map f s.val → x = 0
intro a as
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
a : α
as : ∃ a_1, a_1 ∈ s.val ∧ f a_1 = a
⊢ a = 0
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
a : α
as : a ∈ Multiset.map f s.val
⊢ a = 0
rw [Multiset.mem_map] at as
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
b : β
bs : b ∈ s.val
⊢ f b = 0
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
a : α
as : ∃ a_1, a_1 ∈ s.val ∧ f a_1 = a
⊢ a = 0
rcases as with ⟨b, ⟨bs, rfl⟩⟩
no goals
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.21349
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
h : ∀ (x : β), x ∈ s → f x = 0
b : β
bs : b ∈ s.val
⊢ f b = 0
apply h b (mem_def.1 bs)