-- Mathlib/Combinatorics/Hindman.lean
theorem FP.mul {M} [Semigroup M] {a : Stream' M} {m : M} (hm : m ∈ FP a) :
    ∃ n, ∀ m' ∈ FP (a.drop n), m * m' ∈ FP a

Proof state:
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
m : M
hm : m ∈ FP a
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), m * m' ∈ FP a

Tactic:
induction hm with
| head a => exact ⟨1, fun m hm => FP.cons a m hm⟩
| tail a m _ ih =>
  obtain ⟨n, hn⟩ := ih
  use n + 1
  intro m' hm'
  exact FP.tail _ _ (hn _ hm')
| cons a m _ ih =>
  obtain ⟨n, hn⟩ := ih
  use n + 1
  intro m' hm'
  rw [mul_assoc]
  exact FP.cons _ _ (hn _ hm')

Result:
no goals

Proof state:
case cons.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), a.head * m * m' ∈ FP a

Tactic:
use n + 1

Result:
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∀ m' ∈ FP (Stream'.drop (n + 1) a), a.head * m * m' ∈ FP a

Proof state:
case cons
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
ih : ∃ n, ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), a.head * m * m' ∈ FP a

Tactic:
obtain ⟨n, hn⟩ := ih

Result:
case cons.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), a.head * m * m' ∈ FP a

Proof state:
case head
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m : M
a : Stream' M
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), a.head * m' ∈ FP a

Tactic:
exact ⟨1, fun m hm => FP.cons a m hm⟩

Result:
no goals

Proof state:
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ a.head * m * m' ∈ FP a

Tactic:
rw [mul_assoc]

Result:
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ a.head * (m * m') ∈ FP a

Proof state:
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ a.head * (m * m') ∈ FP a

Tactic:
exact FP.cons _ _ (hn _ hm')

Result:
no goals

Proof state:
case tail.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), m * m' ∈ FP a

Tactic:
use n + 1

Result:
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∀ m' ∈ FP (Stream'.drop (n + 1) a), m * m' ∈ FP a

Proof state:
case tail
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
ih : ∃ n, ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), m * m' ∈ FP a

Tactic:
obtain ⟨n, hn⟩ := ih

Result:
case tail.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), m * m' ∈ FP a

Proof state:
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∀ m' ∈ FP (Stream'.drop (n + 1) a), m * m' ∈ FP a

Tactic:
intro m' hm'

Result:
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ m * m' ∈ FP a

Proof state:
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ m * m' ∈ FP a

Tactic:
exact FP.tail _ _ (hn _ hm')

Result:
no goals

Proof state:
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∀ m' ∈ FP (Stream'.drop (n + 1) a), a.head * m * m' ∈ FP a

Tactic:
intro m' hm'

Result:
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ a.head * m * m' ∈ FP a