no goals
α : Type u_2
β : Type u_1
γ : Type ?u.16783
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ gcd (∅ ∪ s₂) f = GCDMonoid.gcd (gcd ∅ f) (gcd s₂ f)
rw [empty_union, gcd_empty, gcd_zero_left, normalize_gcd]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.16783
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
a : β
s : Finset β
x✝ : ¬a ∈ s
ih : gcd (s ∪ s₂) f = GCDMonoid.gcd (gcd s f) (gcd s₂ f)
⊢ gcd (insert a s ∪ s₂) f = GCDMonoid.gcd (gcd (insert a s) f) (gcd s₂ f)
rw [insert_union, gcd_insert, gcd_insert, ih, gcd_assoc]