case pos
α : Type u_2
β : Type u_1
γ : Type ?u.3612
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ lcm (insert b s) f = GCDMonoid.lcm (f b) (lcm s f)

case neg
α : Type u_2
β : Type u_1
γ : Type ?u.3612
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : ¬b ∈ s
⊢ lcm (insert b s) f = GCDMonoid.lcm (f b) (lcm s f)
α : Type u_2
β : Type u_1
γ : Type ?u.3612
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
⊢ lcm (insert b s) f = GCDMonoid.lcm (f b) (lcm s f)
by_cases h : b ∈ s
no goals
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.3612
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : ¬b ∈ s
⊢ lcm (insert b s) f = GCDMonoid.lcm (f b) (lcm s f)
apply fold_insert h
no goals
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.3612
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ lcm (insert b s) f = GCDMonoid.lcm (f b) (lcm s f)
rw [insert_eq_of_mem h,
  (lcm_eq_right_iff (f b) (s.lcm f) (Multiset.normalize_lcm (s.1.map f))).2 (dvd_lcm h)]