-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem gcd_eq_gcd_filter_ne_zero [DecidablePred fun x : β ↦ f x = 0] :
    s.gcd f = (s.filter fun x ↦ f x ≠ 0).gcd f

Proof state:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ α

Tactic:
exact (gcd (filter (fun x => (f x ≠ 0)) s) f)

Result:
no goals

Proof state:
case refine_2.refine_1
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ (filter (fun x => f x = 0) ∅).gcd f = 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ s.gcd f = (filter (fun x => f x ≠ 0) s).gcd f

Tactic:
trans ((s.filter fun x ↦ f x = 0) ∪ s.filter fun x ↦ (f x ≠ 0)).gcd f

Result:
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ s.gcd f = (filter (fun x => f x = 0) s ∪ filter (fun x => f x ≠ 0) s).gcd f

α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ (filter (fun x => f x = 0) s ∪ filter (fun x => f x ≠ 0) s).gcd f = (filter (fun x => f x ≠ 0) s).gcd f

Proof state:
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd ((filter (fun x => f x = 0) s).gcd f) ((filter (fun x => f x ≠ 0) s).gcd f) =
    (filter (fun x => f x ≠ 0) s).gcd f

Tactic:
refine Eq.trans (?_ : _ = GCDMonoid.gcd (0 : α) ?_) (?_ : GCDMonoid.gcd (0 : α) _ = _)

Result:
case refine_1
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ α

case refine_2
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd ((filter (fun x => f x = 0) s).gcd f) ((filter (fun x => f x ≠ 0) s).gcd f) = GCDMonoid.gcd 0 ?refine_1

case refine_3
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd 0 ?refine_1 = (filter (fun x => f x ≠ 0) s).gcd f

Proof state:
case refine_2.refine_2
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : a ∉ s
h : (filter (fun x => f x = 0) s).gcd f = 0
⊢ (if f a = 0 then insert a (filter (fun x => f x = 0) s) else filter (fun x => f x = 0) s).gcd f = 0

Tactic:
split_ifs with h1 <;> simp [h, h1]

Result:
no goals

Proof state:
case refine_3
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd 0 ((filter (fun x => f x ≠ 0) s).gcd f) = (filter (fun x => f x ≠ 0) s).gcd f

Tactic:
simp only [gcd_zero_left, normalize_gcd]

Result:
no goals

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd ((filter (fun x => f x = 0) s).gcd f) ((filter (fun x => f x ≠ 0) s).gcd f) =
    GCDMonoid.gcd 0 ((filter (fun x => f x ≠ 0) s).gcd f)

Tactic:
refine congr (congr rfl <| s.induction_on ?_ ?_) (by simp)

Result:
case refine_2.refine_1
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ (filter (fun x => f x = 0) ∅).gcd f = 0

case refine_2.refine_2
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ ∀ ⦃a : β⦄ {s : Finset β},
    a ∉ s → (filter (fun x => f x = 0) s).gcd f = 0 → (filter (fun x => f x = 0) (insert a s)).gcd f = 0

Proof state:
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ (filter (fun x => f x ≠ 0) s).gcd f = (filter (fun x => f x ≠ 0) s).gcd f

Tactic:
simp

Result:
no goals

Proof state:
case refine_2.refine_2
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : a ∉ s
h : (filter (fun x => f x = 0) s).gcd f = 0
⊢ (filter (fun x => f x = 0) (insert a s)).gcd f = 0

Tactic:
rw [filter_insert]

Result:
case refine_2.refine_2
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : a ∉ s
h : (filter (fun x => f x = 0) s).gcd f = 0
⊢ (if f a = 0 then insert a (filter (fun x => f x = 0) s) else filter (fun x => f x = 0) s).gcd f = 0

Proof state:
case refine_2.refine_2
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ ∀ ⦃a : β⦄ {s : Finset β},
    a ∉ s → (filter (fun x => f x = 0) s).gcd f = 0 → (filter (fun x => f x = 0) (insert a s)).gcd f = 0

Tactic:
intro a s _ h

Result:
case refine_2.refine_2
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s✝ : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
a : β
s : Finset β
a✝ : a ∉ s
h : (filter (fun x => f x = 0) s).gcd f = 0
⊢ (filter (fun x => f x = 0) (insert a s)).gcd f = 0

Proof state:
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ (filter (fun x => f x = 0) s ∪ filter (fun x => f x ≠ 0) s).gcd f = (filter (fun x => f x ≠ 0) s).gcd f

Tactic:
rw [gcd_union]

Result:
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ GCDMonoid.gcd ((filter (fun x => f x = 0) s).gcd f) ((filter (fun x => f x ≠ 0) s).gcd f) =
    (filter (fun x => f x ≠ 0) s).gcd f

Proof state:
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x => f x = 0
⊢ s.gcd f = (filter (fun x => f x = 0) s ∪ filter (fun x => f x ≠ 0) s).gcd f

Tactic:
rw [filter_union_filter_neg_eq]

Result:
no goals