awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
Hs : (↑t : Set I).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ t, s i ∣ z
empty :
  ∀ (Hs : (↑∅ : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ (i : I), Membership.mem (γ := Finset I) ∅ i → s i ∣ z),
    ∏ x ∈ ∅, s x ∣ z
⊢ ∏ x ∈ t, s x ∣ z
have insert : ∀ (a : I) (r : Finset I) (har : a ∉ r)
  (ih : ∀ (Hs : (↑r : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ i ∈ r, s i ∣ z), ∏ x ∈ r, s x ∣ z)
  (Hs : (↑(insert a r) : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ i ∈ insert a r, s i ∣ z), ∏ x ∈ insert a r, s x ∣ z
Tactic: classical
  induction t using Finset.induction_on with
  | empty => simp
  | insert a r har ih =>
    rw [Finset.prod_insert har]
    refine IsCoprime.mul_dvd ?_ ?_ ?_
    · refine IsCoprime.prod_right fun i hir ↦ ?_
      exact Hs (by simp) (by simp [hir]) (ne_of_mem_of_not_mem hir har).symm
    · exact Hs1 a (Finset.mem_insert_self a r)
    · refine ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi
      simp only [Finset.coe_insert, Set.subset_insert]
Cleared hypotheses: Hs, Hs1
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
⊢ (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥(cons a t hat))
      (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥(cons a t hat)) ↦ s (↑i : I))
have cons : (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j) 1) ↔
  Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (a : ↥t) ↦ s (↑a : I)) ∧
    ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
Tactic: rw [pairwise_cons']
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
x : I
hx : x ∈ t
⊢ a ∈ insert a t \ {x}
have rw : a ∈ insert a t ∧ ¬a = x
Tactic: rw [mem_sdiff, mem_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (hypothesis)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
⊢ (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (a : ↥t) ↦ s (↑a : I)) ∧
      ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
have mem : ∀ x ∈ t, a ∈ insert a t \ {x}
Tactic: have mem : ∀ x ∈ t, a ∈ insert a t \ {x} := fun x hx ↦ by
      rw [mem_sdiff, mem_singleton]
      exact ⟨mem_insert_self _ _, fun ha ↦ hat (ha ▸ hx)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
⊢ (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (a : ↥t) ↦ s (↑a : I)) ∧
      ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
have cons : (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j) 1) →
  Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (a : ↥t) ↦ s (↑a : I)) ∧
    ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
cons :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ Finset.cons a t hat, μ i * ∏ j ∈ Finset.cons a t hat \ {i}, s j) 1) →
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (a : ↥t) ↦ s (↑a : I)) ∧
      ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
⊢ (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ Finset.cons a t hat, μ i * ∏ j ∈ Finset.cons a t hat \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (a : ↥t) ↦ s (↑a : I)) ∧
      ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
have cons₁ : (Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (a : ↥t) ↦ s (↑a : I)) ∧
    ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)) →
  ∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ Finset.cons a t hat, μ i * ∏ j ∈ Finset.cons a t hat \ {i}, s j) 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (hypothesis)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : Eq.{u + 1} (α := R) (∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j) 1
⊢ Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (a : ↥t) ↦ s (↑a : I)) ∧
    ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
have hμ₁ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
Tactic: rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat] at hμ
Cleared hypotheses: hμ
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
⊢ Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (a : ↥t) ↦ s (↑a : I)) ∧
    ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
have cons : Eq.{u + 1} (α := R)
  (∑ i ∈ t,
    HAdd.hAdd (α := (j : I) → R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)))
        (μ * fun (x : I) ↦ s a) i *
      ∏ j ∈ t \ {i}, s j)
  1
Tactic: refine ⟨ih.mp ⟨Pi.single h.choose (μ a * s h.choose) + μ * fun _ ↦ s a, ?_⟩, fun b hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
cons :
  Eq.{u + 1} (α := R)
    (∑ i ∈ t,
      HAdd.hAdd (α := (j : I) → R)
          (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h)))
          (μ * fun (x : I) ↦ s a) i *
        ∏ j ∈ t \ {i}, s j)
    1
⊢ Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (a : ↥t) ↦ s (↑a : I)) ∧
    ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
have cons₁ : ∀ (b : I) (hb : b ∈ t), IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
Tactic: refine ⟨ih.mp ⟨Pi.single h.choose (μ a * s h.choose) + μ * fun _ ↦ s a, ?_⟩, fun b hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (hypothesis)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
⊢ Eq.{u + 1} (α := R)
    (∑ i ∈ t,
      HAdd.hAdd (α := (j : I) → R)
          (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h)))
          (μ * fun (x : I) ↦ s a) i *
        ∏ j ∈ t \ {i}, s j)
    1
have hμ₁ : μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x +
    ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
  1
Tactic: rw [prod_eq_mul_prod_diff_singleton_of_mem h.choose_spec, ← mul_assoc, ←
          @if_pos _ _ h.choose_spec R (_ * _) 0, ← sum_pi_single', ← sum_add_distrib] at hμ
Cleared hypotheses: hμ
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (hypothesis)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ₁ :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
⊢ Eq.{u + 1} (α := R)
    (∑ i ∈ t,
      HAdd.hAdd (α := (j : I) → R)
          (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h)))
          (μ * fun (x : I) ↦ s a) i *
        ∏ j ∈ t \ {i}, s j)
    1
have hμ₂ : Eq.{u + 1} (α := R)
  (∑ x ∈ t,
    HAdd.hAdd (α := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
          x :
        R)
      (μ x * ∏ j ∈ insert a t \ {x}, s j))
  1
