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₀
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₀
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)
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₀
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₀
let elem : { s // s ∈ U } → M := fun p => (exists_elem p.property).some
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₀
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₀
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)⟩
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₀
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₀
use Stream'.corec elem succ (Subtype.mk s₀ sU)
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
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₀
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
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
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
clear sU s₀
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
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
intro a m h
case 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

case 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

case 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
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
induction' h with b b n h ih b n h ih
no goals
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
rwa [← U_idem] at hs
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₀
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₀
intro m hm
no goals
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₀
exact this _ m hm ⟨s₀, sU⟩ rfl
case 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
case 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
rintro p rfl
case 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
case 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
rw [Stream'.corec_eq, Stream'.head_cons]
no goals
case 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
exact Set.inter_subset_left _ _ (Set.Nonempty.some_mem _)
case 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
case 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
rintro p rfl
case 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)
case 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
refine' Set.inter_subset_left _ _ (ih (succ p) _)
no goals
case 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)
rw [Stream'.corec_eq, Stream'.tail_cons]
case 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
case 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
rintro p rfl
case 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

case 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)
case 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
have := Set.inter_subset_right _ _ (ih (succ p) ?_)
no goals
case 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)
rw [Stream'.corec_eq, Stream'.tail_cons]
no goals
case 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
simpa only using this