awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a_1 : Stream' M
m_1 : M
a : Stream' M
m : M
h : FP a.tail m
ih : ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), a.head * m * m' ∈ FP a
have cons' : ∀ (n : ℕ) (hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail),
  ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), a.head * m * m' ∈ FP a
Tactic: obtain ⟨n, hn⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a_1 : Stream' M
m_1 : M
a : Stream' M
m : M
h : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), a.head * m * m' ∈ FP a
have h : ∀ m' ∈ FP (Stream'.drop (n + 1) a), a.head * m * m' ∈ FP a
Tactic: use n + 1
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a_1 : Stream' M
m_1 : M
a : Stream' M
m : M
h : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
m' : M
hm' : m' ∈ FP (Stream'.drop (n + 1) a)
⊢ a.head * m * m' ∈ FP a
have h : a.head * (m * m') ∈ FP a
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
m : M
hm : m ∈ FP a
⊢ ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), m * m' ∈ FP a
have head' : ∀ (a : Stream' M), ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), a.head * m' ∈ FP a
Tactic: induction hm with
  | head' a => exact ⟨1, fun m hm => FP.cons a m hm⟩
  | tail' a m _ ih =>
    obtain ⟨n, hn⟩ := ih
    use n + 1
    intro m' hm'
    exact FP.tail _ _ (hn _ hm')
  | cons' a m _ ih =>
    obtain ⟨n, hn⟩ := ih
    use n + 1
    intro m' hm'
    rw [mul_assoc]
    exact FP.cons _ _ (hn _ hm')
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
m : M
hm : m ∈ FP a
head' : ∀ (a : Stream' M), ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), a.head * m' ∈ FP a
⊢ ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), m * m' ∈ FP a
have tail' : ∀ (a : Stream' M) (m : M),
  FP a.tail m →
    ∀ (ih : ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail),
      ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), m * m' ∈ FP a
Tactic: induction hm with
  | head' a => exact ⟨1, fun m hm => FP.cons a m hm⟩
  | tail' a m _ ih =>
    obtain ⟨n, hn⟩ := ih
    use n + 1
    intro m' hm'
    exact FP.tail _ _ (hn _ hm')
  | cons' a m _ ih =>
    obtain ⟨n, hn⟩ := ih
    use n + 1
    intro m' hm'
    rw [mul_assoc]
    exact FP.cons _ _ (hn _ hm')
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
m : M
hm : m ∈ FP a
head' : ∀ (a : Stream' M), ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), a.head * m' ∈ FP a
tail' :
  ∀ (a : Stream' M) (m : M),
    FP a.tail m →
      ∀ (ih : ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail),
        ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), m * m' ∈ FP a
⊢ ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), m * m' ∈ FP a
have cons' : ∀ (a : Stream' M) (m : M),
  FP a.tail m →
    ∀ (ih : ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail),
      ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), a.head * m * m' ∈ FP a
Tactic: induction hm with
  | head' a => exact ⟨1, fun m hm => FP.cons a m hm⟩
  | tail' a m _ ih =>
    obtain ⟨n, hn⟩ := ih
    use n + 1
    intro m' hm'
    exact FP.tail _ _ (hn _ hm')
  | cons' a m _ ih =>
    obtain ⟨n, hn⟩ := ih
    use n + 1
    intro m' hm'
    rw [mul_assoc]
    exact FP.cons _ _ (hn _ hm')
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a
have refine_5 : ∀ (h : ∃ m ∈ S, m * m = m), ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a
Tactic: have h := exists_idempotent_in_compact_subsemigroup ?_ S ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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_5 : ∀ (h : ∃ m ∈ S, m * m = m), ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a
⊢ ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a
have refine_1 : ∀ (r : Ultrafilter M), Continuous (Y := Ultrafilter M) fun (x : Ultrafilter M) ↦ x * r
Tactic: have h := exists_idempotent_in_compact_subsemigroup ?_ S ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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_5 : ∀ (h : ∃ m ∈ S, m * m = m), ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a
refine_1 : ∀ (r : Ultrafilter M), Continuous (Y := Ultrafilter M) fun (x : Ultrafilter M) ↦ x * r
⊢ ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a
have refine_2 : S.Nonempty
Tactic: have h := exists_idempotent_in_compact_subsemigroup ?_ S ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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_5 : ∀ (h : ∃ m ∈ S, m * m = m), ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a
refine_1 : ∀ (r : Ultrafilter M), Continuous (Y := Ultrafilter M) fun (x : Ultrafilter M) ↦ x * r
refine_2 : S.Nonempty
⊢ ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a
have refine_3 : IsCompact S
Tactic: have h := exists_idempotent_in_compact_subsemigroup ?_ S ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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_5 : ∀ (h : ∃ m ∈ S, m * m = m), ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a
refine_1 : ∀ (r : Ultrafilter M), Continuous (Y := Ultrafilter M) fun (x : Ultrafilter M) ↦ x * r
refine_2 : S.Nonempty
refine_3 : IsCompact S
⊢ ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a
have refine_4 : ∀ x ∈ S, ∀ y ∈ S, x * y ∈ S
Tactic: have h := exists_idempotent_in_compact_subsemigroup ?_ S ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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)}
h : ∃ m ∈ S, m * m = m
⊢ ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a
have refine_5 : ∀ (U : Ultrafilter M) (hU : U ∈ S) (U_idem : U * U = U),
  ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a