Tactic: rw [prod_eq_mul_prod_diff_singleton_of_mem h.choose_spec, ← mul_assoc, ←
          @if_pos _ _ h.choose_spec R (_ * _) 0, ← sum_pi_single', ← sum_add_distrib] at hμ
Cleared hypotheses: hμ
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ_1 :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
hμ :
  Eq.{u + 1} (α := R)
    (∑ x ∈ t,
      HAdd.hAdd (α := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h) *
              ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
            x :
          R)
        (μ x * ∏ j ∈ insert a t \ {x}, s j))
    1
⊢ Eq.{u + 1} (α := R)
    (∑ i ∈ t,
      HAdd.hAdd (α := (j : I) → R)
          (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h)))
          (μ * fun (x : I) ↦ s a) i *
        ∏ j ∈ t \ {i}, s j)
    1
have cons : ∀ x ∈ t,
  HAdd.hAdd (α := (j : I) → R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)))
        (μ * fun (x : I) ↦ s a) x *
      ∏ j ∈ t \ {x}, s j =
    HAdd.hAdd (α := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
          x :
        R)
      (μ x * ∏ j ∈ insert a t \ {x}, s j)
Tactic: rw [← hμ, sum_congr rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ_1 :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
hμ :
  Eq.{u + 1} (α := R)
    (∑ x ∈ t,
      HAdd.hAdd (α := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h) *
              ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
            x :
          R)
        (μ x * ∏ j ∈ insert a t \ {x}, s j))
    1
x : I
hx : x ∈ t
⊢ HAdd.hAdd (α := (j : I) → R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)))
        (μ * fun (x : I) ↦ s a) x *
      ∏ j ∈ t \ {x}, s j =
    HAdd.hAdd (α := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
          x :
        R)
      (μ x * ∏ j ∈ insert a t \ {x}, s j)
have h₁ : Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
    (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x) x =
  HMul.hMul (α := R) (β := R)
    (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
        (μ a * s (Exists.choose (p := Membership.mem t) h)) x :
      R)
    (∏ j ∈ t \ {x}, s j : R)
Tactic: convert! add_mul (R := R) _ _ _ using 2
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ_1 :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
hμ :
  Eq.{u + 1} (α := R)
    (∑ x ∈ t,
      HAdd.hAdd (α := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h) *
              ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
            x :
          R)
        (μ x * ∏ j ∈ insert a t \ {x}, s j))
    1
x : I
hx : x ∈ t
h₁ :
  Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
      (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x) x =
    HMul.hMul (α := R) (β := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)) x :
        R)
      (∏ j ∈ t \ {x}, s j : R)
⊢ HAdd.hAdd (α := (j : I) → R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)))
        (μ * fun (x : I) ↦ s a) x *
      ∏ j ∈ t \ {x}, s j =
    HAdd.hAdd (α := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
          x :
        R)
      (μ x * ∏ j ∈ insert a t \ {x}, s j)
have h₂ : μ x * ∏ j ∈ insert a t \ {x}, s j = HMul.hMul (β := I → R) μ (fun (x : I) ↦ s a) x * ∏ j ∈ t \ {x}, s j
Tactic: convert! add_mul (R := R) _ _ _ using 2
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ_1 :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
hμ :
  Eq.{u + 1} (α := R)
    (∑ x ∈ t,
      HAdd.hAdd (α := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h) *
              ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
            x :
          R)
        (μ x * ∏ j ∈ insert a t \ {x}, s j))
    1
x : I
hx : x ∈ t
⊢ Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
      (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x) x =
    HMul.hMul (α := R) (β := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)) x :
        R)
      (∏ j ∈ t \ {x}, s j : R)
have pos : ∀ (hx : x = Exists.choose (p := Membership.mem t) h),
  Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
      (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x) x =
    HMul.hMul (α := R) (β := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)) x :
        R)
      (∏ j ∈ t \ {x}, s j : R)
Tactic: by_cases hx : x = h.choose
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ_1 :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
hμ :
  Eq.{u + 1} (α := R)
    (∑ x ∈ t,
      HAdd.hAdd (α := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h) *
              ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
            x :
          R)
        (μ x * ∏ j ∈ insert a t \ {x}, s j))
    1
x : I
hx : x ∈ t
pos :
  ∀ (hx : x = Exists.choose (p := Membership.mem t) h),
    Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
        (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
        x =
      HMul.hMul (α := R) (β := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h)) x :
          R)
        (∏ j ∈ t \ {x}, s j : R)
⊢ Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
      (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x) x =
    HMul.hMul (α := R) (β := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)) x :
        R)
      (∏ j ∈ t \ {x}, s j : R)
have neg : ∀ (hx : ¬x = Exists.choose (p := Membership.mem t) h),
  Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
      (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x) x =
    HMul.hMul (α := R) (β := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)) x :
        R)
      (∏ j ∈ t \ {x}, s j : R)
Tactic: by_cases hx : x = h.choose
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ_1 :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
hμ :
  Eq.{u + 1} (α := R)
    (∑ x ∈ t,
      HAdd.hAdd (α := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h) *
              ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
            x :
          R)
        (μ x * ∏ j ∈ insert a t \ {x}, s j))
    1
x : I
hx_1 : x ∈ t
hx : x = Exists.choose (p := Membership.mem t) h
⊢ Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
      (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x) x =
    HMul.hMul (α := R) (β := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)) x :
        R)
      (∏ j ∈ t \ {x}, s j : R)
have pos : Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
    (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
    (Exists.choose (p := Membership.mem t) h) =
  HMul.hMul (α := R) (β := R)
    (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
        (μ a * s (Exists.choose (p := Membership.mem t) h)) (Exists.choose (p := Membership.mem t) h) :
      R)
    (∏ j ∈ t \ {Exists.choose (p := Membership.mem t) h}, s j : R)
Tactic: rw [hx, Pi.single_eq_same, Pi.single_eq_same]