[GOAL]
M : Type ?u.870
inst✝ : Semigroup M
src✝ : Mul (Ultrafilter M) := mul
U V W : Ultrafilter M
p : M → Prop
⊢ (∀ᶠ (x : M) in ↑(U * V * W), p x) ↔ ∀ᶠ (x : M) in ↑(U * (V * W)), p x
[PROOFSTEP]
simp_rw [Ultrafilter.eventually_mul, mul_assoc]
[GOAL]
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
[PROOFSTEP]
induction' hm with a a m hm ih a m hm ih
[GOAL]
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
[PROOFSTEP]
exact ⟨1, fun m hm => FP.cons a m hm⟩
[GOAL]
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
[PROOFSTEP]
cases' ih with n hn
[GOAL]
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
[PROOFSTEP]
use n + 1
[GOAL]
case h
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
[PROOFSTEP]
intro m' hm'
[GOAL]
case h
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
[PROOFSTEP]
exact FP.tail _ _ (hn _ hm')
[GOAL]
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
[PROOFSTEP]
cases' ih with n hn
[GOAL]
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
[PROOFSTEP]
use n + 1
[GOAL]
case h
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
[PROOFSTEP]
intro m' hm'
[GOAL]
case h
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
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case h
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
[PROOFSTEP]
exact FP.cons _ _ (hn _ hm')
[GOAL]
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a
[PROOFSTEP]
let S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ m in U, m ∈ FP (a.drop n)}
[GOAL]
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a
[PROOFSTEP]
have h := exists_idempotent_in_compact_subsemigroup ?_ S ?_ ?_ ?_
[GOAL]
case refine_5
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
h : ∃ m, m ∈ S ∧ m * m = m
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a
[PROOFSTEP]
rcases h with ⟨U, hU, U_idem⟩
[GOAL]
case refine_5.intro.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : U ∈ S
U_idem : U * U = U
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a
[PROOFSTEP]
refine' ⟨U, U_idem, _⟩
[GOAL]
case refine_5.intro.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : U ∈ S
U_idem : U * U = U
⊢ ∀ᶠ (m : M) in ↑U, m ∈ FP a
[PROOFSTEP]
convert Set.mem_iInter.mp hU 0
[GOAL]
case refine_1
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∀ (r : Ultrafilter M), Continuous fun x => x * r
[PROOFSTEP]
exact Ultrafilter.continuous_mul_left
[GOAL]
case refine_2
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ Set.Nonempty S
[PROOFSTEP]
apply IsCompact.nonempty_iInter_of_sequence_nonempty_compact_closed
[GOAL]
case refine_2.hZd
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∀ (i : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (i + 1) a)} ⊆ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
[PROOFSTEP]
intro n U hU
[GOAL]
case refine_2.hZd
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
hU : U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)}
⊢ U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
[PROOFSTEP]
apply Eventually.mono hU
[GOAL]
case refine_2.hZd
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
hU : U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)}
⊢ ∀ (x : M), x ∈ FP (Stream'.drop (n + 1) a) → x ∈ FP (Stream'.drop n a)
[PROOFSTEP]
rw [add_comm, ← Stream'.drop_drop, ← Stream'.tail_eq_drop]
[GOAL]
case refine_2.hZd
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
hU : U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop (n + 1) a)}
⊢ ∀ (x : M), x ∈ FP (Stream'.tail (Stream'.drop n a)) → x ∈ FP (Stream'.drop n a)
[PROOFSTEP]
exact FP.tail _
[GOAL]
case refine_2.hZn
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∀ (i : ℕ), Set.Nonempty {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
[PROOFSTEP]
intro n
[GOAL]
case refine_2.hZn
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
⊢ Set.Nonempty {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
[PROOFSTEP]
exact ⟨pure _, mem_pure.mpr <| FP.head _⟩
[GOAL]
case refine_2.hZ0
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ IsCompact {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop 0 a)}
[PROOFSTEP]
exact (ultrafilter_isClosed_basic _).isCompact
[GOAL]
case refine_2.hZcl
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∀ (i : ℕ), IsClosed {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
[PROOFSTEP]
intro n
[GOAL]
case refine_2.hZcl
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
⊢ IsClosed {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
[PROOFSTEP]
apply ultrafilter_isClosed_basic
[GOAL]
case refine_3
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ IsCompact S
[PROOFSTEP]
exact IsClosed.isCompact (isClosed_iInter fun i => ultrafilter_isClosed_basic _)
[GOAL]
case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∀ (x : Ultrafilter M), x ∈ S → ∀ (y : Ultrafilter M), y ∈ S → x * y ∈ S
[PROOFSTEP]
intro U hU V hV
[GOAL]
case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : U ∈ S
V : Ultrafilter M
hV : V ∈ S
⊢ U * V ∈ S
[PROOFSTEP]
rw [Set.mem_iInter] at *
[GOAL]
case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
⊢ ∀ (i : ℕ), U * V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
[PROOFSTEP]
intro n
[GOAL]
case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
⊢ U * V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
[PROOFSTEP]
rw [Set.mem_setOf_eq, Ultrafilter.eventually_mul]
[GOAL]
case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
⊢ ∀ᶠ (m : M) in ↑U, ∀ᶠ (m' : M) in ↑V, m * m' ∈ FP (Stream'.drop n a)
[PROOFSTEP]
apply Eventually.mono (hU n)
[GOAL]
case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
⊢ ∀ (x : M), x ∈ FP (Stream'.drop n a) → ∀ᶠ (m' : M) in ↑V, x * m' ∈ FP (Stream'.drop n a)
[PROOFSTEP]
intro m hm
[GOAL]
case refine_4
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
⊢ ∀ᶠ (m' : M) in ↑V, m * m' ∈ FP (Stream'.drop n a)
[PROOFSTEP]
obtain ⟨n', hn⟩ := FP.mul hm
[GOAL]
case refine_4.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
n' : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n' (Stream'.drop n a)) → m * m' ∈ FP (Stream'.drop n a)
⊢ ∀ᶠ (m' : M) in ↑V, m * m' ∈ FP (Stream'.drop n a)
[PROOFSTEP]
apply Eventually.mono (hV (n' + n))
[GOAL]
case refine_4.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
n' : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n' (Stream'.drop n a)) → m * m' ∈ FP (Stream'.drop n a)
⊢ ∀ (x : M), x ∈ FP (Stream'.drop (n' + n) a) → m * x ∈ FP (Stream'.drop n a)
[PROOFSTEP]
intro m' hm'
[GOAL]
case refine_4.intro
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
n' : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n' (Stream'.drop n a)) → m * m' ∈ FP (Stream'.drop n a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n' + n) a)
⊢ m * m' ∈ FP (Stream'.drop n a)
[PROOFSTEP]
apply hn
[GOAL]
case refine_4.intro.a
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
n' : ℕ
hn : ∀ (m' : M), m' ∈ FP (Stream'.drop n' (Stream'.drop n a)) → m * m' ∈ FP (Stream'.drop n a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n' + n) a)
⊢ m' ∈ FP (Stream'.drop n' (Stream'.drop n a))
[PROOFSTEP]
simpa only [Stream'.drop_drop] using hm'
[GOAL]
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
⊢ ∃ a, FP a ⊆ s₀
[PROOFSTEP]
have exists_elem : ∀ {s : Set M} (_hs : s ∈ U), (s ∩ {m | ∀ᶠ m' in U, m * m' ∈ s}).Nonempty := fun {s} hs =>
  Ultrafilter.nonempty_of_mem (inter_mem hs <| by rwa [← U_idem] at hs )
[GOAL]
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
s : Set M
hs : s ∈ U
⊢ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s} ∈ ↑U
[PROOFSTEP]
rwa [← U_idem] at hs 
[GOAL]
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
⊢ ∃ a, FP a ⊆ s₀
[PROOFSTEP]
let elem : { s // s ∈ U } → M := fun p => (exists_elem p.property).some
[GOAL]
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
⊢ ∃ a, FP a ⊆ s₀
[PROOFSTEP]
let succ : { s // s ∈ U } → { s // s ∈ U } := fun (p : { s // s ∈ U }) =>
  ⟨p.val ∩ {m : M | elem p * m ∈ p.val},
    inter_mem p.property
      (show (exists_elem p.property).some ∈ {m : M | ∀ᶠ (m' : M) in ↑U, m * m' ∈ p.val} from
        p.val.inter_subset_right {m : M | ∀ᶠ (m' : M) in ↑U, m * m' ∈ p.val} (exists_elem p.property).some_mem)⟩
[GOAL]
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
⊢ ∃ a, FP a ⊆ s₀
[PROOFSTEP]
use Stream'.corec elem succ (Subtype.mk s₀ sU)
[GOAL]
case h
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
⊢ FP (Stream'.corec elem succ { val := s₀, property := sU }) ⊆ s₀
[PROOFSTEP]
suffices ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ p, a = Stream'.corec elem succ p → m ∈ p.val
  by
  intro m hm
  exact this _ m hm ⟨s₀, sU⟩ rfl
[GOAL]
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
this : ∀ (a : Stream' M) (m : M), m ∈ FP a → ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
⊢ FP (Stream'.corec elem succ { val := s₀, property := sU }) ⊆ s₀
[PROOFSTEP]
intro m hm
[GOAL]
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
this : ∀ (a : Stream' M) (m : M), m ∈ FP a → ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
m : M
hm : m ∈ FP (Stream'.corec elem succ { val := s₀, property := sU })
⊢ m ∈ s₀
[PROOFSTEP]
exact this _ m hm ⟨s₀, sU⟩ rfl
[GOAL]
case h
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
⊢ ∀ (a : Stream' M) (m : M), m ∈ FP a → ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
[PROOFSTEP]
clear sU s₀
[GOAL]
case h
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
⊢ ∀ (a : Stream' M) (m : M), m ∈ FP a → ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
[PROOFSTEP]
intro a m h
[GOAL]
case h
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m : M
h : m ∈ FP a
⊢ ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
[PROOFSTEP]
induction' h with b b n h ih b n h ih
[GOAL]
case h.head
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m : M
b : Stream' M
⊢ ∀ (p : { s // s ∈ U }), b = Stream'.corec elem succ p → Stream'.head b ∈ ↑p
[PROOFSTEP]
rintro p rfl
[GOAL]
case h.head
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m : M
p : { s // s ∈ U }
⊢ Stream'.head (Stream'.corec elem succ p) ∈ ↑p
[PROOFSTEP]
rw [Stream'.corec_eq, Stream'.head_cons]
[GOAL]
case h.head
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m : M
p : { s // s ∈ U }
⊢ elem p ∈ ↑p
[PROOFSTEP]
exact Set.inter_subset_left _ _ (Set.Nonempty.some_mem _)
[GOAL]
case h.tail
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m : M
b : Stream' M
n : M
h : FP (Stream'.tail b) n
ih : ∀ (p : { s // s ∈ U }), Stream'.tail b = Stream'.corec elem succ p → n ∈ ↑p
⊢ ∀ (p : { s // s ∈ U }), b = Stream'.corec elem succ p → n ∈ ↑p
[PROOFSTEP]
rintro p rfl
[GOAL]
case h.tail
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.tail (Stream'.corec elem succ p)) n
ih : ∀ (p_1 : { s // s ∈ U }), Stream'.tail (Stream'.corec elem succ p) = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ n ∈ ↑p
[PROOFSTEP]
refine' Set.inter_subset_left _ _ (ih (succ p) _)
[GOAL]
case h.tail
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.tail (Stream'.corec elem succ p)) n
ih : ∀ (p_1 : { s // s ∈ U }), Stream'.tail (Stream'.corec elem succ p) = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ Stream'.tail (Stream'.corec elem succ p) = Stream'.corec elem succ (succ p)
[PROOFSTEP]
rw [Stream'.corec_eq, Stream'.tail_cons]
[GOAL]
case h.cons
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m : M
b : Stream' M
n : M
h : FP (Stream'.tail b) n
ih : ∀ (p : { s // s ∈ U }), Stream'.tail b = Stream'.corec elem succ p → n ∈ ↑p
⊢ ∀ (p : { s // s ∈ U }), b = Stream'.corec elem succ p → Stream'.head b * n ∈ ↑p
[PROOFSTEP]
rintro p rfl
[GOAL]
case h.cons
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.tail (Stream'.corec elem succ p)) n
ih : ∀ (p_1 : { s // s ∈ U }), Stream'.tail (Stream'.corec elem succ p) = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ Stream'.head (Stream'.corec elem succ p) * n ∈ ↑p
[PROOFSTEP]
have := Set.inter_subset_right _ _ (ih (succ p) ?_)
[GOAL]
case h.cons.refine_2
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.tail (Stream'.corec elem succ p)) n
ih : ∀ (p_1 : { s // s ∈ U }), Stream'.tail (Stream'.corec elem succ p) = Stream'.corec elem succ p_1 → n ∈ ↑p_1
this : n ∈ {m | elem p * m ∈ ↑p}
⊢ Stream'.head (Stream'.corec elem succ p) * n ∈ ↑p
[PROOFSTEP]
simpa only using this
[GOAL]
case h.cons.refine_1
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → Set.Nonempty (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s})
elem : { s // s ∈ U } → M := fun p => Set.Nonempty.some (_ : Set.Nonempty (↑p ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ ↑p}))
succ : { s // s ∈ U } → { s // s ∈ U } :=
  fun p => { val := ↑p ∩ {m | elem p * m ∈ ↑p}, property := (_ : ↑p ∩ {m | elem p * m ∈ ↑p} ∈ ↑U) }
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.tail (Stream'.corec elem succ p)) n
ih : ∀ (p_1 : { s // s ∈ U }), Stream'.tail (Stream'.corec elem succ p) = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ Stream'.tail (Stream'.corec elem succ p) = Stream'.corec elem succ (succ p)
[PROOFSTEP]
rw [Stream'.corec_eq, Stream'.tail_cons]
[GOAL]
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
⊢ FP (Stream'.drop n a) ⊆ FP a
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ FP (Stream'.drop Nat.zero a) ⊆ FP a
[PROOFSTEP]
rfl
[GOAL]
case succ
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop (Nat.succ n) a) ⊆ FP a
[PROOFSTEP]
rw [Nat.succ_eq_one_add, ← Stream'.drop_drop]
[GOAL]
case succ
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop 1 (Stream'.drop n a)) ⊆ FP a
[PROOFSTEP]
exact _root_.trans (FP.tail _) ih
[GOAL]
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i : ℕ
⊢ Stream'.nth a i ∈ FP a
[PROOFSTEP]
induction' i with i ih generalizing a
[GOAL]
case zero
M : Type u_1
inst✝ : Semigroup M
a✝ a : Stream' M
⊢ Stream'.nth a Nat.zero ∈ FP a
[PROOFSTEP]
apply FP.head
[GOAL]
case succ
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
i : ℕ
ih : ∀ (a : Stream' M), Stream'.nth a i ∈ FP a
a : Stream' M
⊢ Stream'.nth a (Nat.succ i) ∈ FP a
[PROOFSTEP]
apply FP.tail
[GOAL]
case succ.h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
i : ℕ
ih : ∀ (a : Stream' M), Stream'.nth a i ∈ FP a
a : Stream' M
⊢ FP (Stream'.tail a) (Stream'.nth a (Nat.succ i))
[PROOFSTEP]
apply ih
[GOAL]
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
[PROOFSTEP]
refine' FP_drop_subset_FP _ i _
[GOAL]
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)
[PROOFSTEP]
rw [← Stream'.head_drop]
[GOAL]
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)
[PROOFSTEP]
apply FP.cons
[GOAL]
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)
[PROOFSTEP]
rcases le_iff_exists_add.mp (Nat.succ_le_of_lt ij) with
  ⟨d, hd⟩
    -- Porting note: need to fix breakage of Set notation
[GOAL]
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)
[PROOFSTEP]
change _ ∈ FP _
[GOAL]
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))
[PROOFSTEP]
have := FP.singleton (a.drop i).tail d
[GOAL]
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))
[PROOFSTEP]
rw [Stream'.tail_eq_drop, Stream'.nth_drop, Stream'.nth_drop] at this 
[GOAL]
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))
[PROOFSTEP]
convert this
[GOAL]
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
[PROOFSTEP]
rw [hd, add_comm, Nat.succ_add, Nat.add_succ]
[GOAL]
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
[PROOFSTEP]
refine' FP_drop_subset_FP _ (s.min' hs) _
[GOAL]
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)
[PROOFSTEP]
induction' s using Finset.strongInduction with s ih
[GOAL]
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)
[PROOFSTEP]
rw [← Finset.mul_prod_erase _ _ (s.min'_mem hs), ← Stream'.head_drop]
[GOAL]
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)
[PROOFSTEP]
cases' (s.erase (s.min' hs)).eq_empty_or_nonempty with h h
[GOAL]
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)
[PROOFSTEP]
rw [h, Finset.prod_empty, mul_one]
[GOAL]
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)
[PROOFSTEP]
exact FP.head _
[GOAL]
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)
[PROOFSTEP]
apply FP.cons
[GOAL]
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)
[PROOFSTEP]
rw [Stream'.tail_eq_drop, Stream'.drop_drop, add_comm]
[GOAL]
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)
[PROOFSTEP]
refine' Set.mem_of_subset_of_mem _ (ih _ (Finset.erase_ssubset <| s.min'_mem hs) h)
[GOAL]
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)
[PROOFSTEP]
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 _ _)
[GOAL]
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)
[PROOFSTEP]
cases' le_iff_exists_add.mp this with d hd
[GOAL]
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)
[PROOFSTEP]
rw [hd, add_comm, ← Stream'.drop_drop]
[GOAL]
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)
[PROOFSTEP]
apply FP_drop_subset_FP
