no goals
α : Type u_3
β : Type u_1
γ : Type u_2
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ gcd (image g s) f = gcd s (f ∘ g)
classical induction' s using Finset.induction with c s _ ih <;> simp [*]
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ gcd (image g s) f = gcd s (f ∘ g)
induction' s using Finset.induction with c s _ ih <;> simp [*]