awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
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.insert a r) : Set I).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ Insert.insert a r, s i ∣ z
insert : s a * ∏ x ∈ r, s x ∣ z
⊢ ∏ x ∈ Insert.insert a r, s x ∣ z

Tactic:
rw [Finset.prod_insert har]

Premises used: Finset.prod_insert
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
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
⊢ s a * ∏ x ∈ r, s x ∣ z

Tactic:
IsCoprime.mul_dvd ?_ ?_ ?_

Premises used: IsCoprime.mul_dvd
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
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.insert a r) : Set I).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ Insert.insert a r, s i ∣ z
insert : IsCoprime (s a) (∏ x ∈ r, s x)
insert₁ : s a ∣ z
insert₂ : ∏ x ∈ r, s x ∣ z
⊢ s a * ∏ x ∈ r, s x ∣ z

Tactic:
refine IsCoprime.mul_dvd ?_ ?_ ?_

Premises used: IsCoprime.mul_dvd
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
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
⊢ IsCoprime (s a) (∏ x ∈ r, s x)

Tactic:
IsCoprime.prod_right fun i hir ↦ ?_

Premises used: IsCoprime.prod_right
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
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.insert a r) : Set I).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ Insert.insert a r, s i ∣ z
insert : ∀ (i : I) (hir : i ∈ r), IsCoprime (s a) (s i)
⊢ IsCoprime (s a) (∏ x ∈ r, s x)

Tactic:
refine IsCoprime.prod_right fun i hir ↦ ?_

Premises used: IsCoprime.prod_right
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
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
i : I
hir : i ∈ r
⊢ a ∈ (↑(insert a r) : Set I)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
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
i : I
hir : i ∈ r
⊢ i ∈ (↑(insert a r) : Set I)

Tactic:
simp [hir]
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
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
i : I
hir : i ∈ r
⊢ IsCoprime (s a) (s i)

Tactic:
exact Hs (by simp) (by simp [hir]) (ne_of_mem_of_not_mem hir har).symm

Premises used: Ne.symm, ne_of_mem_of_not_mem
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
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
⊢ s a ∣ z

Tactic:
Hs1 a (Finset.mem_insert_self a r)

Premises used: Finset.mem_insert_self
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
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
⊢ s a ∣ z

Tactic:
exact Hs1 a (Finset.mem_insert_self a r)

Premises used: Finset.mem_insert_self
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
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 ∈ r, s x ∣ z

Tactic:
ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi

Premises used: Set.Pairwise.mono, Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
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.insert a r) : Set I).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ Insert.insert a r, s i ∣ z
insert : (↑r : Set I) ⊆ (↑(Insert.insert a r) : Set I)
⊢ ∏ x ∈ r, s x ∣ z

Tactic:
refine ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi

Premises used: Set.Pairwise.mono, Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
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
⊢ (↑r : Set I) ⊆ (↑(insert a r) : Set I)

Tactic:
simp only [Finset.coe_insert, Set.subset_insert]

Premises used: Finset.coe_insert, Set.subset_insert
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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
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.insert a r) : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ i ∈ Insert.insert a r, s i ∣ z),
    ∏ x ∈ Insert.insert a r, s x ∣ z
⊢ ∏ x ∈ t, s x ∣ z

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

Premises used: IsCoprime.mul_dvd, Insert.insert, Finset.coe_insert, Set.subset_insert, IsCoprime.prod_right
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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
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.insert a r) : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ i ∈ Insert.insert a r, s i ∣ z),
    ∏ x ∈ Insert.insert a r, s x ∣ z
⊢ ∏ x ∈ t, 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]

Premises used: IsCoprime.mul_dvd, Insert.insert, Finset.coe_insert, Set.subset_insert, IsCoprime.prod_right
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
inst_1 : Fintype I
Hs : Pairwise (IsCoprime on s)
Hs1 : ∀ (i : I), s i ∣ z
⊢ ∏ x : I, s x ∣ z

Tactic:
Finset.prod_dvd_of_coprime (Hs.set_pairwise _) fun i _ ↦ Hs1 i

Premises used: Finset.prod_dvd_of_coprime, Pairwise.set_pairwise
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t : Finset I
inst_1 : DecidableEq I
a : I
⊢ (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ {a}, μ i * ∏ j ∈ {a} \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥{a}) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥{a}) ↦ s (↑i : I))

Tactic:
simp [exists_apply_eq, Pairwise, Function.onFun]

Premises used: Function.onFun, Pairwise, exists_apply_eq
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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))
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} (α := ↥(Finset.cons a t hat))
      (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥(Finset.cons a t hat)) ↦ s (↑i : I))

Tactic:
rw [pairwise_cons']

Premises used: Finset.pairwise_cons'
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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
rw : a ∈ insert a t ∧ ¬a = x
⊢ a ∈ insert a t \ {x}

Tactic:
rw [mem_sdiff, mem_singleton]

Premises used: Finset.mem_singleton, Finset.mem_sdiff
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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 ∧ ¬a = x

Tactic:
⟨mem_insert_self _ _, fun ha ↦ hat (ha ▸ hx)⟩

Premises used: Finset.mem_insert_self, Eq.rec, And.intro, Eq.symm
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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 ∧ ¬a = x

Tactic:
exact ⟨mem_insert_self _ _, fun ha ↦ hat (ha ▸ hx)⟩
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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 ∈ 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)⟩
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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)
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
⊢ (∃ (μ : 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)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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
⊢ μ 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μ

Premises used: Finset.sdiff_singleton_eq_erase, Finset.sum_cons, Finset.erase_insert, Finset.cons_eq_insert
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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)

Tactic:
⟨ih.mp ⟨Pi.single h.choose (μ a * s h.choose) + μ * fun _ ↦ s a, ?_⟩, fun b hb ↦ ?_⟩

Premises used: HMul.hMul, Pi.single, HAdd.hAdd, And.intro, Exists.intro, Iff.mp, Exists.choose
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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
cons₁ : ∀ (b : I) (hb : b ∈ t), IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
⊢ 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:
refine ⟨ih.mp ⟨Pi.single h.choose (μ a * s h.choose) + μ * fun _ ↦ s a, ?_⟩, fun b hb ↦ ?_⟩
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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
⊢ μ 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μ

Premises used: Exists.choose_spec, Finset.sum_add_distrib, mul_assoc, if_pos, Finset.prod_eq_mul_prod_diff_singleton_of_mem, Finset.sum_pi_single'
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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)
    (∑ 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μ

Premises used: Exists.choose_spec, Finset.sum_add_distrib, mul_assoc, if_pos, Finset.prod_eq_mul_prod_diff_singleton_of_mem, Finset.sum_pi_single'
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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
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)
⊢ 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:
rw [← hμ, sum_congr rfl]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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 (α := 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)
        (HMul.hMul (β := I → R) μ (fun (x : I) ↦ s a) x) *
      ∏ j ∈ t \ {x}, s j =
    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) +
      HMul.hMul (β := I → R) μ (fun (x : I) ↦ s a) x * ∏ j ∈ t \ {x}, s j

Tactic:
add_mul (R := R) _ _ _

Premises used: add_mul