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 : β → α
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
⊢ Eq.{u_2 + 1} (α := α) (s.gcd fun (x : β) ↦ 1) 1
have pos₂ : Eq.{u_2 + 1} (α := α) ((normalize : (a : α) → α) (id 1) : α) (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
pos₁ : Eq (α := α) (gcd {1} id) 1
pos₂ : Eq.{u_2 + 1} (α := α) ((normalize : (a : α) → α) (id 1) : α) (1 : α)
⊢ Eq.{u_2 + 1} (α := α) (s.gcd fun (x : β) ↦ 1) 1
have pos₃ : Eq.{u_2 + 1} (α := α) ((normalize : (a : α) → α) 1 : α) (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
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 : α)
⊢ Eq.{u_2 + 1} (α := α) (s.gcd fun (x : β) ↦ 1) 1
have pos₄ : Eq.{u_2 + 1} (α := α) 1 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
⊢ ∃ (g : β → α), (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
have 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
Tactic: choose g' hg using @gcd_dvd _ _ _ _ s 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 : β → α
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
have neg : ∀ (b : β) (hb : b ∈ s), f b = s.gcd f * (fun (b : β) ↦ (if hb : b ∈ s then g' hb else 0 : α)) b
Tactic: refine ⟨fun b ↦ if hb : b ∈ s then g' hb else 0, fun b hb ↦ ?_,
          extract_gcd' f _ h fun b hb ↦ ?_⟩
-- 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 : β} → (hb : b ∈ s) → α
hg : ∀ {b : β} (hb : b ∈ s), f b = s.gcd f * g' hb
b : β
hb : b ∈ s
⊢ f b = s.gcd f * if hb : b ∈ s then g' hb else 0
have neg : f b = s.gcd f * g' hb
Tactic: rw [dif_pos hb, hg hb]
-- 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 : β} → (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
⊢ f b = s.gcd f * if hb : b ∈ s then g' hb else 0
have neg₁ : s.gcd f * g' hb = s.gcd f * g' hb
Tactic: rw [dif_pos hb, hg hb]
-- 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: 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]
-- 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: 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]
-- 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
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
⊢ ∃ (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: 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]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
⊢ Eq.{u_2 + 1} (α := α) (s.gcd fun (j : ι) ↦ f j / s.gcd f) 1
have 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
Tactic: obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨i, his⟩
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
have refine : ∀ (a : ι) (ha : a ∈ s), f a / s.gcd f = g a
Tactic: refine (Finset.gcd_congr rfl fun a ha ↦ ?_).trans hg
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
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
a : ι
ha : a ∈ s
⊢ f a / s.gcd f = g a
have ha₁ : s.gcd f ≠ 0
Tactic: rw [he a ha, mul_div_cancel_left₀]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
h : ∀ x ∈ s, a ∣ f x - g x
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
have revert : ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
  @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
⊢ ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
have refine_1 : ∀ (h : ∀ (x : β), Membership.mem (γ := Finset β) ∅ x → a ∣ f x - g x),
  @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ f) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ g)
Tactic: refine s.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
refine_1 :
  ∀ (h : ∀ (x : β), Membership.mem (γ := Finset β) ∅ x → a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ g)
⊢ ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
have refine_2 : ∀ (a_1 : β) (s : Finset β),
  a_1 ∉ s →
    (∀ (h : ∀ x ∈ s, a ∣ f x - g x),
        @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
          @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)) →
      ∀ (h : ∀ x ∈ insert a_1 s, a ∣ f x - g x),
        @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert a_1 s).gcd f) =
          @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert a_1 s).gcd g)
Tactic: refine s.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s_1 : Finset β
f g : β → α
a : α
b : β
s : Finset β
h_1 : b ∉ s
hi :
  ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
h : ∀ x ∈ insert b s, a ∣ f x - g x
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert b s).gcd f) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert b s).gcd g)
have refine_2 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (s.gcd g)
    (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (f b)) =
  @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (s.gcd g)
    (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (g b))
Tactic: rw [gcd_insert, gcd_insert, gcd_comm (f b), ← gcd_assoc,
      hi fun x hx ↦ h _ (mem_insert_of_mem hx), gcd_comm a, gcd_assoc,
      gcd_comm a (GCDMonoid.gcd _ _), gcd_comm (g b), gcd_assoc _ _ a, gcd_comm _ a]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
h : ∀ x ∈ s, a ∣ f x - g x
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
have revert : ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
  @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
Tactic: classical
    revert h
    refine s.induction_on ?_ ?_
    · simp
    intro b s _ hi h
    rw [gcd_insert, gcd_insert, gcd_comm (f b), ← gcd_assoc,
      hi fun x hx ↦ h _ (mem_insert_of_mem hx), gcd_comm a, gcd_assoc,
      gcd_comm a (GCDMonoid.gcd _ _), gcd_comm (g b), gcd_assoc _ _ a, gcd_comm _ a]
    exact congr_arg _ (gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
h : ∀ x ∈ s, a ∣ f x - g x
revert :
  ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
have refine_1 : ∀ (h : ∀ (x : β), Membership.mem (γ := Finset β) ∅ x → a ∣ f x - g x),
  @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ f) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ g)
