-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem exists_sum_eq_one_iff_pairwise_coprime [DecidableEq I] (h : t.Nonempty) :
    (∃ μ : I → R, (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) = 1) ↔
      Pairwise (IsCoprime on fun i : t ↦ s i)

Proof state:
case cons.mp.intro.refine_2.refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑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
b : I
hb : b ∈ t
x : I
hx : x ∈ t
⊢ μ x * ((∏ j ∈ t \ {x}, s j) * s a) = μ x * ∏ j ∈ insert a t \ {x}, s j

Tactic:
congr

Result:
case cons.mp.intro.refine_2.refine_1.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑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
b : I
hb : b ∈ t
x : I
hx : x ∈ t
⊢ (∏ j ∈ t \ {x}, s j) * s a = ∏ j ∈ insert a t \ {x}, s j

Proof state:
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
x : I
hx : x ∈ t
⊢ a ∈ insert a t \ {x}

Tactic:
rw [mem_sdiff, mem_singleton]

Result:
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
x : I
hx : x ∈ t
⊢ a ∈ insert a t ∧ ¬a = x

Proof state:
case cons.mp.intro
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1
⊢ Pairwise (IsCoprime on fun a => s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)

Tactic:
rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat] at hμ

Result:
case cons.mp.intro
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑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 (IsCoprime on fun a => s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)

Proof state:
case cons
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
⊢ (∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1) ↔
    Pairwise (IsCoprime on fun a => s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)

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)⟩

Result:
case cons
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
⊢ (∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1) ↔
    Pairwise (IsCoprime on fun a => s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)

Proof state:
case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
⊢ (fun i => if i = a then u else v * μ i) a * ∏ j ∈ t, s j +
      ∑ x ∈ t, (fun i => if i = a then u else v * μ i) x * ∏ j ∈ insert a t \ {x}, s j =
    1

Tactic:
simp only [↓reduceIte, ite_mul]

Result:
case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
⊢ (u * ∏ j ∈ t, s j +
      ∑ x ∈ t, if x = a then u * ∏ j ∈ insert a t \ {x}, s j else v * μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1

Proof state:
case cons.mp.intro.refine_1.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ μ x * s a * ∏ j ∈ t \ {x}, s j = μ x * ∏ j ∈ insert a t \ {x}, s j

Tactic:
rw [mul_assoc]

Result:
case cons.mp.intro.refine_1.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ μ x * (s a * ∏ j ∈ t \ {x}, s j) = μ x * ∏ j ∈ insert a t \ {x}, s j