awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
apply : (∀ b ∈ Multiset.map f s.val, b ∣ a) ↔ ∀ b ∈ s, f b ∣ a
⊢ s.lcm f ∣ a ↔ ∀ b ∈ s, f b ∣ a

Tactic:
apply Iff.trans Multiset.lcm_dvd

Premises used: Iff.trans, Multiset.lcm_dvd
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
simp : (∀ (b : α), ∀ x ∈ s.val, f x = b → b ∣ a) ↔ ∀ b ∈ s, f b ∣ a
⊢ (∀ b ∈ Multiset.map f s.val, b ∣ a) ↔ ∀ b ∈ s, f b ∣ a

Tactic:
simp only [Multiset.mem_map, and_imp, exists_imp]

Premises used: and_imp, Multiset.mem_map, exists_imp
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ (b : α), ∀ x ∈ s.val, f x = b → b ∣ a) ↔ ∀ b ∈ s, f b ∣ a

Tactic:
⟨fun k b hb ↦ k _ _ hb rfl, fun k a' b hb h ↦ h ▸ k _ hb⟩

Premises used: Eq.rec, Iff.intro, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ (b : α), ∀ x ∈ s.val, f x = b → b ∣ a) ↔ ∀ b ∈ s, f b ∣ a

Tactic:
exact ⟨fun k b hb ↦ k _ _ hb rfl, fun k a' b hb h ↦ h ▸ k _ hb⟩
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ b ∈ s, f b ∣ a) → s.lcm f ∣ a

Tactic:
lcm_dvd_iff.2

Premises used: Iff.mpr, Finset.lcm_dvd_iff
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
b : β
hb : b ∈ s
⊢ f b ∣ s.lcm f

Tactic:
lcm_dvd_iff.1 dvd_rfl _ hb

Premises used: Iff.mp, dvd_rfl, Finset.lcm_dvd_iff
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq β
b : β
pos : ∀ (h : b ∈ s), (insert b s).lcm f = @GCDMonoid.lcm _ inst _ (f b) (s.lcm f)
neg : ∀ (h : b ∉ s), (insert b s).lcm f = @GCDMonoid.lcm _ inst _ (f b) (s.lcm f)
⊢ (insert b s).lcm f = @GCDMonoid.lcm _ inst _ (f b) (s.lcm f)

Tactic:
by_cases h : b ∈ s
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq β
b : β
h : b ∈ s
pos : s.lcm f = @GCDMonoid.lcm _ inst _ (f b) (s.lcm f)
pos₁ pos₂ : s.lcm f = s.lcm f
⊢ (insert b s).lcm f = @GCDMonoid.lcm _ inst _ (f b) (s.lcm f)

Tactic:
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)]

Premises used: Iff.mpr, Multiset.map, Finset.val, lcm_eq_right_iff, Finset.insert_eq_of_mem, Multiset.normalize_lcm, Finset.lcm, Finset.dvd_lcm
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq β
b : β
h : b ∉ s
⊢ (insert b s).lcm f = @GCDMonoid.lcm _ inst _ (f b) (s.lcm f)

Tactic:
apply fold_insert h

Premises used: Finset.fold_insert
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
b : β
⊢ lcm {b} f = (normalize : (a : α) → α) (f b)

Tactic:
Multiset.lcm_singleton

Premises used: Multiset.map, Multiset.lcm_singleton, List.map, Finset.fold, Multiset.cons, Multiset.ofList, Finset.lcm
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ (normalize : (a : α) → α) (s.lcm f) = s.lcm f

Tactic:
simp [lcm_def]

