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

Proof state:
case refine_2
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
⊢ Pairwise (IsCoprime on fun i => s ↑i)

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

Result:
case refine_2.mk.mk
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
h : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ (IsCoprime on fun i => s ↑i) ⟨i, hi⟩ ⟨j, hj⟩

Proof state:
case refine_2.mk.mk
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
h : ⟨i, hi⟩ ≠ ⟨j, hj⟩
⊢ (IsCoprime on fun i => s ↑i) ⟨i, hi⟩ ⟨j, hj⟩

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

Result:
case refine_2.mk.mk.a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsCoprime (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:
case refine_2.mk.mk.a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsCoprime (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_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsCoprime on fun i => s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t \ {i}
⊢ IsCoprime (s i) (s j)

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

Result:
case refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsCoprime on fun i => s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t ∧ ¬j = i
⊢ IsCoprime (s i) (s j)

Proof state:
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
⊢ Pairwise (IsCoprime on fun i => s ↑i) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)

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

Result:
case refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsCoprime on fun i => s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t \ {i}
⊢ IsCoprime (s i) (s j)

case refine_2
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
⊢ Pairwise (IsCoprime on fun i => s ↑i)

Proof state:
case refine_1.intro
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsCoprime on fun i => s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
ji : ¬j = i
⊢ IsCoprime (s i) (s j)

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

Result:
no goals

Proof state:
case refine_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsCoprime on fun i => s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t ∧ ¬j = i
⊢ IsCoprime (s i) (s j)

Tactic:
obtain ⟨hj, ji⟩ := hj

Result:
case refine_1.intro
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : Pairwise (IsCoprime on fun i => s ↑i)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
ji : ¬j = i
⊢ IsCoprime (s i) (s j)