awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : U ∈ S
U_idem : U * U = U
⊢ Membership.mem (γ := Set (Ultrafilter M))
    {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop 0 a)} U

Tactic:
Set.mem_iInter.mp hU 0

Premises used: Set.mem_iInter, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : U ∈ S
U_idem : U * U = U
⊢ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a

Tactic:
convert! Set.mem_iInter.mp hU 0

Premises used: Set.mem_iInter, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
⊢ ∀ (r : Ultrafilter M), Continuous (Y := Ultrafilter M) fun (x : Ultrafilter M) ↦ x * r

Tactic:
Ultrafilter.continuous_mul_left

Premises used: Ultrafilter.continuous_mul_left
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
⊢ ∀ (r : Ultrafilter M), Continuous (Y := Ultrafilter M) fun (x : Ultrafilter M) ↦ x * r

Tactic:
exact Ultrafilter.continuous_mul_left

Premises used: Ultrafilter.continuous_mul_left
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
refine_2 :
  ∀ (i : ℕ),
    Subset.{u_1} (α := Set (Ultrafilter M))
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop (i + 1) a)}
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)}
refine_2₁ :
  ∀ (i : ℕ),
    Set.Nonempty.{u_1} (α := Ultrafilter M)
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)}
refine_2₂ :
  IsCompact.{u_1} (X := Ultrafilter M) {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop 0 a)}
refine_2₃ :
  ∀ (i : ℕ),
    IsClosed.{u_1} (X := Ultrafilter M) {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)}
⊢ S.Nonempty

Tactic:
apply IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed

Premises used: IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
hU :
  Membership.mem (γ := Set (Ultrafilter M))
    {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop (n + 1) a)} U
h : ∀ a_1 ∈ FP (Stream'.drop (n + 1) a), a_1 ∈ FP (Stream'.drop n a)
⊢ Membership.mem (γ := Set (Ultrafilter M))
    {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)} U

Tactic:
filter_upwards [hU]
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
hU :
  Membership.mem (γ := Set (Ultrafilter M))
    {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop (n + 1) a)} U
h : ∀ a_1 ∈ FP (Stream'.drop n a).tail, a_1 ∈ FP (Stream'.drop n a)
⊢ ∀ a_1 ∈ FP (Stream'.drop (n + 1) a), a_1 ∈ FP (Stream'.drop n a)

Tactic:
rw [← Stream'.drop_drop, ← Stream'.tail_eq_drop]

Premises used: Stream'.tail_eq_drop, Stream'.drop_drop
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
hU :
  Membership.mem (γ := Set (Ultrafilter M))
    {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop (n + 1) a)} U
⊢ ∀ a_1 ∈ FP (Stream'.drop n a).tail, a_1 ∈ FP (Stream'.drop n a)

Tactic:
FP.tail _

Premises used: Hindman.FP.tail, Set.Mem
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
n : ℕ
U : Ultrafilter M
hU :
  Membership.mem (γ := Set (Ultrafilter M))
    {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop (n + 1) a)} U
⊢ ∀ a_1 ∈ FP (Stream'.drop n a).tail, a_1 ∈ FP (Stream'.drop n a)

Tactic:
exact FP.tail _

Premises used: Hindman.FP.tail
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
n : ℕ
⊢ Set.Nonempty.{u_1} (α := Ultrafilter M) {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}

Tactic:
⟨pure _, mem_pure.mpr <| FP.head _⟩

Premises used: Pure.pure, Iff.mpr, Hindman.FP.head, Set.Nonempty, Exists.intro, Filter.mem_pure
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
n : ℕ
⊢ Set.Nonempty.{u_1} (α := Ultrafilter M) {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}

Tactic:
exact ⟨pure _, mem_pure.mpr <| FP.head _⟩
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
⊢ IsCompact.{u_1} (X := Ultrafilter M) {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop 0 a)}

Tactic:
(ultrafilter_isClosed_basic _).isCompact

Premises used: Filter.Eventually, setOf, IsClosed.isCompact, ultrafilter_isClosed_basic
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
⊢ IsCompact.{u_1} (X := Ultrafilter M) {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop 0 a)}

Tactic:
exact (ultrafilter_isClosed_basic _).isCompact

Premises used: IsClosed.isCompact, ultrafilter_isClosed_basic
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
n : ℕ
⊢ IsClosed.{u_1} (X := Ultrafilter M) {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}

Tactic:
apply ultrafilter_isClosed_basic

Premises used: ultrafilter_isClosed_basic
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
⊢ IsCompact S

Tactic:
IsClosed.isCompact (isClosed_iInter fun i => ultrafilter_isClosed_basic _)

Premises used: Hindman.FP, Stream'.drop, setOf, Membership.mem, IsClosed.isCompact, ultrafilter_isClosed_basic, isClosed_iInter
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
⊢ IsCompact S