Premises used: Finset.lcm_def
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
rw : s₂.lcm f = @GCDMonoid.lcm _ inst _ (lcm ∅ f) (s₂.lcm f)
rw₁ : s₂.lcm f = @GCDMonoid.lcm _ inst _ 1 (s₂.lcm f)
rw₂ : s₂.lcm f = (normalize : (a : α) → α) (s₂.lcm f)
rw₃ rw₄ : s₂.lcm f = s₂.lcm f
⊢ (∅ ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ (lcm ∅ f) (s₂.lcm f)

Tactic:
rw [empty_union, lcm_empty, lcm_one_left, normalize_lcm]

Premises used: Finset.empty_union, Finset.normalize_lcm, Finset.lcm_empty, lcm_one_left
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
a : β
s : Finset β
h : a ∉ s
ih : (s ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ (s.lcm f) (s₂.lcm f)
rw : (insert a (s ∪ s₂)).lcm f = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
rw₁ : @GCDMonoid.lcm _ inst _ (f a) ((s ∪ s₂).lcm f) = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)
rw₂ :
  @GCDMonoid.lcm _ inst _ (f a) ((s ∪ s₂).lcm f) =
    @GCDMonoid.lcm _ inst _ (@GCDMonoid.lcm _ inst _ (f a) (s.lcm f)) (s₂.lcm f)
rw₃ :
  @GCDMonoid.lcm _ inst _ (f a) (@GCDMonoid.lcm _ inst _ (s.lcm f) (s₂.lcm f)) =
    @GCDMonoid.lcm _ inst _ (@GCDMonoid.lcm _ inst _ (f a) (s.lcm f)) (s₂.lcm f)
rw₄ rw₅ :
  @GCDMonoid.lcm _ inst _ (f a) (@GCDMonoid.lcm _ inst _ (s.lcm f) (s₂.lcm f)) =
    @GCDMonoid.lcm _ inst _ (f a) (@GCDMonoid.lcm _ inst _ (s.lcm f) (s₂.lcm f))
⊢ (insert a s ∪ s₂).lcm f = @GCDMonoid.lcm _ inst _ ((insert a s).lcm f) (s₂.lcm f)

Tactic:
rw [insert_union, lcm_insert, lcm_insert, ih, lcm_assoc]

Premises used: Finset.insert_union, lcm_assoc, Finset.lcm_insert
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f g : β → α
hs : s₁ = s₂
hfg : ∀ a ∈ s₂, f a = g a
subst : ∀ (hfg : ∀ a ∈ s₁, f a = g a), s₁.lcm f = s₁.lcm g
⊢ s₁.lcm f = s₂.lcm g

Tactic:
subst hs
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ : Finset β
f g : β → α
hfg : ∀ a ∈ s₁, f a = g a
⊢ s₁.lcm f = s₁.lcm g

Tactic:
Finset.fold_congr hfg

Premises used: Finset.fold_congr, Finset.lcm
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ : Finset β
f g : β → α
hfg : ∀ a ∈ s₁, f a = g a
⊢ s₁.lcm f = s₁.lcm g

Tactic:
exact Finset.fold_congr hfg

Premises used: Finset.fold_congr
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
h : ∀ b ∈ s, f b ∣ g b
⊢ s.lcm f ∣ s.lcm g

Tactic:
lcm_dvd fun b hb ↦ (h b hb).trans (dvd_lcm hb)

Premises used: Finset.lcm_dvd, Finset.dvd_lcm, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
h : s₁ ⊆ s₂
⊢ s₁.lcm f ∣ s₂.lcm f

Tactic:
lcm_dvd fun _ hb ↦ dvd_lcm (h hb)

Premises used: Finset.lcm_dvd, Finset.dvd_lcm
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
s : Finset γ
empty : (image g ∅).lcm f = lcm ∅ (f ∘ g)
insert :
  ∀ (a : γ) (s : Finset γ),
    a ∉ s → (image g s).lcm f = s.lcm (f ∘ g) → (image g (Insert.insert a s)).lcm f = (Insert.insert a s).lcm (f ∘ g)
⊢ (image g s).lcm f = s.lcm (f ∘ g)

Tactic:
induction s using Finset.induction
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
⊢ (image g ∅).lcm f = lcm ∅ (f ∘ g)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
a : γ
s : Finset γ
h : a ∉ s
h_1 : (image g s).lcm f = s.lcm (f ∘ g)
⊢ (image g (insert a s)).lcm f = (insert a s).lcm (f ∘ g)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
s : Finset γ
empty : (image g ∅).lcm f = lcm ∅ (f ∘ g)
insert :
  ∀ (a : γ) (s : Finset γ),
    a ∉ s → (image g s).lcm f = s.lcm (f ∘ g) → (image g (Insert.insert a s)).lcm f = (Insert.insert a s).lcm (f ∘ g)
empty₁ : (image g ∅).lcm f = lcm ∅ (f ∘ g)
insert₁ :
  ∀ (a : γ) (s : Finset γ),
    a ∉ s → (image g s).lcm f = s.lcm (f ∘ g) → (image g (Insert.insert a s)).lcm f = (Insert.insert a s).lcm (f ∘ g)
empty₂ : (image g ∅).lcm f = lcm ∅ (f ∘ g)
insert₂ :
  ∀ (a : γ) (s : Finset γ),
    a ∉ s → (image g s).lcm f = s.lcm (f ∘ g) → (image g (Insert.insert a s)).lcm f = (Insert.insert a s).lcm (f ∘ g)
empty₃ : (image g ∅).lcm f = lcm ∅ (f ∘ g)
insert₃ :
  ∀ (a : γ) (s : Finset γ),
    a ∉ s → (image g s).lcm f = s.lcm (f ∘ g) → (image g (Insert.insert a s)).lcm f = (Insert.insert a s).lcm (f ∘ g)
⊢ (image g s).lcm f = s.lcm (f ∘ g)

Tactic:
classical induction s using Finset.induction <;> simp [*]
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq α
⊢ s.lcm f = (image f s).lcm id

Tactic:
Eq.symm <| lcm_image _

Premises used: Finset.lcm_image, Eq.symm
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : Nontrivial α
⊢ s.lcm f = 0 ↔ ∃ x ∈ s, f x = 0

Tactic:
simp only [lcm_def, Multiset.lcm_eq_zero_iff, Multiset.mem_map, mem_val]

Premises used: Multiset.lcm_eq_zero_iff, Multiset.mem_map, Finset.lcm_def, Finset.mem_val
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : Nontrivial α
⊢ s.lcm f ≠ 0 ↔ ∀ x ∈ s, f x ≠ 0

Tactic:
simp [lcm_eq_zero_iff]

Premises used: Finset.lcm_eq_zero_iff
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ s.gcd f = (Multiset.map f s.val).gcd

Tactic:
rfl

Premises used: Multiset.gcd, Finset.gcd, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
⊢ gcd ∅ f = 0

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, Finset.gcd, List.foldr, rfl, Multiset.fold
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
apply : (∀ b ∈ Multiset.map f s.val, a ∣ b) ↔ ∀ b ∈ s, a ∣ f b
⊢ a ∣ s.gcd f ↔ ∀ b ∈ s, a ∣ f b

Tactic:
apply Iff.trans Multiset.dvd_gcd

Premises used: Multiset.dvd_gcd, Iff.trans
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
simp : (∀ (b : α), ∀ x ∈ s.val, f x = b → a ∣ b) ↔ ∀ b ∈ s, a ∣ f b
⊢ (∀ b ∈ Multiset.map f s.val, a ∣ b) ↔ ∀ b ∈ s, a ∣ f b

Tactic:
simp only [Multiset.mem_map, and_imp, exists_imp]

Premises used: and_imp, Multiset.mem_map, exists_imp
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ (b : α), ∀ x ∈ s.val, f x = b → a ∣ b) ↔ ∀ b ∈ s, a ∣ f b

