-- 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
h : t.Nonempty
singleton :
  ∀ (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))
cons :
  ∀ (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 ∈ 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))
⊢ (∃ (μ : 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))

Tactic:
induction h using Finset.Nonempty.cons_induction with
  | singleton =>
    simp [exists_apply_eq, Pairwise, Function.onFun]
  | cons a t hat h ih =>
    rw [pairwise_cons']
    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)⟩
    constructor
    · rintro ⟨μ, hμ⟩
      rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat] at hμ
      refine ⟨ih.mp ⟨Pi.single h.choose (μ a * s h.choose) + μ * fun _ ↦ s a, ?_⟩, fun b hb ↦ ?_⟩
      · 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μ
        rw [← hμ, sum_congr rfl]
        intro x hx
        convert! add_mul (R := R) _ _ _ using 2
        · by_cases hx : x = h.choose
          · rw [hx, Pi.single_eq_same, Pi.single_eq_same]
          · rw [Pi.single_eq_of_ne hx, Pi.single_eq_of_ne hx, zero_mul]
        · convert! (mul_assoc _ _ _).symm
          rw [prod_eq_prod_diff_singleton_mul (mem x hx), mul_comm, sdiff_sdiff_comm,
            sdiff_singleton_eq_erase a, erase_insert hat]
      · have : IsCoprime (s b) (s a) :=
          ⟨μ a * ∏ i ∈ t \ {b}, s i, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j, ?_⟩
        · exact ⟨this.symm, this⟩
        rw [mul_assoc, ← prod_eq_prod_diff_singleton_mul hb, sum_mul, ← hμ, sum_congr rfl]
        intro x hx
        rw [mul_assoc]
        congr
        rw [prod_eq_prod_diff_singleton_mul (mem x hx) _]
        congr 2
        rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]
    · rintro ⟨hs, Hb⟩
      obtain ⟨μ, hμ⟩ := ih.mpr hs
      obtain ⟨u, v, huv⟩ := IsCoprime.prod_left fun b hb ↦ (Hb b hb).right
      use fun i ↦ if i = a then u else v * μ i
      have hμ' : (∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a)) = v * s a := by
        rw [← mul_sum, ← sum_mul, hμ, one_mul]
      rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat]
      simp only [↓reduceIte, ite_mul]
      rw [← huv, ← hμ', sum_congr rfl]
      intro x hx
      rw [mul_assoc, if_neg fun ha : x = a ↦ hat (ha.casesOn hx)]
      rw [mul_assoc]
      congr
      rw [prod_eq_prod_diff_singleton_mul (mem x hx) _]
      congr 2
      rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]

Premises used: add_mul, Exists.choose_spec, Finset.sdiff_singleton_eq_erase, sdiff_sdiff_comm, Finset.sum_cons, Function.onFun, Finset.cons, Finset.sum_add_distrib, MulZeroClass.zero_mul, mul_assoc, Finset.pairwise_cons', if_pos, Finset.prod_eq_mul_prod_diff_singleton_of_mem, ite_mul, Finset.cons_eq_insert, Finset.sum_pi_single', Pairwise, mul_comm, reduceIte, Exists.choose, exists_apply_eq, Pi.single_eq_same, Singleton.singleton, Eq.symm, Finset.sum_congr, rfl, Finset.sum_mul