Tactic: rcases h with ⟨U, hU, U_idem⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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
⊢ ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a
have refine_5 : ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a
Tactic: refine ⟨U, U_idem, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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)}
⊢ S.Nonempty
have 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)}
Tactic: apply IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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)}
⊢ S.Nonempty
have refine_2₁ : ∀ (i : ℕ),
  Set.Nonempty.{u_1} (α := Ultrafilter M) {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)}
Tactic: apply IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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)}
⊢ S.Nonempty
have refine_2₂ : IsCompact.{u_1} (X := Ultrafilter M) {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop 0 a)}
Tactic: apply IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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)}
⊢ S.Nonempty
have refine_2₃ : ∀ (i : ℕ),
  IsClosed.{u_1} (X := Ultrafilter M) {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop i a)}
Tactic: apply IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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
⊢ Membership.mem (γ := Set (Ultrafilter M))
    {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)} U
have h : ∀ a_1 ∈ FP (Stream'.drop (n + 1) a), a_1 ∈ FP (Stream'.drop n a)
Tactic: filter_upwards [hU]
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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 + 1) a), a_1 ∈ FP (Stream'.drop n a)
have h : ∀ a_1 ∈ FP (Stream'.drop n a).tail, a_1 ∈ FP (Stream'.drop n a)
Tactic: rw [← Stream'.drop_drop, ← Stream'.tail_eq_drop]
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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
⊢ U * V ∈ S
have 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)
Tactic: rw [Set.mem_iInter] at *
Cleared hypotheses: hU, V, hV
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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 : ℕ
⊢ Membership.mem (γ := Set (Ultrafilter M))
    {U : Ultrafilter M | ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP (Stream'.drop n a)} (U * V)
have refine_4 : ∀ᶠ (m : M) in (↑U : Filter M), ∀ᶠ (m' : M) in (↑V : Filter M), m * m' ∈ FP (Stream'.drop n a)
Tactic: rw [Set.mem_setOf_eq, Ultrafilter.eventually_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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) in (↑U : Filter M), ∀ᶠ (m' : M) in (↑V : Filter M), m * m' ∈ FP (Stream'.drop n a)
have h : ∀ (m : M) (hm : m ∈ FP (Stream'.drop n a)), ∀ᶠ (m' : M) in (↑V : Filter M), m * m' ∈ FP (Stream'.drop n a)
Tactic: filter_upwards [hU n] with m hm
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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)
⊢ ∀ᶠ (m' : M) in (↑V : Filter M), m * m' ∈ FP (Stream'.drop n a)
have 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)
Tactic: obtain ⟨n', hn⟩ := FP.mul hm
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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) in (↑V : Filter M), m * m' ∈ FP (Stream'.drop n a)
have h : ∀ (m' : M) (hm' : m' ∈ FP (Stream'.drop (n' + n) a)), m * m' ∈ FP (Stream'.drop n a)
Tactic: filter_upwards [hV (n' + n)] with m' hm'
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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 * m' ∈ FP (Stream'.drop n a)
have h : m' ∈ FP (Stream'.drop n' (Stream'.drop n a))
Tactic: apply hn
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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' : M) in (↑U : Filter M), m * m' ∈ s} ∈ (↑U : Filter M)
have rwa : ∀ (hs : s ∈ U * U), {m : M | ∀ᶠ (m' : M) in (↑U : Filter M), m * m' ∈ s} ∈ (↑U : Filter M)
Tactic: rwa [← U_idem] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (hypothesis)
Goal:
M : Type u_1
inst : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
⊢ ∃ (a : Stream' M), FP a ⊆ s₀
have exists_elem : ∀ {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)
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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)}) ⋯
⊢ ∃ (a : Stream' M), FP a ⊆ s₀
have h : FP (Stream'.corec elem succ (Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) s₀ sU)) ⊆ s₀
Tactic: use Stream'.corec elem succ (Subtype.mk s₀ sU)
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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)}) ⋯
⊢ FP (Stream'.corec elem succ (Subtype.mk (p := fun (s : Set M) ↦ s ∈ U) s₀ sU)) ⊆ s₀
have h : ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ (p : { s : Set M // s ∈ U }), a = Stream'.corec elem succ p → m ∈ (↑p : Set M)
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
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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 }
⊢ (Stream'.corec elem succ p).head ∈ (↑p : Set M)
have h : elem p ∈ (↑p : Set M)
Tactic: rw [Stream'.corec_eq, Stream'.head_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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)
have h₁ : (Stream'.corec elem succ p).tail = Stream'.corec elem succ (succ p)
Tactic: refine Set.inter_subset_left (ih (succ p) ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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)
⊢ (Stream'.corec elem succ p).tail = Stream'.corec elem succ (succ p)
have h₁ : (Stream'.cons (elem p) (Stream'.corec elem succ (succ p))).tail = Stream'.corec elem succ (succ p)
Tactic: rw [Stream'.corec_eq, Stream'.tail_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
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)
⊢ (Stream'.corec elem succ p).tail = Stream'.corec elem succ (succ p)
have h₂ : Stream'.corec elem succ (succ p) = Stream'.corec elem succ (succ p)
Tactic: rw [Stream'.corec_eq, Stream'.tail_cons]