Tactic:
exact IsClosed.isCompact (isClosed_iInter fun i => ultrafilter_isClosed_basic _)

Premises used: IsClosed.isCompact, ultrafilter_isClosed_basic, isClosed_iInter
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : U ∈ S
V : Ultrafilter M
hV : V ∈ S
refine_4 :
  ∀
    (hU :
      ∀ (i : ℕ),
        Membership.mem (γ := Set (Ultrafilter M))
          {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)} U)
    (V : Ultrafilter M)
    (hV :
      ∀ (i : ℕ),
        Membership.mem (γ := Set (Ultrafilter M))
          {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)} V)
    (i : ℕ),
    Membership.mem (γ := Set (Ultrafilter M))
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)} (U * V)
⊢ U * V ∈ S

Tactic:
rw [Set.mem_iInter] at *

Premises used: Set.mem_iInter
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU :
  ∀ (i : ℕ),
    Membership.mem (γ := Set (Ultrafilter M))
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)} U
V : Ultrafilter M
hV :
  ∀ (i : ℕ),
    Membership.mem (γ := Set (Ultrafilter M))
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)} V
n : ℕ
refine_4 : ∀ᶠ (m : M) in (↑U : Filter M), ∀ᶠ (m' : M) in (↑V : Filter M), m * m' ∈ FP (Stream'.drop n a)
⊢ Membership.mem (γ := Set (Ultrafilter M))
    {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)} (U * V)

Tactic:
rw [Set.mem_setOf_eq, Ultrafilter.eventually_mul]

Premises used: Ultrafilter.eventually_mul, Set.mem_setOf_eq
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU :
  ∀ (i : ℕ),
    Membership.mem (γ := Set (Ultrafilter M))
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)} U
V : Ultrafilter M
hV :
  ∀ (i : ℕ),
    Membership.mem (γ := Set (Ultrafilter M))
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)} V
n : ℕ
h : ∀ (m : M) (hm : m ∈ FP (Stream'.drop n a)), ∀ᶠ (m' : M) in (↑V : Filter M), m * m' ∈ FP (Stream'.drop n a)
⊢ ∀ᶠ (m : M) in (↑U : Filter M), ∀ᶠ (m' : M) in (↑V : Filter M), m * m' ∈ FP (Stream'.drop n a)

Tactic:
filter_upwards [hU n] with m hm
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU :
  ∀ (i : ℕ),
    Membership.mem (γ := Set (Ultrafilter M))
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)} U
V : Ultrafilter M
hV :
  ∀ (i : ℕ),
    Membership.mem (γ := Set (Ultrafilter M))
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)} V
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
h :
  ∀ (n' : ℕ) (hn : ∀ m' ∈ FP (Stream'.drop n' (Stream'.drop n a)), m * m' ∈ FP (Stream'.drop n a)),
    ∀ᶠ (m' : M) in (↑V : Filter M), m * m' ∈ FP (Stream'.drop n a)
⊢ ∀ᶠ (m' : M) in (↑V : Filter M), m * m' ∈ FP (Stream'.drop n a)

Tactic:
obtain ⟨n', hn⟩ := FP.mul hm

Premises used: Hindman.FP.mul
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU :
  ∀ (i : ℕ),
    Membership.mem (γ := Set (Ultrafilter M))
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)} U
V : Ultrafilter M
hV :
  ∀ (i : ℕ),
    Membership.mem (γ := Set (Ultrafilter M))
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)} V
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
n' : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n' (Stream'.drop n a)), m * m' ∈ FP (Stream'.drop n a)
h : ∀ (m' : M) (hm' : m' ∈ FP (Stream'.drop (n' + n) a)), m * m' ∈ FP (Stream'.drop n a)
⊢ ∀ᶠ (m' : M) in (↑V : Filter M), m * m' ∈ FP (Stream'.drop n a)

Tactic:
filter_upwards [hV (n' + n)] with m' hm'

Premises used: HAdd.hAdd
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU :
  ∀ (i : ℕ),
    Membership.mem (γ := Set (Ultrafilter M))
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)} U
V : Ultrafilter M
hV :
  ∀ (i : ℕ),
    Membership.mem (γ := Set (Ultrafilter M))
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)} V
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
n' : ℕ
hn : ∀ 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)
h : m' ∈ FP (Stream'.drop n' (Stream'.drop n a))
⊢ m * m' ∈ FP (Stream'.drop n a)

Tactic:
apply hn
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ (n : ℕ), {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU :
  ∀ (i : ℕ),
    Membership.mem (γ := Set (Ultrafilter M))
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)} U
V : Ultrafilter M
hV :
  ∀ (i : ℕ),
    Membership.mem (γ := Set (Ultrafilter M))
      {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)} V
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
n' : ℕ
hn : ∀ 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))

Tactic:
simpa only [Stream'.drop_drop, add_comm] using hm'

Premises used: Stream'.drop_drop, add_comm
-- Module: Mathlib.Combinatorics.Hindman
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
rwa rwa₁ rwa₂ rwa₃ : ∀ (hs : s ∈ U * U), {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ s} ∈ (↑U : Filter M)
⊢ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ s} ∈ (↑U : Filter M)

Tactic:
rwa [← U_idem] at hs
-- Module: Mathlib.Combinatorics.Hindman
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), (s ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ s}).Nonempty

