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 : β → α
inst_2 : DecidablePred fun (x : β) ↦ f x = 0
refine_1 : α
refine_2 :
  @GCDMonoid.gcd _ inst _ ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) =
    @GCDMonoid.gcd _ inst _ 0 ({x ∈ s | f x ≠ 0}.gcd f)
refine_3 : @GCDMonoid.gcd _ inst _ 0 ({x ∈ s | f x ≠ 0}.gcd f) = {x ∈ s | f x ≠ 0}.gcd f
⊢ @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:
refine Eq.trans (?_ : _ = GCDMonoid.gcd (0 : α) ?_) (?_ : GCDMonoid.gcd (0 : α) _ = _)

Premises used: Eq.trans
-- 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
⊢ α

Tactic:
exact gcd {x ∈ s | f x ≠ 0} f

Premises used: Ne, Finset.gcd, OfNat.ofNat, Finset.filter
-- 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
⊢ {x ∈ s | f x ≠ 0}.gcd f = {x ∈ s | f x ≠ 0}.gcd f

Tactic:
simp
-- 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
refine_2 : gcd ({x ∈ ∅ | f x = 0}) f = 0
refine_2₁ : ∀ (a : β) (s : Finset β), a ∉ s → {x ∈ s | f x = 0}.gcd f = 0 → {x ∈ insert a s | f x = 0}.gcd f = 0
⊢ @GCDMonoid.gcd _ inst _ ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) =
    @GCDMonoid.gcd _ inst _ 0 ({x ∈ s | f x ≠ 0}.gcd f)

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

Premises used: Finset.induction_on, congr, rfl
-- 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
⊢ gcd ({x ∈ ∅ | f x = 0}) f = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s_1 : Finset β
f : β → α
inst_2 : DecidablePred fun (x : β) ↦ f x = 0
a : β
s : Finset β
refine_2 : a ∉ s → {x ∈ s | f x = 0}.gcd f = 0 → {x ∈ insert a s | f x = 0}.gcd f = 0
⊢ a ∉ s → {x ∈ s | f x = 0}.gcd f = 0 → {x ∈ insert a s | f x = 0}.gcd f = 0

Tactic:
_
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s_1 : Finset β
f : β → α
inst_2 : DecidablePred fun (x : β) ↦ f x = 0
a : β
s : Finset β
h_1 : a ∉ s
h : {x ∈ s | f x = 0}.gcd f = 0
refine_2 : (if f a = 0 then insert a ({x ∈ s | f x = 0}) else {x ∈ s | f x = 0}).gcd f = 0
⊢ {x ∈ insert a s | f x = 0}.gcd f = 0

Tactic:
rw [filter_insert]

Premises used: Finset.filter_insert
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s_1 : Finset β
f : β → α
inst_2 : DecidablePred fun (x : β) ↦ f x = 0
a : β
s : Finset β
h_1 : a ∉ s
h : {x ∈ s | f x = 0}.gcd f = 0
pos : ∀ (h1 : f a = 0), (insert a ({x ∈ s | f x = 0})).gcd f = 0
neg : ∀ (h1 : ¬f a = 0), {x ∈ s | f x = 0}.gcd f = 0
⊢ (if f a = 0 then insert a ({x ∈ s | f x = 0}) else {x ∈ s | f x = 0}).gcd f = 0

Tactic:
split_ifs with h1
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s_1 : Finset β
f : β → α
inst_2 : DecidablePred fun (x : β) ↦ f x = 0
a : β
s : Finset β
h_1 : a ∉ s
h : {x ∈ s | f x = 0}.gcd f = 0
h1 : f a = 0
⊢ (insert a ({x ∈ s | f x = 0})).gcd f = 0

Tactic:
simp [h, h1]
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s_1 : Finset β
f : β → α
inst_2 : DecidablePred fun (x : β) ↦ f x = 0
a : β
s : Finset β
h_1 : a ∉ s
h : {x ∈ s | f x = 0}.gcd f = 0
h1 : ¬f a = 0
⊢ {x ∈ s | f x = 0}.gcd f = 0

Tactic:
simp [h, h1]
-- 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 _ 0 ({x ∈ s | f x ≠ 0}.gcd f) = {x ∈ s | f x ≠ 0}.gcd f

Tactic:
simp only [gcd_zero_left, normalize_gcd]

