M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ Stream'.nth a i * Stream'.nth a j ∈ FP (Stream'.drop i a)
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ Stream'.nth a i * Stream'.nth a j ∈ FP a
refine' FP_drop_subset_FP _ i _
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ Stream'.head (Stream'.drop i a) * Stream'.nth a j ∈ FP (Stream'.drop i a)
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ Stream'.nth a i * Stream'.nth a j ∈ FP (Stream'.drop i a)
rw [← Stream'.head_drop]
case h
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ FP (Stream'.tail (Stream'.drop i a)) (Stream'.nth a j)
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ Stream'.head (Stream'.drop i a) * Stream'.nth a j ∈ FP (Stream'.drop i a)
apply FP.cons
case h.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = Nat.succ i + d
⊢ FP (Stream'.tail (Stream'.drop i a)) (Stream'.nth a j)
case h
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ FP (Stream'.tail (Stream'.drop i a)) (Stream'.nth a j)
rcases le_iff_exists_add.mp (Nat.succ_le_of_lt ij) with ⟨d, hd⟩
case h.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = Nat.succ i + d
⊢ Stream'.nth a j ∈ FP (Stream'.tail (Stream'.drop i a))
case h.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = Nat.succ i + d
⊢ FP (Stream'.tail (Stream'.drop i a)) (Stream'.nth a j)
change _ ∈ FP _
case h.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = Nat.succ i + d
this : Stream'.nth (Stream'.tail (Stream'.drop i a)) d ∈ FP (Stream'.tail (Stream'.drop i a))
⊢ Stream'.nth a j ∈ FP (Stream'.tail (Stream'.drop i a))
case h.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = Nat.succ i + d
⊢ Stream'.nth a j ∈ FP (Stream'.tail (Stream'.drop i a))
have := FP.singleton (a.drop i).tail d
case h.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = Nat.succ i + d
this : Stream'.nth a (d + 1 + i) ∈ FP (Stream'.drop 1 (Stream'.drop i a))
⊢ Stream'.nth a j ∈ FP (Stream'.tail (Stream'.drop i a))
case h.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = Nat.succ i + d
this : Stream'.nth (Stream'.tail (Stream'.drop i a)) d ∈ FP (Stream'.tail (Stream'.drop i a))
⊢ Stream'.nth a j ∈ FP (Stream'.tail (Stream'.drop i a))
rw [Stream'.tail_eq_drop, Stream'.nth_drop, Stream'.nth_drop] at this
case h.e'_4.h.e'_3
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = Nat.succ i + d
this : Stream'.nth a (d + 1 + i) ∈ FP (Stream'.drop 1 (Stream'.drop i a))
⊢ j = d + 1 + i
case h.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = Nat.succ i + d
this : Stream'.nth a (d + 1 + i) ∈ FP (Stream'.drop 1 (Stream'.drop i a))
⊢ Stream'.nth a j ∈ FP (Stream'.tail (Stream'.drop i a))
convert this
no goals
case h.e'_4.h.e'_3
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = Nat.succ i + d
this : Stream'.nth a (d + 1 + i) ∈ FP (Stream'.drop 1 (Stream'.drop i a))
⊢ j = d + 1 + i
rw [hd, add_comm, Nat.succ_add, Nat.add_succ]