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

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

case cons
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
ih : ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n a) → Stream'.head a * m * m' ∈ FP a
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
m : M
hm : m ∈ FP a
⊢ ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n a) → m * m' ∈ FP a
induction' hm with a a m hm ih a m hm ih
no goals
case head
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m : M
a : Stream' M
⊢ ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n a) → Stream'.head a * m' ∈ FP a
exact ⟨1, fun m hm => FP.cons a m hm⟩
case tail.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n a) → m * m' ∈ FP a
case tail
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
ih : ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n a) → m * m' ∈ FP a
cases' ih with n hn
case tail.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∀ (m' : M), m' ∈ FP (Stream'.drop (n + 1) a) → m * m' ∈ FP a
case tail.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n a) → m * m' ∈ FP a
use n + 1
case tail.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ m * m' ∈ FP a
case tail.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∀ (m' : M), m' ∈ FP (Stream'.drop (n + 1) a) → m * m' ∈ FP a
intro m' hm'
no goals
case tail.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ m * m' ∈ FP a
exact FP.tail _ _ (hn _ hm')
case cons.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n a) → Stream'.head a * m * m' ∈ FP a
case cons
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
ih : ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n a) → Stream'.head a * m * m' ∈ FP a
cases' ih with n hn
case cons.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∀ (m' : M), m' ∈ FP (Stream'.drop (n + 1) a) → Stream'.head a * m * m' ∈ FP a
case cons.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∃ n, ∀ (m' : M), m' ∈ FP (Stream'.drop n a) → Stream'.head a * m * m' ∈ FP a
use n + 1
case cons.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ Stream'.head a * m * m' ∈ FP a
case cons.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
⊢ ∀ (m' : M), m' ∈ FP (Stream'.drop (n + 1) a) → Stream'.head a * m * m' ∈ FP a
intro m' hm'
case cons.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ Stream'.head a * (m * m') ∈ FP a
case cons.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ Stream'.head a * m * m' ∈ FP a
rw [mul_assoc]
no goals
case cons.intro
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
hm : FP (Stream'.tail a) m
n : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n (Stream'.tail a)) → m * m' ∈ FP (Stream'.tail a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ Stream'.head a * (m * m') ∈ FP a
exact FP.cons _ _ (hn _ hm')