Premises used: gcd_zero_left, Finset.normalize_gcd
-- 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₁ trans₂ : ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f = {x ∈ s | f x ≠ 0}.gcd f
trans₃ : @GCDMonoid.gcd _ inst _ ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) = {x ∈ s | f x ≠ 0}.gcd f
refine_1 : α
refine_2 :
  @GCDMonoid.gcd _ inst _ ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) =
    @GCDMonoid.gcd _ inst _ 0 ({x ∈ s | f x ≠ 0}.gcd f)
refine_3 : @GCDMonoid.gcd _ inst _ 0 ({x ∈ s | f x ≠ 0}.gcd f) = {x ∈ s | f x ≠ 0}.gcd f
refine_2₁ :
  @GCDMonoid.gcd _ inst _ ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) =
    @GCDMonoid.gcd _ inst _ 0 ({x ∈ s | f x ≠ 0}.gcd f)
refine_3₁ refine_3₂ : @GCDMonoid.gcd _ inst _ 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:
classical
    trans ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f
    · rw [filter_union_filter_not_eq]
    rw [gcd_union]
    refine Eq.trans (?_ : _ = GCDMonoid.gcd (0 : α) ?_) (?_ : GCDMonoid.gcd (0 : α) _ = _)
    · exact gcd {x ∈ s | f x ≠ 0} f
    · refine congr (congr rfl <| s.induction_on ?_ ?_) (by simp)
      · simp
      · intro a s _ h
        rw [filter_insert]
        split_ifs with h1 <;> simp [h, h1]
    simp only [gcd_zero_left, normalize_gcd]