Tactic:
⟨fun k b hb ↦ k _ _ hb rfl, fun k a' b hb h ↦ h ▸ k _ hb⟩

Premises used: Eq.rec, Iff.intro, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ (b : α), ∀ x ∈ s.val, f x = b → a ∣ b) ↔ ∀ b ∈ s, a ∣ f b

Tactic:
exact ⟨fun k b hb ↦ k _ _ hb rfl, fun k a' b hb h ↦ h ▸ k _ hb⟩
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
b : β
hb : b ∈ s
⊢ s.gcd f ∣ f b

Tactic:
dvd_gcd_iff.1 dvd_rfl _ hb

Premises used: Finset.dvd_gcd_iff, Iff.mp, dvd_rfl
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ b ∈ s, a ∣ f b) → a ∣ s.gcd f

Tactic:
dvd_gcd_iff.2

Premises used: Iff.mpr, Finset.dvd_gcd_iff
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
b : β
h : b ∉ s
⊢ (cons b s h).gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)

Tactic:
fold_cons h

Premises used: Finset.fold_cons, Finset.gcd
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq β
b : β
pos : ∀ (h : b ∈ s), (insert b s).gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)
neg : ∀ (h : b ∉ s), (insert b s).gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)
⊢ (insert b s).gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)

Tactic:
by_cases h : b ∈ s
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq β
b : β
h : b ∈ s
pos : s.gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)
pos₁ pos₂ : s.gcd f = s.gcd f
⊢ (insert b s).gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)

Tactic:
rw [insert_eq_of_mem h,
      (gcd_eq_right_iff (f b) (s.gcd f) (Multiset.normalize_gcd (s.1.map f))).2 (gcd_dvd h)]

Premises used: Iff.mpr, Finset.gcd_dvd, Multiset.map, Finset.gcd, Finset.val, Finset.insert_eq_of_mem, Multiset.normalize_gcd, gcd_eq_right_iff
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq β
b : β
h : b ∉ s
⊢ (insert b s).gcd f = @GCDMonoid.gcd _ inst _ (f b) (s.gcd f)

Tactic:
apply fold_insert h

Premises used: Finset.fold_insert
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
b : β
⊢ gcd {b} f = (normalize : (a : α) → α) (f b)

Tactic:
Multiset.gcd_singleton

