M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
hs : Finset.Nonempty s
⊢ (Finset.prod s fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' s hs) a)
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
hs : Finset.Nonempty s
⊢ (Finset.prod s fun i => Stream'.nth a i) ∈ FP a
refine' FP_drop_subset_FP _ (s.min' hs) _
case H
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
⊢ (Finset.prod s fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' s hs) a)
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
hs : Finset.Nonempty s
⊢ (Finset.prod s fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' s hs) a)
induction' s using Finset.strongInduction with s ih
case H
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
⊢ (Stream'.head (Stream'.drop (Finset.min' s hs) a) *
      Finset.prod (Finset.erase s (Finset.min' s hs)) fun x => Stream'.nth a x) ∈
    FP (Stream'.drop (Finset.min' s hs) a)
case H
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
⊢ (Finset.prod s fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' s hs) a)
rw [← Finset.mul_prod_erase _ _ (s.min'_mem hs), ← Stream'.head_drop]
case H.inl
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.erase s (Finset.min' s hs) = ∅
⊢ (Stream'.head (Stream'.drop (Finset.min' s hs) a) *
      Finset.prod (Finset.erase s (Finset.min' s hs)) fun x => Stream'.nth a x) ∈
    FP (Stream'.drop (Finset.min' s hs) a)

case H.inr
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
⊢ (Stream'.head (Stream'.drop (Finset.min' s hs) a) *
      Finset.prod (Finset.erase s (Finset.min' s hs)) fun x => Stream'.nth a x) ∈
    FP (Stream'.drop (Finset.min' s hs) a)
case H
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
⊢ (Stream'.head (Stream'.drop (Finset.min' s hs) a) *
      Finset.prod (Finset.erase s (Finset.min' s hs)) fun x => Stream'.nth a x) ∈
    FP (Stream'.drop (Finset.min' s hs) a)
cases' (s.erase (s.min' hs)).eq_empty_or_nonempty with h h
case H.inl
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.erase s (Finset.min' s hs) = ∅
⊢ Stream'.head (Stream'.drop (Finset.min' s hs) a) ∈ FP (Stream'.drop (Finset.min' s hs) a)
case H.inl
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.erase s (Finset.min' s hs) = ∅
⊢ (Stream'.head (Stream'.drop (Finset.min' s hs) a) *
      Finset.prod (Finset.erase s (Finset.min' s hs)) fun x => Stream'.nth a x) ∈
    FP (Stream'.drop (Finset.min' s hs) a)
rw [h, Finset.prod_empty, mul_one]
no goals
case H.inl
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.erase s (Finset.min' s hs) = ∅
⊢ Stream'.head (Stream'.drop (Finset.min' s hs) a) ∈ FP (Stream'.drop (Finset.min' s hs) a)
exact FP.head _
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
⊢ FP (Stream'.tail (Stream'.drop (Finset.min' s hs) a))
    (Finset.prod (Finset.erase s (Finset.min' s hs)) fun x => Stream'.nth a x)
case H.inr
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
⊢ (Stream'.head (Stream'.drop (Finset.min' s hs) a) *
      Finset.prod (Finset.erase s (Finset.min' s hs)) fun x => Stream'.nth a x) ∈
    FP (Stream'.drop (Finset.min' s hs) a)
apply FP.cons
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
⊢ FP (Stream'.drop (Finset.min' s hs + 1) a) (Finset.prod (Finset.erase s (Finset.min' s hs)) fun x => Stream'.nth a x)
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
⊢ FP (Stream'.tail (Stream'.drop (Finset.min' s hs) a))
    (Finset.prod (Finset.erase s (Finset.min' s hs)) fun x => Stream'.nth a x)
rw [Stream'.tail_eq_drop, Stream'.drop_drop, add_comm]
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
⊢ FP (Stream'.drop (Finset.min' (Finset.erase s (Finset.min' s hs)) h) a) ⊆ FP (Stream'.drop (Finset.min' s hs + 1) a)
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
⊢ FP (Stream'.drop (Finset.min' s hs + 1) a) (Finset.prod (Finset.erase s (Finset.min' s hs)) fun x => Stream'.nth a x)
refine' Set.mem_of_subset_of_mem _ (ih _ (Finset.erase_ssubset <| s.min'_mem hs) h)
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
this : Finset.min' s hs + 1 ≤ Finset.min' (Finset.erase s (Finset.min' s hs)) h
⊢ FP (Stream'.drop (Finset.min' (Finset.erase s (Finset.min' s hs)) h) a) ⊆ FP (Stream'.drop (Finset.min' s hs + 1) a)
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
⊢ FP (Stream'.drop (Finset.min' (Finset.erase s (Finset.min' s hs)) h) a) ⊆ FP (Stream'.drop (Finset.min' s hs + 1) a)
have : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h :=
  Nat.succ_le_of_lt (Finset.min'_lt_of_mem_erase_min' _ _ <| Finset.min'_mem _ _)
case H.inr.h.intro
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
this : Finset.min' s hs + 1 ≤ Finset.min' (Finset.erase s (Finset.min' s hs)) h
d : ℕ
hd : Finset.min' (Finset.erase s (Finset.min' s hs)) h = Finset.min' s hs + 1 + d
⊢ FP (Stream'.drop (Finset.min' (Finset.erase s (Finset.min' s hs)) h) a) ⊆ FP (Stream'.drop (Finset.min' s hs + 1) a)
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
this : Finset.min' s hs + 1 ≤ Finset.min' (Finset.erase s (Finset.min' s hs)) h
⊢ FP (Stream'.drop (Finset.min' (Finset.erase s (Finset.min' s hs)) h) a) ⊆ FP (Stream'.drop (Finset.min' s hs + 1) a)
cases' le_iff_exists_add.mp this with d hd
case H.inr.h.intro
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
this : Finset.min' s hs + 1 ≤ Finset.min' (Finset.erase s (Finset.min' s hs)) h
d : ℕ
hd : Finset.min' (Finset.erase s (Finset.min' s hs)) h = Finset.min' s hs + 1 + d
⊢ FP (Stream'.drop d (Stream'.drop (Finset.min' s hs + 1) a)) ⊆ FP (Stream'.drop (Finset.min' s hs + 1) a)
case H.inr.h.intro
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
this : Finset.min' s hs + 1 ≤ Finset.min' (Finset.erase s (Finset.min' s hs)) h
d : ℕ
hd : Finset.min' (Finset.erase s (Finset.min' s hs)) h = Finset.min' s hs + 1 + d
⊢ FP (Stream'.drop (Finset.min' (Finset.erase s (Finset.min' s hs)) h) a) ⊆ FP (Stream'.drop (Finset.min' s hs + 1) a)
rw [hd, add_comm, ← Stream'.drop_drop]
no goals
case H.inr.h.intro
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s✝ : Finset ℕ
hs✝ : Finset.Nonempty s✝
s : Finset ℕ
ih :
  ∀ (t : Finset ℕ),
    t ⊂ s →
      ∀ (hs : Finset.Nonempty t), (Finset.prod t fun i => Stream'.nth a i) ∈ FP (Stream'.drop (Finset.min' t hs) a)
hs : Finset.Nonempty s
h : Finset.Nonempty (Finset.erase s (Finset.min' s hs))
this : Finset.min' s hs + 1 ≤ Finset.min' (Finset.erase s (Finset.min' s hs)) h
d : ℕ
hd : Finset.min' (Finset.erase s (Finset.min' s hs)) h = Finset.min' s hs + 1 + d
⊢ FP (Stream'.drop d (Stream'.drop (Finset.min' s hs + 1) a)) ⊆ FP (Stream'.drop (Finset.min' s hs + 1) a)
apply FP_drop_subset_FP