Premises used: Ne, Finset.gcd, Finset.filter_union_filter_not_eq, Finset.gcd_union, Finset.filter_insert, gcd_zero_left, OfNat.ofNat, Finset.filter, Finset.normalize_gcd, Eq.trans
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (s.gcd fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (s.gcd f)

Tactic:
s.induction_on ?_ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
refine_1 : (gcd ∅ fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (gcd ∅ f)
refine_2 :
  ∀ (a_1 : β) (s : Finset β),
    a_1 ∉ s →
      (s.gcd fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (s.gcd f) →
        ((insert a_1 s).gcd fun (x : β) ↦ a * f x) =
          HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) ((insert a_1 s).gcd f)
⊢ (s.gcd fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (s.gcd f)

Tactic:
refine s.induction_on ?_ ?_
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (gcd ∅ fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (gcd ∅ f)

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
refine_2 :
  b ∉ t →
    (t.gcd fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (t.gcd f) →
      ((insert b t).gcd fun (x : β) ↦ a * f x) =
        HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) ((insert b t).gcd f)
⊢ b ∉ t →
    (t.gcd fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (t.gcd f) →
      ((insert b t).gcd fun (x : β) ↦ a * f x) =
        HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) ((insert b t).gcd f)

Tactic:
_
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
h_1 : b ∉ t
h : (t.gcd fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (t.gcd f)
refine_2 :
  @GCDMonoid.gcd _ inst _ (a * f b) (HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (t.gcd f)) =
    @GCDMonoid.gcd _ inst _ (a * f b) (a * t.gcd f)
⊢ ((insert b t).gcd fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) ((insert b t).gcd f)

Tactic:
rw [gcd_insert, gcd_insert, h, ← gcd_mul_left]

Premises used: gcd_mul_left, Finset.gcd_insert
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
h_1 : b ∉ t
h : (t.gcd fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (t.gcd f)
⊢ @GCDMonoid.gcd _ inst _ (a * f b) (HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (t.gcd f)) =
    @GCDMonoid.gcd _ inst _ (a * f b) (a * t.gcd f)

Tactic:
apply ((normalize_associated a).mul_right _).gcd_eq_right

Premises used: Associated.gcd_eq_right, Associated.mul_right, normalize_associated
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
refine_1 : (gcd ∅ fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (gcd ∅ f)
refine_2 refine_2₁ :
  ∀ (a_1 : β) (s : Finset β),
    a_1 ∉ s →
      (s.gcd fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (s.gcd f) →
        ((insert a_1 s).gcd fun (x : β) ↦ a * f x) =
          HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) ((insert a_1 s).gcd f)
⊢ (s.gcd fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (s.gcd f)

Tactic:
classical
    refine s.induction_on ?_ ?_
    · simp
    · intro b t _ h
      rw [gcd_insert, gcd_insert, h, ← gcd_mul_left]
      apply ((normalize_associated a).mul_right _).gcd_eq_right

Premises used: Associated.gcd_eq_right, Finset.gcd_mul_left, Finset.gcd_insert, Associated.mul_right, normalize_associated
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (s.gcd fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (s.gcd f) ((normalize : (a : α) → α) a : α)

Tactic:
s.induction_on ?_ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
refine_1 : (gcd ∅ fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (gcd ∅ f) ((normalize : (a : α) → α) a : α)
refine_2 :
  ∀ (a_1 : β) (s : Finset β),
    a_1 ∉ s →
      (s.gcd fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (s.gcd f) ((normalize : (a : α) → α) a : α) →
        ((insert a_1 s).gcd fun (x : β) ↦ f x * a) =
          HMul.hMul (β := α) ((insert a_1 s).gcd f) ((normalize : (a : α) → α) a : α)
⊢ (s.gcd fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (s.gcd f) ((normalize : (a : α) → α) a : α)

Tactic:
refine s.induction_on ?_ ?_
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (gcd ∅ fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (gcd ∅ f) ((normalize : (a : α) → α) a : α)

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
refine_2 :
  b ∉ t →
    (t.gcd fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (t.gcd f) ((normalize : (a : α) → α) a : α) →
      ((insert b t).gcd fun (x : β) ↦ f x * a) =
        HMul.hMul (β := α) ((insert b t).gcd f) ((normalize : (a : α) → α) a : α)
⊢ b ∉ t →
    (t.gcd fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (t.gcd f) ((normalize : (a : α) → α) a : α) →
      ((insert b t).gcd fun (x : β) ↦ f x * a) =
        HMul.hMul (β := α) ((insert b t).gcd f) ((normalize : (a : α) → α) a : α)

Tactic:
_
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
h_1 : b ∉ t
h : (t.gcd fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (t.gcd f) ((normalize : (a : α) → α) a : α)
refine_2 :
  @GCDMonoid.gcd _ inst _ (f b * a) (HMul.hMul (β := α) (t.gcd f) ((normalize : (a : α) → α) a : α)) =
    @GCDMonoid.gcd _ inst _ (f b * a) (t.gcd f * a)
⊢ ((insert b t).gcd fun (x : β) ↦ f x * a) = HMul.hMul (β := α) ((insert b t).gcd f) ((normalize : (a : α) → α) a : α)

Tactic:
rw [gcd_insert, gcd_insert, h, ← gcd_mul_right]

Premises used: Finset.gcd_insert, gcd_mul_right
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
h_1 : b ∉ t
h : (t.gcd fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (t.gcd f) ((normalize : (a : α) → α) a : α)
⊢ @GCDMonoid.gcd _ inst _ (f b * a) (HMul.hMul (β := α) (t.gcd f) ((normalize : (a : α) → α) a : α)) =
    @GCDMonoid.gcd _ inst _ (f b * a) (t.gcd f * a)

Tactic:
apply ((normalize_associated a).mul_left _).gcd_eq_right

Premises used: Associated.gcd_eq_right, Associated.mul_left, normalize_associated
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
refine_1 : (gcd ∅ fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (gcd ∅ f) ((normalize : (a : α) → α) a : α)
refine_2 refine_2₁ :
  ∀ (a_1 : β) (s : Finset β),
    a_1 ∉ s →
      (s.gcd fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (s.gcd f) ((normalize : (a : α) → α) a : α) →
        ((insert a_1 s).gcd fun (x : β) ↦ f x * a) =
          HMul.hMul (β := α) ((insert a_1 s).gcd f) ((normalize : (a : α) → α) a : α)
⊢ (s.gcd fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (s.gcd f) ((normalize : (a : α) → α) a : α)

Tactic:
classical
    refine s.induction_on ?_ ?_
    · simp
    · intro b t _ h
      rw [gcd_insert, gcd_insert, h, ← gcd_mul_right]
      apply ((normalize_associated a).mul_left _).gcd_eq_right

Premises used: Associated.gcd_eq_right, Finset.gcd_insert, Associated.mul_left, Finset.gcd_mul_right, normalize_associated
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
hs : ∃ x ∈ s, f x ≠ 0
hg : ∀ b ∈ s, f b = s.gcd f * g b
rw : s.gcd f
| s.gcd f * s.gcd g

Tactic:
rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]

Premises used: Finset.gcd_congr, Finset.gcd_mul_left, Finset.normalize_gcd, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
hs : ∃ x ∈ s, f x ≠ 0
hg : ∀ b ∈ s, f b = s.gcd f * g b
conv_lhs : s.gcd f * s.gcd g = s.gcd f
conv_lhs₁ : s.gcd f = s.gcd f
⊢ s.gcd f * s.gcd g = s.gcd f

Tactic:
conv_lhs => rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]

Premises used: Finset.gcd_congr, Finset.gcd_mul_left, Finset.normalize_gcd, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
hs : ∃ x ∈ s, f x ≠ 0
hg : ∀ b ∈ s, f b = s.gcd f * g b
contrapose! : ∀ (hs : s.gcd f = 0) (x : β) (_ : x ∈ s), f x = 0
⊢ ¬s.gcd f = 0

Tactic:
contrapose! hs
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
hg : ∀ b ∈ s, f b = s.gcd f * g b
hs : s.gcd f = 0
⊢ ∀ (x : β) (_ : x ∈ s), f x = 0

Tactic:
gcd_eq_zero_iff.1 hs

Premises used: Finset.gcd_eq_zero_iff, Iff.mp
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
hg : ∀ b ∈ s, f b = s.gcd f * g b
hs : s.gcd f = 0
⊢ ∀ (x : β) (_ : x ∈ s), f x = 0

Tactic:
exact gcd_eq_zero_iff.1 hs

Premises used: Finset.gcd_eq_zero_iff, Iff.mp
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
pos : ∀ (h : ∀ x ∈ s, f x = 0), ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
neg : ∀ (h : ∃ x ∈ s, f x ≠ 0), ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
⊢ ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

Tactic:
by_cases! h : ∀ x ∈ s, f x = (0 : α)

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
b : β
hb : b ∈ s
rw : 0 = s.gcd f * (fun (x : β) ↦ (1 : α)) b
rw₁ : 0 = HMul.hMul (α := α) 0 ((fun (x : β) ↦ (1 : α)) b)
rw₂ rw₃ : Eq.{u_2 + 1} (α := α) 0 0
⊢ f b = s.gcd f * (fun (x : β) ↦ (1 : α)) b

Tactic:
rw [h b hb, gcd_eq_zero_iff.2 h, mul_one]

Premises used: Iff.mpr, Finset.gcd_eq_zero_iff, mul_one
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
pos : Eq.{u_2 + 1} (α := α) (s.gcd fun (x : β) ↦ 1) 1
⊢ ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

Tactic:
refine ⟨fun _ ↦ 1, fun b hb ↦ by rw [h b hb, gcd_eq_zero_iff.2 h, mul_one], ?_⟩
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
pos : Eq.{u_2 + 1} (α := α) (gcd (image (fun (x : β) ↦ 1) s) id) 1
pos₁ : Eq (α := α) (gcd {1} id) 1
pos₂ : Eq.{u_2 + 1} (α := α) ((normalize : (a : α) → α) (id 1) : α) (1 : α)
pos₃ : Eq.{u_2 + 1} (α := α) ((normalize : (a : α) → α) 1 : α) (1 : α)
pos₄ pos₅ : Eq.{u_2 + 1} (α := α) 1 1
⊢ Eq.{u_2 + 1} (α := α) (s.gcd fun (x : β) ↦ 1) 1

Tactic:
rw [gcd_eq_gcd_image, image_const hs, gcd_singleton, id, normalize_one]

Premises used: normalize_one, Finset.image_const, id, Finset.gcd_singleton, Finset.gcd_eq_gcd_image
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
neg :
  ∀ (g' : {b : β} → (hb : b ∈ s) → α) (hg : ∀ {b : β} (hb : b ∈ s), f b = s.gcd f * g' hb),
    ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
⊢ ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

Tactic:
choose g' hg using @gcd_dvd _ _ _ _ s f

Premises used: Finset.gcd_dvd
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
g' : {b : β} → (hb : b ∈ s) → α
hg : ∀ {b : β} (hb : b ∈ s), f b = s.gcd f * g' hb
⊢ ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

Tactic:
⟨fun b ↦ if hb : b ∈ s then g' hb else 0, fun b hb ↦ ?_,
          extract_gcd' f _ h fun b hb ↦ ?_⟩

Premises used: Membership.mem, dite, Finset.extract_gcd', And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
g' : {b : β} → (hb : b ∈ s) → α
hg : ∀ {b : β} (hb : b ∈ s), f b = s.gcd f * g' hb
neg : ∀ (b : β) (hb : b ∈ s), f b = s.gcd f * (fun (b : β) ↦ (if hb : b ∈ s then g' hb else 0 : α)) b
neg₁ : ∀ (b : β) (hb : b ∈ s), f b = s.gcd f * if hb : b ∈ s then g' hb else 0
⊢ ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

Tactic:
refine ⟨fun b ↦ if hb : b ∈ s then g' hb else 0, fun b hb ↦ ?_,
          extract_gcd' f _ h fun b hb ↦ ?_⟩
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
g' : {b : β} → (hb : b ∈ s) → α
hg : ∀ {b : β} (hb : b ∈ s), f b = s.gcd f * g' hb
b : β
hb : b ∈ s
⊢ f b = s.gcd f * (fun (b : β) ↦ (if hb : b ∈ s then g' hb else 0 : α)) b

Tactic:
simp only [hb, hg, dite_true]

Premises used: dite_true
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
g' : {b : β} → (hb : b ∈ s) → α
hg : ∀ {b : β} (hb : b ∈ s), f b = s.gcd f * g' hb
b : β
hb : b ∈ s
neg : f b = s.gcd f * g' hb
neg₁ neg₂ : s.gcd f * g' hb = s.gcd f * g' hb
⊢ f b = s.gcd f * if hb : b ∈ s then g' hb else 0

Tactic:
rw [dif_pos hb, hg hb]

Premises used: dif_pos
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
pos : ∀ (h : ∀ x ∈ s, f x = 0), ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
neg : ∀ (h : ¬∀ x ∈ s, f x = 0), ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
pos₁ : ∀ (h : ∀ x ∈ s, f x = 0), ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
neg₁ : ∀ (h : ¬∀ x ∈ s, f x = 0), ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
pos₂ : ∀ (h : ∀ x ∈ s, f x = 0), ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
neg₂ neg₃ : ∀ (h : ∃ x ∈ s, f x ≠ 0), ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
⊢ ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

Tactic:
classical
    by_cases! h : ∀ x ∈ s, f x = (0 : α)
    · refine ⟨fun _ ↦ 1, fun b hb ↦ by rw [h b hb, gcd_eq_zero_iff.2 h, mul_one], ?_⟩
      rw [gcd_eq_gcd_image, image_const hs, gcd_singleton, id, normalize_one]
    · choose g' hg using @gcd_dvd _ _ _ _ s f
      refine ⟨fun b ↦ if hb : b ∈ s then g' hb else 0, fun b hb ↦ ?_,
          extract_gcd' f _ h fun b hb ↦ ?_⟩
      · simp only [hb, hg, dite_true]
      rw [dif_pos hb, hg hb]

Premises used: normalize_one, Finset.gcd_dvd, Finset.image_const, id, Finset.gcd_singleton, Finset.gcd_eq_gcd_image, dite_true, OfNat.ofNat
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : Div α
inst_3 : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
obtain :
  ∀ (g : ι → α) (he : ∀ b ∈ s, f b = s.gcd f * g b) (hg : s.gcd g = 1),
    Eq.{u_2 + 1} (α := α) (s.gcd fun (j : ι) ↦ f j / s.gcd f) 1
⊢ Eq.{u_2 + 1} (α := α) (s.gcd fun (j : ι) ↦ f j / s.gcd f) 1

Tactic:
obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨i, his⟩

Premises used: Finset.extract_gcd, Exists.intro
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : Div α
inst_3 : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
g : ι → α
he : ∀ b ∈ s, f b = s.gcd f * g b
hg : s.gcd g = 1
⊢ Eq.{u_2 + 1} (α := α) (s.gcd fun (j : ι) ↦ f j / s.gcd f) 1

Tactic:
(Finset.gcd_congr rfl fun a ha ↦ ?_).trans hg

Premises used: Finset.gcd_congr, rfl, Eq.trans
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
inst_2 : Div α
inst_3 : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
g : ι → α
he : ∀ b ∈ s, f b = s.gcd f * g b
hg : s.gcd g = 1
refine : ∀ (a : ι) (ha : a ∈ s), f a / s.gcd f = g a
⊢ Eq.{u_2 + 1} (α := α) (s.gcd fun (j : ι) ↦ f j / s.gcd f) 1

Tactic:
refine (Finset.gcd_congr rfl fun a ha ↦ ?_).trans hg

Premises used: Finset.gcd_congr, rfl, Eq.trans