α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd s f = gcd (filter (fun x => f x = 0) s ∪ filter (fun x => f x ≠ 0) s) f

α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd (filter (fun x => f x = 0) s ∪ filter (fun x => f x ≠ 0) s) f = gcd (filter (fun x => f x ≠ 0) s) f
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd s f = gcd (filter (fun x => f x ≠ 0) s) f
trans ((s.filter fun x ↦ f x = 0) ∪ s.filter fun x ↦ (f x ≠ 0)).gcd f
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd (gcd (filter (fun x => f x = 0) s) f) (gcd (filter (fun x => f x ≠ 0) s) f) =
    gcd (filter (fun x => f x ≠ 0) s) f
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd (filter (fun x => f x = 0) s ∪ filter (fun x => f x ≠ 0) s) f = gcd (filter (fun x => f x ≠ 0) s) f
rw [gcd_union]
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ α

case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd (gcd (filter (fun x => f x = 0) s) f) (gcd (filter (fun x => f x ≠ 0) s) f) = GCDMonoid.gcd 0 ?refine'_1

case refine'_3
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd 0 ?refine'_1 = gcd (filter (fun x => f x ≠ 0) s) f
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd (gcd (filter (fun x => f x = 0) s) f) (gcd (filter (fun x => f x ≠ 0) s) f) =
    gcd (filter (fun x => f x ≠ 0) s) f
refine' Eq.trans (_ : _ = GCDMonoid.gcd (0 : α) _) (_ : GCDMonoid.gcd (0 : α) _ = _)
no goals
case refine'_3
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd 0 (gcd (filter (fun x => f x ≠ 0) s) f) = gcd (filter (fun x => f x ≠ 0) s) f
simp only [gcd_zero_left, normalize_gcd]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd s f = gcd (filter (fun x => f x = 0) s ∪ filter (fun x => f x ≠ 0) s) f
rw [filter_union_filter_neg_eq]
no goals
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ α
exact (gcd (filter (fun x => (f x ≠ 0)) s) f)
case refine'_2.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd (filter (fun x => f x = 0) ∅) f = 0

case refine'_2.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ ∀ ⦃a : β⦄ {s : Finset β},
    ¬a ∈ s → gcd (filter (fun x => f x = 0) s) f = 0 → gcd (filter (fun x => f x = 0) (insert a s)) f = 0
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd (gcd (filter (fun x => f x = 0) s) f) (gcd (filter (fun x => f x ≠ 0) s) f) =
    GCDMonoid.gcd 0 (gcd (filter (fun x => f x ≠ 0) s) f)
refine' congr (congr rfl <| s.induction_on _ _) (by simp)
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd (filter (fun x => f x ≠ 0) s) f = gcd (filter (fun x => f x ≠ 0) s) f
simp
no goals
case refine'_2.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ gcd (filter (fun x => f x = 0) ∅) f = 0
simp
case refine'_2.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : ¬a ∈ s
h : gcd (filter (fun x => f x = 0) s) f = 0
⊢ gcd (filter (fun x => f x = 0) (insert a s)) f = 0
case refine'_2.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ ∀ ⦃a : β⦄ {s : Finset β},
    ¬a ∈ s → gcd (filter (fun x => f x = 0) s) f = 0 → gcd (filter (fun x => f x = 0) (insert a s)) f = 0
intro a s _ h
case refine'_2.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : ¬a ∈ s
h : gcd (filter (fun x => f x = 0) s) f = 0
⊢ gcd (if f a = 0 then insert a (filter (fun x => f x = 0) s) else filter (fun x => f x = 0) s) f = 0
case refine'_2.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : ¬a ∈ s
h : gcd (filter (fun x => f x = 0) s) f = 0
⊢ gcd (filter (fun x => f x = 0) (insert a s)) f = 0
rw [filter_insert]
no goals
case refine'_2.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.22138
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ s₁ s₂ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : ¬a ∈ s
h : gcd (filter (fun x => f x = 0) s) f = 0
⊢ gcd (if f a = 0 then insert a (filter (fun x => f x = 0) s) else filter (fun x => f x = 0) s) f = 0
split_ifs with h1 <;> simp [h, h1]