Premises used: Multiset.map, List.map, Finset.fold, Multiset.cons, Multiset.gcd_singleton, Finset.gcd, Multiset.ofList
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ (normalize : (a : α) → α) (s.gcd f) = s.gcd f

Tactic:
simp [gcd_def]

Premises used: Finset.gcd_def
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
rw : s₂.gcd f = @GCDMonoid.gcd _ inst _ (gcd ∅ f) (s₂.gcd f)
rw₁ : s₂.gcd f = @GCDMonoid.gcd _ inst _ 0 (s₂.gcd f)
rw₂ : s₂.gcd f = (normalize : (a : α) → α) (s₂.gcd f)
rw₃ rw₄ : s₂.gcd f = s₂.gcd f
⊢ (∅ ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ (gcd ∅ f) (s₂.gcd f)

Tactic:
rw [empty_union, gcd_empty, gcd_zero_left, normalize_gcd]

Premises used: Finset.gcd_empty, Finset.empty_union, gcd_zero_left, Finset.normalize_gcd
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst_2 : DecidableEq β
a : β
s : Finset β
h : a ∉ s
ih : (s ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ (s.gcd f) (s₂.gcd f)
rw : (insert a (s ∪ s₂)).gcd f = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
rw₁ : @GCDMonoid.gcd _ inst _ (f a) ((s ∪ s₂).gcd f) = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)
rw₂ :
  @GCDMonoid.gcd _ inst _ (f a) ((s ∪ s₂).gcd f) =
    @GCDMonoid.gcd _ inst _ (@GCDMonoid.gcd _ inst _ (f a) (s.gcd f)) (s₂.gcd f)
rw₃ :
  @GCDMonoid.gcd _ inst _ (f a) (@GCDMonoid.gcd _ inst _ (s.gcd f) (s₂.gcd f)) =
    @GCDMonoid.gcd _ inst _ (@GCDMonoid.gcd _ inst _ (f a) (s.gcd f)) (s₂.gcd f)
rw₄ rw₅ :
  @GCDMonoid.gcd _ inst _ (f a) (@GCDMonoid.gcd _ inst _ (s.gcd f) (s₂.gcd f)) =
    @GCDMonoid.gcd _ inst _ (f a) (@GCDMonoid.gcd _ inst _ (s.gcd f) (s₂.gcd f))
⊢ (insert a s ∪ s₂).gcd f = @GCDMonoid.gcd _ inst _ ((insert a s).gcd f) (s₂.gcd f)

Tactic:
rw [insert_union, gcd_insert, gcd_insert, ih, gcd_assoc]

Premises used: gcd_assoc, Finset.insert_union, Finset.gcd_insert
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f g : β → α
hs : s₁ = s₂
hfg : ∀ a ∈ s₂, f a = g a
subst : ∀ (hfg : ∀ a ∈ s₁, f a = g a), s₁.gcd f = s₁.gcd g
⊢ s₁.gcd f = s₂.gcd g

Tactic:
subst hs
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ : Finset β
f g : β → α
hfg : ∀ a ∈ s₁, f a = g a
⊢ s₁.gcd f = s₁.gcd g

Tactic:
Finset.fold_congr hfg

Premises used: Finset.fold_congr, Finset.gcd
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ : Finset β
f g : β → α
hfg : ∀ a ∈ s₁, f a = g a
⊢ s₁.gcd f = s₁.gcd g

Tactic:
exact Finset.fold_congr hfg

Premises used: Finset.fold_congr
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
h : ∀ b ∈ s, f b ∣ g b
⊢ s.gcd f ∣ s.gcd g

Tactic:
dvd_gcd fun b hb ↦ (gcd_dvd hb).trans (h b hb)

Premises used: Finset.gcd_dvd, Finset.dvd_gcd, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
h : s₁ ⊆ s₂
⊢ s₂.gcd f ∣ s₁.gcd f

Tactic:
dvd_gcd fun _ hb ↦ gcd_dvd (h hb)

Premises used: Finset.gcd_dvd, Finset.dvd_gcd
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
s : Finset γ
empty : (image g ∅).gcd f = gcd ∅ (f ∘ g)
insert :
  ∀ (a : γ) (s : Finset γ),
    a ∉ s → (image g s).gcd f = s.gcd (f ∘ g) → (image g (Insert.insert a s)).gcd f = (Insert.insert a s).gcd (f ∘ g)
⊢ (image g s).gcd f = s.gcd (f ∘ g)

Tactic:
induction s using Finset.induction
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
⊢ (image g ∅).gcd f = gcd ∅ (f ∘ g)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
a : γ
s : Finset γ
h : a ∉ s
h_1 : (image g s).gcd f = s.gcd (f ∘ g)
⊢ (image g (insert a s)).gcd f = (insert a s).gcd (f ∘ g)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
inst_2 : DecidableEq β
g : γ → β
s : Finset γ
empty : (image g ∅).gcd f = gcd ∅ (f ∘ g)
insert :
  ∀ (a : γ) (s : Finset γ),
    a ∉ s → (image g s).gcd f = s.gcd (f ∘ g) → (image g (Insert.insert a s)).gcd f = (Insert.insert a s).gcd (f ∘ g)
empty₁ : (image g ∅).gcd f = gcd ∅ (f ∘ g)
insert₁ :
  ∀ (a : γ) (s : Finset γ),
    a ∉ s → (image g s).gcd f = s.gcd (f ∘ g) → (image g (Insert.insert a s)).gcd f = (Insert.insert a s).gcd (f ∘ g)
empty₂ : (image g ∅).gcd f = gcd ∅ (f ∘ g)
insert₂ :
  ∀ (a : γ) (s : Finset γ),
    a ∉ s → (image g s).gcd f = s.gcd (f ∘ g) → (image g (Insert.insert a s)).gcd f = (Insert.insert a s).gcd (f ∘ g)
empty₃ : (image g ∅).gcd f = gcd ∅ (f ∘ g)
insert₃ :
  ∀ (a : γ) (s : Finset γ),
    a ∉ s → (image g s).gcd f = s.gcd (f ∘ g) → (image g (Insert.insert a s)).gcd f = (Insert.insert a s).gcd (f ∘ g)
⊢ (image g s).gcd f = s.gcd (f ∘ g)

Tactic:
classical induction s using Finset.induction <;> simp [*]
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidableEq α
⊢ s.gcd f = (image f s).gcd id

Tactic:
Eq.symm <| gcd_image _

Premises used: Finset.gcd_image, Eq.symm
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ gcd ∅ f = 0 ↔ ∀ (x : β), Membership.mem (γ := Finset β) ∅ x → f x = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s_1 : Finset β
f : β → α
a : β
s : Finset β
h : a ∉ s
ih : s.gcd f = 0 ↔ ∀ x ∈ s, f x = 0
⊢ (cons a s h).gcd f = 0 ↔ ∀ x ∈ cons a s h, f x = 0

Tactic:
grind [gcd_cons, _root_.gcd_eq_zero_iff]

Premises used: Finset.gcd_cons, gcd_eq_zero_iff
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
empty : gcd ∅ f = 0 ↔ ∀ (x : β), Membership.mem (γ := Finset β) ∅ x → f x = 0
cons :
  ∀ (a : β) (s : Finset β) (h : a ∉ s) (ih : s.gcd f = 0 ↔ ∀ x ∈ s, f x = 0),
    (Finset.cons a s h).gcd f = 0 ↔ ∀ x ∈ Finset.cons a s h, f x = 0
⊢ s.gcd f = 0 ↔ ∀ x ∈ s, f x = 0

Tactic:
induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s h ih => grind [gcd_cons, _root_.gcd_eq_zero_iff]

Premises used: Finset.cons, Finset.gcd_cons, gcd_eq_zero_iff
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ s.gcd f ≠ 0 ↔ ∃ x ∈ s, f x ≠ 0

Tactic:
simp [gcd_eq_zero_iff]

Premises used: Finset.gcd_eq_zero_iff
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidablePred fun (x : β) ↦ f x = 0
trans : s.gcd f = ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f
trans₁ : ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f = {x ∈ s | f x ≠ 0}.gcd f
⊢ s.gcd f = {x ∈ s | f x ≠ 0}.gcd f

Tactic:
trans ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f

Premises used: Ne, Finset.gcd, Union.union, OfNat.ofNat, Finset.filter, Eq
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidablePred fun (x : β) ↦ f x = 0
rw rw₁ : s.gcd f = s.gcd f
⊢ s.gcd f = ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f

Tactic:
rw [filter_union_filter_not_eq]

Premises used: Finset.filter_union_filter_not_eq
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidablePred fun (x : β) ↦ f x = 0
rw : @GCDMonoid.gcd _ inst _ ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) = {x ∈ s | f x ≠ 0}.gcd f
⊢ ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f = {x ∈ s | f x ≠ 0}.gcd f

Tactic:
rw [gcd_union]

Premises used: Finset.gcd_union
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidablePred fun (x : β) ↦ f x = 0
⊢ @GCDMonoid.gcd _ inst _ ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) = {x ∈ s | f x ≠ 0}.gcd f

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

Premises used: Eq.trans