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
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ FP a
let S : Set (Ultrafilter M) := ⋂ n, { U | ∀ᶠ m in U, m ∈ FP (a.drop n) }
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

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

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

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

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
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
have h := exists_idempotent_in_compact_subsemigroup ?_ S ?_ ?_ ?_
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
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
rcases h with ⟨U, hU, U_idem⟩
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
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
refine' ⟨U, U_idem, _⟩
no goals
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
convert Set.mem_iInter.mp hU 0
no goals
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
exact Ultrafilter.continuous_mul_left
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)}

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)}

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)}

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)}
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
apply IsCompact.nonempty_iInter_of_sequence_nonempty_compact_closed
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)}
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)}
intro n U hU
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)
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)}
apply Eventually.mono hU
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)
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)
rw [add_comm, ← Stream'.drop_drop, ← Stream'.tail_eq_drop]
no goals
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)
exact FP.tail _
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)}
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)}
intro n
no goals
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)}
exact ⟨pure _, mem_pure.mpr <| FP.head _⟩
no goals
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)}
exact (ultrafilter_isClosed_basic _).isCompact
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)}
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)}
intro n
no goals
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)}
apply ultrafilter_isClosed_basic
no goals
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
exact IsClosed.isCompact (isClosed_iInter fun i => ultrafilter_isClosed_basic _)
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
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
intro U hU V hV
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)}
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
rw [Set.mem_iInter] at *
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)}
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)}
intro n
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)
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)}
rw [Set.mem_setOf_eq, Ultrafilter.eventually_mul]
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)
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)
apply Eventually.mono (hU n)
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)
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)
intro m hm
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)
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)
obtain ⟨n', hn⟩ := FP.mul hm
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)
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)
apply Eventually.mono (hV (n' + n))
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)
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)
intro m' hm'
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))
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)
apply hn
no goals
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))
simpa only [Stream'.drop_drop] using hm'