Tactic:
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)
-- Module: Mathlib.Combinatorics.Hindman
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} (_hs : s ∈ U), (s ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ s}).Nonempty
elem : { s : Set M // s ∈ U } → M :=
  fun (p : { s : Set M // s ∈ U }) ↦
    ⋯.some (s := (↑p : Set M) ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ (↑p : Set M)})
succ : { s : Set M // s ∈ U } → { s : Set M // s ∈ U } :=
  fun (p : { s : Set M // s ∈ U }) ↦
    Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) ((↑p : Set M) ∩ {m : M | elem p * m ∈ (↑p : Set M)}) ⋯
h : FP (Stream'.corec elem succ (Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) s₀ sU)) ⊆ s₀
⊢ ∃ (a : Stream' M), FP a ⊆ s₀

Tactic:
use Stream'.corec elem succ (Subtype.mk s₀ sU)

Premises used: Subtype.mk, Stream'.corec
-- Module: Mathlib.Combinatorics.Hindman
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} (_hs : s ∈ U), (s ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ s}).Nonempty
elem : { s : Set M // s ∈ U } → M :=
  fun (p : { s : Set M // s ∈ U }) ↦
    ⋯.some (s := (↑p : Set M) ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ (↑p : Set M)})
succ : { s : Set M // s ∈ U } → { s : Set M // s ∈ U } :=
  fun (p : { s : Set M // s ∈ U }) ↦
    Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) ((↑p : Set M) ∩ {m : M | elem p * m ∈ (↑p : Set M)}) ⋯
this : ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ (p : { s : Set M // s ∈ U }), a = Stream'.corec elem succ p → m ∈ (↑p : Set M)
m : M
hm : m ∈ FP (Stream'.corec elem succ (Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) s₀ sU))
⊢ m ∈ s₀

Tactic:
this _ m hm ⟨s₀, sU⟩ rfl

Premises used: Set.Mem, Subtype.mk, rfl
-- Module: Mathlib.Combinatorics.Hindman
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} (_hs : s ∈ U), (s ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ s}).Nonempty
elem : { s : Set M // s ∈ U } → M :=
  fun (p : { s : Set M // s ∈ U }) ↦
    ⋯.some (s := (↑p : Set M) ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ (↑p : Set M)})
succ : { s : Set M // s ∈ U } → { s : Set M // s ∈ U } :=
  fun (p : { s : Set M // s ∈ U }) ↦
    Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) ((↑p : Set M) ∩ {m : M | elem p * m ∈ (↑p : Set M)}) ⋯
this : ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ (p : { s : Set M // s ∈ U }), a = Stream'.corec elem succ p → m ∈ (↑p : Set M)
m : M
hm : m ∈ FP (Stream'.corec elem succ (Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) s₀ sU))
⊢ m ∈ s₀

Tactic:
exact this _ m hm ⟨s₀, sU⟩ rfl

Premises used: Subtype.mk, rfl
-- Module: Mathlib.Combinatorics.Hindman
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} (_hs : s ∈ U), (s ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ s}).Nonempty
elem : { s : Set M // s ∈ U } → M :=
  fun (p : { s : Set M // s ∈ U }) ↦
    ⋯.some (s := (↑p : Set M) ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ (↑p : Set M)})
succ : { s : Set M // s ∈ U } → { s : Set M // s ∈ U } :=
  fun (p : { s : Set M // s ∈ U }) ↦
    Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) ((↑p : Set M) ∩ {m : M | elem p * m ∈ (↑p : Set M)}) ⋯
h : ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ (p : { s : Set M // s ∈ U }), a = Stream'.corec elem succ p → m ∈ (↑p : Set M)
⊢ FP (Stream'.corec elem succ (Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) 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
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M} (_hs : s ∈ U), (s ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ s}).Nonempty
elem : { s : Set M // s ∈ U } → M :=
  fun (p : { s : Set M // s ∈ U }) ↦
    ⋯.some (s := (↑p : Set M) ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ (↑p : Set M)})
succ : { s : Set M // s ∈ U } → { s : Set M // s ∈ U } :=
  fun (p : { s : Set M // s ∈ U }) ↦
    Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) ((↑p : Set M) ∩ {m : M | elem p * m ∈ (↑p : Set M)}) ⋯
a : Stream' M
m : M
p : { s : Set M // s ∈ U }
h : elem p ∈ (↑p : Set M)
⊢ (Stream'.corec elem succ p).head ∈ (↑p : Set M)

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

Premises used: Stream'.corec_eq, Stream'.head_cons
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M} (_hs : s ∈ U), (s ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ s}).Nonempty
elem : { s : Set M // s ∈ U } → M :=
  fun (p : { s : Set M // s ∈ U }) ↦
    ⋯.some (s := (↑p : Set M) ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ (↑p : Set M)})
succ : { s : Set M // s ∈ U } → { s : Set M // s ∈ U } :=
  fun (p : { s : Set M // s ∈ U }) ↦
    Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) ((↑p : Set M) ∩ {m : M | elem p * m ∈ (↑p : Set M)}) ⋯
a : Stream' M
m : M
p : { s : Set M // s ∈ U }
⊢ elem p ∈ (↑p : Set M)

Tactic:
Set.inter_subset_left (Set.Nonempty.some_mem _)

Premises used: Set.inter_subset_left, Set.Nonempty.some_mem
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M} (_hs : s ∈ U), (s ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ s}).Nonempty
elem : { s : Set M // s ∈ U } → M :=
  fun (p : { s : Set M // s ∈ U }) ↦
    ⋯.some (s := (↑p : Set M) ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ (↑p : Set M)})
succ : { s : Set M // s ∈ U } → { s : Set M // s ∈ U } :=
  fun (p : { s : Set M // s ∈ U }) ↦
    Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) ((↑p : Set M) ∩ {m : M | elem p * m ∈ (↑p : Set M)}) ⋯
a : Stream' M
m : M
p : { s : Set M // s ∈ U }
⊢ elem p ∈ (↑p : Set M)

Tactic:
exact Set.inter_subset_left (Set.Nonempty.some_mem _)

Premises used: Set.inter_subset_left, Set.Nonempty.some_mem
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M} (_hs : s ∈ U), (s ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ s}).Nonempty
elem : { s : Set M // s ∈ U } → M :=
  fun (p : { s : Set M // s ∈ U }) ↦
    ⋯.some (s := (↑p : Set M) ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ (↑p : Set M)})
succ : { s : Set M // s ∈ U } → { s : Set M // s ∈ U } :=
  fun (p : { s : Set M // s ∈ U }) ↦
    Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) ((↑p : Set M) ∩ {m : M | elem p * m ∈ (↑p : Set M)}) ⋯
a : Stream' M
m n : M
p : { s : Set M // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih :
  ∀ (p_1 : { s : Set M // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ (↑p_1 : Set M)
⊢ n ∈ (↑p : Set M)

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

Premises used: Set.inter_subset_left
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M} (_hs : s ∈ U), (s ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ s}).Nonempty
elem : { s : Set M // s ∈ U } → M :=
  fun (p : { s : Set M // s ∈ U }) ↦
    ⋯.some (s := (↑p : Set M) ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ (↑p : Set M)})
succ : { s : Set M // s ∈ U } → { s : Set M // s ∈ U } :=
  fun (p : { s : Set M // s ∈ U }) ↦
    Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) ((↑p : Set M) ∩ {m : M | elem p * m ∈ (↑p : Set M)}) ⋯
a : Stream' M
m n : M
p : { s : Set M // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih :
  ∀ (p_1 : { s : Set M // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ (↑p_1 : Set M)
h₁ : (Stream'.corec elem succ p).tail = Stream'.corec elem succ (succ p)
⊢ n ∈ (↑p : Set M)

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

Premises used: Set.inter_subset_left
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M} (_hs : s ∈ U), (s ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ s}).Nonempty
elem : { s : Set M // s ∈ U } → M :=
  fun (p : { s : Set M // s ∈ U }) ↦
    ⋯.some (s := (↑p : Set M) ∩ {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ (↑p : Set M)})
succ : { s : Set M // s ∈ U } → { s : Set M // s ∈ U } :=
  fun (p : { s : Set M // s ∈ U }) ↦
    Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) ((↑p : Set M) ∩ {m : M | elem p * m ∈ (↑p : Set M)}) ⋯
a : Stream' M
m n : M
p : { s : Set M // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih :
  ∀ (p_1 : { s : Set M // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ (↑p_1 : Set M)
h₁ : (Stream'.cons (elem p) (Stream'.corec elem succ (succ p))).tail = Stream'.corec elem succ (succ p)
h₂ h₃ : Stream'.corec elem succ (succ p) = Stream'.corec elem succ (succ p)
⊢ (Stream'.corec elem succ p).tail = Stream'.corec elem succ (succ p)

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

Premises used: Stream'.corec_eq, Stream'.tail_cons