-- Mathlib/Combinatorics/Hindman.lean
theorem FP.finset_prod {M} [CommMonoid M] (a : Stream' M) (s : Finset ℕ) (hs : s.Nonempty) :
    (s.prod fun i => a.get i) ∈ FP a

Proof state:
case H
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
rcases (s.erase (s.min' hs)).eq_empty_or_nonempty with h | h

Result:
case H.inl
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : s.erase (s.min' hs) = ∅
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)

case H.inr
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)

Proof state:
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)

Tactic:
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 _ _)

Result:
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
this : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h
⊢ FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)

Proof state:
case H.inr.h.intro
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
this : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h
d : ℕ
hd : (s.erase (s.min' hs)).min' h = s.min' hs + 1 + d
⊢ FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)

Tactic:
rw [hd, ← Stream'.drop_drop, add_comm]

Result:
case H.inr.h.intro
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
this : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h
d : ℕ
hd : (s.erase (s.min' hs)).min' h = s.min' hs + 1 + d
⊢ FP (Stream'.drop d (Stream'.drop (1 + s.min' hs) a)) ⊆ FP (Stream'.drop (1 + s.min' hs) a)

Proof state:
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ FP (Stream'.drop (s.min' hs) a).tail (∏ x ∈ s.erase (s.min' hs), a.get x)

Tactic:
rw [Stream'.tail_eq_drop, Stream'.drop_drop, add_comm]

Result:
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ FP (Stream'.drop (1 + s.min' hs) a) (∏ x ∈ s.erase (s.min' hs), a.get x)

Proof state:
case H.inr
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
apply FP.cons

Result:
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ FP (Stream'.drop (s.min' hs) a).tail (∏ x ∈ s.erase (s.min' hs), a.get x)

Proof state:
case H.inr.h.intro
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
this : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h
d : ℕ
hd : (s.erase (s.min' hs)).min' h = s.min' hs + 1 + d
⊢ FP (Stream'.drop d (Stream'.drop (1 + s.min' hs) a)) ⊆ FP (Stream'.drop (1 + s.min' hs) a)

Tactic:
apply FP_drop_subset_FP

Result:
no goals

Proof state:
case H.inl
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : s.erase (s.min' hs) = ∅
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
rw [h, Finset.prod_empty, mul_one]

Result:
case H.inl
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : s.erase (s.min' hs) = ∅
⊢ (Stream'.drop (s.min' hs) a).head ∈ FP (Stream'.drop (s.min' hs) a)

Proof state:
case H.inl
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : s.erase (s.min' hs) = ∅
⊢ (Stream'.drop (s.min' hs) a).head ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
exact FP.head _

Result:
no goals

Proof state:
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ FP (Stream'.drop (1 + s.min' hs) a) (∏ x ∈ s.erase (s.min' hs), a.get x)

Tactic:
refine Set.mem_of_subset_of_mem ?_ (ih _ (Finset.erase_ssubset <| s.min'_mem hs) h)

Result:
case H.inr.h
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
hs : s.Nonempty
⊢ ∏ i ∈ s, a.get i ∈ FP a

Tactic:
refine FP_drop_subset_FP _ (s.min' hs) ?_

Result:
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
hs : s.Nonempty
⊢ ∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)

Proof state:
case H
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
⊢ ∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
rw [← Finset.mul_prod_erase _ _ (s.min'_mem hs), ← Stream'.head_drop]

Result:
case H
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)
hs : s.Nonempty
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)