-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem pairwise_isRelPrime_iff_isRelPrime_prod [DecidableEq I] :
    Pairwise (IsRelPrime on fun i : t ↦ s i) ↔ ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)

Proof state:
case refine_1
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsRelPrime on fun i => s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t \ {i}
⊢ IsRelPrime (s i) (s j)

Tactic:
rw [Finset.mem_sdiff, Finset.mem_singleton] at hj

Result:
case refine_1
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsRelPrime on fun i => s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t ∧ ¬j = i
⊢ IsRelPrime (s i) (s j)

Proof state:
case refine_2
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)
⊢ Pairwise (IsRelPrime on fun i => s ↑i)

Tactic:
rintro ⟨i, hi⟩ ⟨j, hj⟩ h

Result:
case refine_2.mk.mk
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
h : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ (IsRelPrime on fun i => s ↑i) ⟨i, hi⟩ ⟨j, hj⟩

Proof state:
case refine_1.intro
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsRelPrime on fun i => s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
ji : ¬j = i
⊢ IsRelPrime (s i) (s j)

Tactic:
exact @hp ⟨i, hi⟩ ⟨j, hj⟩ fun h ↦ ji (congrArg Subtype.val h).symm

Result:
no goals

Proof state:
case refine_1
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsRelPrime on fun i => s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t ∧ ¬j = i
⊢ IsRelPrime (s i) (s j)

Tactic:
obtain ⟨hj, ji⟩ := hj

Result:
case refine_1.intro
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsRelPrime on fun i => s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
ji : ¬j = i
⊢ IsRelPrime (s i) (s j)

Proof state:
case refine_2.mk.mk.a
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
h : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ ↑⟨j, hj⟩ ∈ t \ {i}

Tactic:
exact Finset.mem_sdiff.mpr ⟨hj, fun f ↦ h <| Subtype.ext (Finset.mem_singleton.mp f).symm⟩

Result:
no goals

Proof state:
case refine_2.mk.mk
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
h : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ (IsRelPrime on fun i => s ↑i) ⟨i, hi⟩ ⟨j, hj⟩

Tactic:
apply IsRelPrime.prod_right_iff.mp (hp i hi)

Result:
case refine_2.mk.mk.a
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
h : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ ↑⟨j, hj⟩ ∈ t \ {i}

Proof state:
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
⊢ Pairwise (IsRelPrime on fun i => s ↑i) ↔ ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)

Tactic:
refine ⟨fun hp i hi ↦ IsRelPrime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩

Result:
case refine_1
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsRelPrime on fun i => s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t \ {i}
⊢ IsRelPrime (s i) (s j)

case refine_2
α : Type u_2
I : Type u_1
inst✝² : CommMonoid α
inst✝¹ : DecompositionMonoid α
s : I → α
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)
⊢ Pairwise (IsRelPrime on fun i => s ↑i)