awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ s.gcd f = 0 ↔ ∀ x ∈ s, f x = 0
have cons : ∀ (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: induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s h ih => grind [gcd_cons, _root_.gcd_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidablePred fun (x : β) ↦ f x = 0
⊢ s.gcd f = {x ∈ s | f x ≠ 0}.gcd f
have trans : s.gcd f = ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f
Tactic: trans ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ s.gcd f = {x ∈ s | f x ≠ 0}.gcd f
have trans₁ : ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f = {x ∈ s | f x ≠ 0}.gcd f
Tactic: trans ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidablePred fun (x : β) ↦ f x = 0
⊢ s.gcd f = ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f
have rw : s.gcd f = s.gcd f
Tactic: rw [filter_union_filter_not_eq]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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} ∪ {x ∈ s | f x ≠ 0}).gcd f = {x ∈ s | f x ≠ 0}.gcd f
have 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
Tactic: rw [gcd_union]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
have refine_1 : α
Tactic: refine Eq.trans (?_ : _ = GCDMonoid.gcd (0 : α) ?_) (?_ : GCDMonoid.gcd (0 : α) _ = _)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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 : α
⊢ @GCDMonoid.gcd _ inst _ ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) = {x ∈ s | f x ≠ 0}.gcd f
have 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)
Tactic: refine Eq.trans (?_ : _ = GCDMonoid.gcd (0 : α) ?_) (?_ : GCDMonoid.gcd (0 : α) _ = _)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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)
⊢ @GCDMonoid.gcd _ inst _ ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) = {x ∈ s | f x ≠ 0}.gcd f
have refine_3 : @GCDMonoid.gcd _ inst _ 0 ({x ∈ s | f x ≠ 0}.gcd f) = {x ∈ s | f x ≠ 0}.gcd f
Tactic: refine Eq.trans (?_ : _ = GCDMonoid.gcd (0 : α) ?_) (?_ : GCDMonoid.gcd (0 : α) _ = _)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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) =
    @GCDMonoid.gcd _ inst _ 0 ({x ∈ s | f x ≠ 0}.gcd f)
