case refine'_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : 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
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ (i : I), i ∈ t → IsCoprime (s i) (∏ j in t \ {i}, s j)
⊢ Pairwise (IsCoprime on fun i => s ↑i)
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
⊢ Pairwise (IsCoprime on fun i => s ↑i) ↔ ∀ (i : I), i ∈ t → IsCoprime (s i) (∏ j in t \ {i}, s j)
refine' ⟨fun hp i hi ↦ IsCoprime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩
case refine'_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : 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)
case refine'_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : 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)
rw [Finset.mem_sdiff, Finset.mem_singleton] at hj
case refine'_1.intro
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : 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)
case refine'_1
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : 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)
obtain ⟨hj, ji⟩ := hj
no goals
case refine'_1.intro
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : 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)
refine @hp ⟨i, hi⟩ ⟨j, hj⟩ fun h ↦ ji (congrArg Subtype.val h).symm
case refine'_2.mk.mk
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ (i : I), i ∈ t → IsCoprime (s i) (∏ j in t \ {i}, s j)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
h : { val := i, property := hi } ≠ { val := j, property := hj }
⊢ (IsCoprime on fun i => s ↑i) { val := i, property := hi } { val := j, property := hj }
case refine'_2
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ (i : I), i ∈ t → IsCoprime (s i) (∏ j in t \ {i}, s j)
⊢ Pairwise (IsCoprime on fun i => s ↑i)
rintro ⟨i, hi⟩ ⟨j, hj⟩ h
case refine'_2.mk.mk.a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ (i : I), i ∈ t → IsCoprime (s i) (∏ j in t \ {i}, s j)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
h : { val := i, property := hi } ≠ { val := j, property := hj }
⊢ ↑{ val := j, property := hj } ∈ t \ {i}
case refine'_2.mk.mk
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ (i : I), i ∈ t → IsCoprime (s i) (∏ j in t \ {i}, s j)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
h : { val := i, property := hi } ≠ { val := j, property := hj }
⊢ (IsCoprime on fun i => s ↑i) { val := i, property := hi } { val := j, property := hj }
apply IsCoprime.prod_right_iff.mp (hp i hi)
no goals
case refine'_2.mk.mk.a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
x y z : R
s : I → R
t : Finset I
inst✝ : DecidableEq I
hp : ∀ (i : I), i ∈ t → IsCoprime (s i) (∏ j in t \ {i}, s j)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
h : { val := i, property := hi } ≠ { val := j, property := hj }
⊢ ↑{ val := j, property := hj } ∈ t \ {i}
exact Finset.mem_sdiff.mpr ⟨hj, fun f ↦ h <| Subtype.ext (Finset.mem_singleton.mp f).symm⟩