Tactic: classical
    revert h
    refine s.induction_on ?_ ?_
    · simp
    intro b s _ hi h
    rw [gcd_insert, gcd_insert, gcd_comm (f b), ← gcd_assoc,
      hi fun x hx ↦ h _ (mem_insert_of_mem hx), gcd_comm a, gcd_assoc,
      gcd_comm a (GCDMonoid.gcd _ _), gcd_comm (g b), gcd_assoc _ _ a, gcd_comm _ a]
    exact congr_arg _ (gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
h : ∀ x ∈ s, a ∣ f x - g x
revert :
  ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
refine_1 :
  ∀ (h : ∀ (x : β), Membership.mem (γ := Finset β) ∅ x → a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ g)
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
have refine_2 : ∀ (a_1 : β) (s : Finset β),
  a_1 ∉ s →
    (∀ (h : ∀ x ∈ s, a ∣ f x - g x),
        @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
          @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)) →
      ∀ (h : ∀ x ∈ insert a_1 s, a ∣ f x - g x),
        @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert a_1 s).gcd f) =
          @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert a_1 s).gcd g)
Tactic: classical
    revert h
    refine s.induction_on ?_ ?_
    · simp
    intro b s _ hi h
    rw [gcd_insert, gcd_insert, gcd_comm (f b), ← gcd_assoc,
      hi fun x hx ↦ h _ (mem_insert_of_mem hx), gcd_comm a, gcd_assoc,
      gcd_comm a (GCDMonoid.gcd _ _), gcd_comm (g b), gcd_assoc _ _ a, gcd_comm _ a]
    exact congr_arg _ (gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
h : ∀ x ∈ s, a ∣ f x - g x
revert :
  ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
refine_1 :
  ∀ (h : ∀ (x : β), Membership.mem (γ := Finset β) ∅ x → a ∣ f x - g x),
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ f) =
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (gcd ∅ g)
refine_2 refine_2₁ refine_2₂ :
  ∀ (b : β) (s : Finset β),
    b ∉ s →
      ∀
        (hi :
          ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
            @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
              @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g))
        (h : ∀ x ∈ insert b s, a ∣ f x - g x),
        @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert b s).gcd f) =
          @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a ((insert b s).gcd g)
⊢ @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g)
have refine_2₃ : ∀ (b : β) (s : Finset β),
  b ∉ s →
    ∀
      (hi :
        ∀ (h : ∀ x ∈ s, a ∣ f x - g x),
          @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd f) =
            @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (s.gcd g))
      (h : ∀ x ∈ insert b s, a ∣ f x - g x),
      @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (s.gcd g)
          (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (f b)) =
        @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (s.gcd g)
          (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a (g b))