have refine_2 : gcd ({x ∈ ∅ | f x = 0}) f = 0
Tactic: refine congr (congr rfl <| s.induction_on ?_ ?_) (by simp)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ @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)
have 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
Tactic: refine congr (congr rfl <| s.induction_on ?_ ?_) (by simp)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ {x ∈ insert a s | f x = 0}.gcd f = 0
have refine_2 : (if f a = 0 then insert a ({x ∈ s | f x = 0}) else {x ∈ s | f x = 0}).gcd f = 0
Tactic: rw [filter_insert]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ (if f a = 0 then insert a ({x ∈ s | f x = 0}) else {x ∈ s | f x = 0}).gcd f = 0
have pos : ∀ (h1 : f a = 0), (insert a ({x ∈ s | f x = 0})).gcd f = 0
Tactic: split_ifs with h1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ (if f a = 0 then insert a ({x ∈ s | f x = 0}) else {x ∈ s | f x = 0}).gcd f = 0
have neg : ∀ (h1 : ¬f a = 0), {x ∈ s | f x = 0}.gcd f = 0
Tactic: split_ifs with h1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst_2 : DecidablePred fun (x : β) ↦ f x = 0
⊢ s.gcd f = {x ∈ s | f x ≠ 0}.gcd f
have trans : s.gcd f = ({x ∈ s | f x = 0} ∪ {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]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ s.gcd f = {x ∈ s | f x ≠ 0}.gcd f
have trans₁ : ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).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]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ s.gcd f = {x ∈ s | f x ≠ 0}.gcd f
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ s.gcd f = {x ∈ s | f x ≠ 0}.gcd f
have refine_1 : α
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]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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 : α
⊢ s.gcd f = {x ∈ s | f x ≠ 0}.gcd f
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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)
⊢ s.gcd f = {x ∈ s | f x ≠ 0}.gcd f
have refine_3 : @GCDMonoid.gcd _ inst _ 0 ({x ∈ s | f x ≠ 0}.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]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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)
have refine_1 : (gcd ∅ fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (gcd ∅ f)
Tactic: refine s.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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)
⊢ (s.gcd fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (s.gcd f)
have 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)
Tactic: refine s.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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)
⊢ ((insert b t).gcd fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) ((insert b t).gcd f)
have 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)
Tactic: rw [gcd_insert, gcd_insert, h, ← gcd_mul_left]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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)
have refine_1 : (gcd ∅ fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (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
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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)
⊢ (s.gcd fun (x : β) ↦ a * f x) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (s.gcd f)
have 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)
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
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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 : α)
have refine_1 : (gcd ∅ fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (gcd ∅ f) ((normalize : (a : α) → α) a : α)
Tactic: refine s.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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 : α)
⊢ (s.gcd fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (s.gcd f) ((normalize : (a : α) → α) a : α)
have 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 : α)
Tactic: refine s.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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 : α)
⊢ ((insert b t).gcd fun (x : β) ↦ f x * a) = HMul.hMul (β := α) ((insert b t).gcd f) ((normalize : (a : α) → α) a : α)
have 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)
Tactic: rw [gcd_insert, gcd_insert, h, ← gcd_mul_right]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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 : α)
have refine_1 : (gcd ∅ fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (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
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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 : α)
⊢ (s.gcd fun (x : β) ↦ f x * a) = HMul.hMul (β := α) (s.gcd f) ((normalize : (a : α) → α) a : α)
have 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 : α)
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
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
| s.gcd f * s.gcd g
have rw : s.gcd f
Tactic: rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ s.gcd f * s.gcd g = s.gcd f
have conv_lhs : s.gcd f * s.gcd g = s.gcd f
Tactic: conv_lhs => rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ s.gcd f * s.gcd g = s.gcd f
have conv_lhs₁ : s.gcd f = s.gcd f
Tactic: conv_lhs => rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ ¬s.gcd f = 0
have contrapose! : ∀ (hs : s.gcd f = 0) (x : β) (_ : x ∈ s), f x = 0
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
⊢ ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
have pos : ∀ (h : ∀ x ∈ s, f x = 0), ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
Tactic: by_cases! h : ∀ x ∈ s, f x = (0 : α)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
have neg : ∀ (h : ∃ x ∈ s, f x ≠ 0), ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
Tactic: by_cases! h : ∀ x ∈ s, f x = (0 : α)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ f b = s.gcd f * (fun (x : β) ↦ (1 : α)) b
have rw : 0 = s.gcd f * (fun (x : β) ↦ (1 : α)) b
Tactic: rw [h b hb, gcd_eq_zero_iff.2 h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ f b = s.gcd f * (fun (x : β) ↦ (1 : α)) b
have rw₁ : 0 = HMul.hMul (α := α) 0 ((fun (x : β) ↦ (1 : α)) b)
Tactic: rw [h b hb, gcd_eq_zero_iff.2 h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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)
⊢ f b = s.gcd f * (fun (x : β) ↦ (1 : α)) b
have rw₂ : Eq.{u_2 + 1} (α := α) 0 0
Tactic: rw [h b hb, gcd_eq_zero_iff.2 h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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 ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
have pos : Eq.{u_2 + 1} (α := α) (s.gcd fun (x : β) ↦ 1) 1
Tactic: refine ⟨fun _ ↦ 1, fun b hb ↦ by rw [h b hb, gcd_eq_zero_iff.2 h, mul_one], ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
⊢ Eq.{u_2 + 1} (α := α) (s.gcd fun (x : β) ↦ 1) 1
have pos : Eq.{u_2 + 1} (α := α) (gcd (image (fun (x : β) ↦ 1) s) id) 1
Tactic: rw [gcd_eq_gcd_image, image_const hs, gcd_singleton, id, normalize_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ Eq.{u_2 + 1} (α := α) (s.gcd fun (x : β) ↦ 1) 1
have pos₁ : Eq (α := α) (gcd {1} id) 1
Tactic: rw [gcd_eq_gcd_image, image_const hs, gcd_singleton, id, normalize_one]