-- Mathlib/Combinatorics/Hindman.lean
theorem exists_FP_of_large {M} [Semigroup M] (U : Ultrafilter M) (U_idem : U * U = U) (s₀ : Set M)
    (sU : s₀ ∈ U) : ∃ a, FP a ⊆ s₀

Proof state:
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 → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih : ∀ (p_1 : { s // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ (Stream'.corec elem succ p).tail = Stream'.corec elem succ (succ p)

Tactic:
rw [Stream'.corec_eq, Stream'.tail_cons]

Result:
no goals

Proof state:
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 → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m : M
b : Stream' M
n : M
h : FP b.tail n
ih : ∀ (p : { s // s ∈ U }), b.tail = Stream'.corec elem succ p → n ∈ ↑p
⊢ ∀ (p : { s // s ∈ U }), b = Stream'.corec elem succ p → n ∈ ↑p

Tactic:
rintro p rfl

Result:
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 → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih : ∀ (p_1 : { s // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ n ∈ ↑p

Proof state:
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

Tactic:
rwa [← U_idem] at hs

Result:
no goals

Proof state:
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 → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih : ∀ (p_1 : { s // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ n ∈ ↑p

Tactic:
refine Set.inter_subset_left (ih (succ p) ?_)

Result:
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 → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih : ∀ (p_1 : { s // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ (Stream'.corec elem succ p).tail = Stream'.corec elem succ (succ p)

Proof state:
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 → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
⊢ FP (Stream'.corec elem succ ⟨s₀, sU⟩) ⊆ s₀

Tactic:
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

Result:
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 → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
⊢ ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p

Proof state:
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 → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m : M
p : { s // s ∈ U }
⊢ (Stream'.corec elem succ p).head ∈ ↑p

Tactic:
rw [Stream'.corec_eq, Stream'.head_cons]

Result:
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 → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m : M
p : { s // s ∈ U }
⊢ elem p ∈ ↑p

Proof state:
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 → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih : ∀ (p_1 : { s // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ (Stream'.corec elem succ p).head * n ∈ ↑p

Tactic:
have := Set.inter_subset_right (ih (succ p) ?_)

Result:
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 → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih : ∀ (p_1 : { s // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ ↑p_1
this : n ∈ {m | elem p * m ∈ ↑p}
⊢ (Stream'.corec elem succ p).head * n ∈ ↑p

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 → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih : ∀ (p_1 : { s // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ (Stream'.corec elem succ p).tail = Stream'.corec elem succ (succ p)

Proof state:
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 → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih : ∀ (p_1 : { s // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ (Stream'.corec elem succ p).tail = Stream'.corec elem succ (succ p)

Tactic:
rw [Stream'.corec_eq, Stream'.tail_cons]

Result:
no goals