Tactic: classical
    revert h
    refine s.induction_on ?_ ?_
    · simp
    intro b s _ hi h
    rw [gcd_insert, gcd_insert, gcd_comm (f b), ← gcd_assoc,
      hi fun x hx ↦ h _ (mem_insert_of_mem hx), gcd_comm a, gcd_assoc,
      gcd_comm a (GCDMonoid.gcd _ _), gcd_comm (g b), gcd_assoc _ _ a, gcd_comm _ a]
    exact congr_arg _ (gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
ι : Type u_1
s_1 : Finset ι
f : ι → ℤ
a : ι
s : Finset ι
has : a ∉ s
ih : 0 ≤ s.gcd f
⊢ 0 ≤ (cons a s has).gcd f
have cons : LE.le (α := ℤ) 0 (↑((f a).gcd (s.gcd f)) : ℤ)
Tactic: rw [gcd_cons, ← Int.coe_gcd]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℤ
⊢ 0 ≤ s.gcd f
have empty : 0 ≤ gcd ∅ f
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s has ih =>
    rw [gcd_cons, ← Int.coe_gcd]
    grind
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Finset (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℤ
empty : 0 ≤ gcd ∅ f
⊢ 0 ≤ s.gcd f
have cons : ∀ (a : ι) (s : Finset ι) (has : a ∉ s) (ih : 0 ≤ s.gcd f), 0 ≤ (cons a s has).gcd f
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s has ih =>
    rw [gcd_cons, ← Int.coe_gcd]
    grind
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
h : (↑s : Set ι).Pairwise (Function.onFun Nat.Coprime f)
⊢ Nat.Coprime = IsRelPrime
have h₁ : ∀ (x x_1 : ℕ), x.Coprime x_1 ↔ IsRelPrime x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (hypothesis)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℕ
h : (↑s : Set ι).Pairwise (Function.onFun Nat.Coprime f)
⊢ s.lcm f = s.prod f
have h₁ : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f)
Tactic: rw [show Nat.Coprime = IsRelPrime by ext; exact Nat.coprime_iff_isRelPrime] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (goal)
Goal:
ι : Type u_1
f : ι → ℕ
s : Finset ι
hf : ∀ k ∈ s, f k ≠ 0
p : ℕ
⊢ Eq (α := ℕ) (((s.lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
    (s.sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)
have empty : ∀ (hf : ∀ (k : ι), Membership.mem (γ := Finset ι) ∅ k → f k ≠ 0),
  Eq (α := ℕ) (((lcm ∅ f).factorization : (a : ℕ) → ℕ) p : ℕ)
    (sup ∅ fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ _ => simp_all [lcm_eq_nat_lcm, Nat.factorization_lcm]
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (goal)
Goal:
ι : Type u_1
f : ι → ℕ
s : Finset ι
hf : ∀ k ∈ s, f k ≠ 0
p : ℕ
empty :
  ∀ (hf : ∀ (k : ι), Membership.mem (γ := Finset ι) ∅ k → f k ≠ 0),
    Eq (α := ℕ) (((lcm ∅ f).factorization : (a : ℕ) → ℕ) p : ℕ)
      (sup ∅ fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ Eq (α := ℕ) (((s.lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
    (s.sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)
have insert : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    (∀ (hf : ∀ k ∈ s, f k ≠ 0),
        Eq (α := ℕ) (((s.lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
          (s.sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)) →
      ∀ (hf : ∀ k ∈ insert a s, f k ≠ 0),
        Eq (α := ℕ) ((((insert a s).lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
          ((insert a s).sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ _ => simp_all [lcm_eq_nat_lcm, Nat.factorization_lcm]
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (goal)
Goal:
ι : Type u_1
f : ι → ℕ
s : Finset ι
hf : ∀ k ∈ s, f k ≠ 0
p : ℕ
⊢ Eq (α := ℕ) (((s.lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
    (s.sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)
have empty : ∀ (hf : ∀ (k : ι), Membership.mem (γ := Finset ι) ∅ k → f k ≠ 0),
  Eq (α := ℕ) (((lcm ∅ f).factorization : (a : ℕ) → ℕ) p : ℕ)
    (sup ∅ fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ _ => simp_all [lcm_eq_nat_lcm, Nat.factorization_lcm]
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (goal)
Goal:
ι : Type u_1
f : ι → ℕ
s : Finset ι
hf : ∀ k ∈ s, f k ≠ 0
p : ℕ
empty :
  ∀ (hf : ∀ (k : ι), Membership.mem (γ := Finset ι) ∅ k → f k ≠ 0),
    Eq (α := ℕ) (((lcm ∅ f).factorization : (a : ℕ) → ℕ) p : ℕ)
      (sup ∅ fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ Eq (α := ℕ) (((s.lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
    (s.sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)
have insert : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    (∀ (hf : ∀ k ∈ s, f k ≠ 0),
        Eq (α := ℕ) (((s.lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
          (s.sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)) →
      ∀ (hf : ∀ k ∈ insert a s, f k ≠ 0),
        Eq (α := ℕ) ((((insert a s).lcm f).factorization : (a : ℕ) → ℕ) p : ℕ)
          ((insert a s).sup fun (a : ι) ↦ ((f a).factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ _ => simp_all [lcm_eq_nat_lcm, Nat.factorization_lcm]
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (goal)
Goal:
ι : Type u_3
f : ι → ℚ
a : ι
s : Finset ι
has : a ∉ s
ih : Rat.den (∑ i ∈ s, f i) ∣ s.lcm fun (i : ι) ↦ (f i).den
⊢ Rat.den (∑ i ∈ insert a s, f i) ∣ (insert a s).lcm fun (i : ι) ↦ (f i).den
have insert : (f a + ∑ x ∈ s, f x).den ∣ @GCDMonoid.lcm _ Nat.instCommMonoidWithZero _ (f a).den (s.lcm fun (i : ι) ↦ (f i).den)
Tactic: rw [Finset.sum_insert has, Finset.lcm_insert]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (goal)
Goal:
ι : Type u_3
s : Finset ι
f : ι → ℚ
⊢ Rat.den (∑ i ∈ s, f i) ∣ s.lcm fun (i : ι) ↦ (f i).den
have empty : Rat.den (∑ i ∈ ∅, f i) ∣ lcm ∅ fun (i : ι) ↦ (f i).den
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ has ih =>
    rw [Finset.sum_insert has, Finset.lcm_insert]
    exact (Rat.add_den_dvd_lcm _ _).trans (lcm_dvd_lcm dvd_rfl ih)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.FinsetLemmas (goal)
Goal:
ι : Type u_3
s : Finset ι
f : ι → ℚ
empty : Rat.den (∑ i ∈ ∅, f i) ∣ lcm ∅ fun (i : ι) ↦ (f i).den
⊢ Rat.den (∑ i ∈ s, f i) ∣ s.lcm fun (i : ι) ↦ (f i).den
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s) (ih : Rat.den (∑ i ∈ s, f i) ∣ s.lcm fun (i : ι) ↦ (f i).den),
  Rat.den (∑ i ∈ insert a s, f i) ∣ (insert a s).lcm fun (i : ι) ↦ (f i).den
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ has ih =>
    rw [Finset.sum_insert has, Finset.lcm_insert]
    exact (Rat.add_den_dvd_lcm _ _).trans (lcm_dvd_lcm dvd_rfl ih)
Cleared hypotheses: s