awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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).head * n ∈ (↑p : Set M)
have h₁ : ∀ (this : Membership.mem (γ := Set M) {m : M | elem p * m ∈ (↑p : Set M)} n),
  (Stream'.corec elem succ p).head * n ∈ (↑p : Set M)
Tactic: have := Set.inter_subset_right (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)
h₁ :
  ∀ (this : Membership.mem (γ := Set M) {m : M | elem p * m ∈ (↑p : Set M)} n),
    (Stream'.corec elem succ p).head * n ∈ (↑p : Set M)
⊢ (Stream'.corec elem succ p).head * n ∈ (↑p : Set M)
have h₂ : (Stream'.corec elem succ p).tail = Stream'.corec elem succ (succ p)
Tactic: have := Set.inter_subset_right (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 : M
h : m ∈ FP a
⊢ ∀ (p : { s : Set M // s ∈ U }), a = Stream'.corec elem succ p → m ∈ (↑p : Set M)
have h₁ : ∀ (b : Stream' M) (p : { s : Set M // s ∈ U }), b = Stream'.corec elem succ p → b.head ∈ (↑p : Set M)
Tactic: induction h with
  | head' b =>
    rintro p rfl
    rw [Stream'.corec_eq, Stream'.head_cons]
    exact Set.inter_subset_left (Set.Nonempty.some_mem _)
  | tail' b n h ih =>
    rintro p rfl
    refine Set.inter_subset_left (ih (succ p) ?_)
    rw [Stream'.corec_eq, Stream'.tail_cons]
  | cons' b n h ih =>
    rintro p rfl
    have := Set.inter_subset_right (ih (succ p) ?_)
    · simpa only using this
    rw [Stream'.corec_eq, Stream'.tail_cons]
Cleared hypotheses: h
-- 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
h : m ∈ FP a
h₁ : ∀ (b : Stream' M) (p : { s : Set M // s ∈ U }), b = Stream'.corec elem succ p → b.head ∈ (↑p : Set M)
⊢ ∀ (p : { s : Set M // s ∈ U }), a = Stream'.corec elem succ p → m ∈ (↑p : Set M)
have h₂ : ∀ (b : Stream' M) (n : M) (h : FP b.tail n)
  (ih : ∀ (p : { s : Set M // s ∈ U }), b.tail = Stream'.corec elem succ p → n ∈ (↑p : Set M))
  (p : { s : Set M // s ∈ U }), b = Stream'.corec elem succ p → n ∈ (↑p : Set M)
Tactic: induction h with
  | head' b =>
    rintro p rfl
    rw [Stream'.corec_eq, Stream'.head_cons]
    exact Set.inter_subset_left (Set.Nonempty.some_mem _)
  | tail' b n h ih =>
    rintro p rfl
    refine Set.inter_subset_left (ih (succ p) ?_)
    rw [Stream'.corec_eq, Stream'.tail_cons]
  | cons' b n h ih =>
    rintro p rfl
    have := Set.inter_subset_right (ih (succ p) ?_)
    · simpa only using this
    rw [Stream'.corec_eq, Stream'.tail_cons]
Cleared hypotheses: h
-- 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
h : m ∈ FP a
h₁ : ∀ (b : Stream' M) (p : { s : Set M // s ∈ U }), b = Stream'.corec elem succ p → b.head ∈ (↑p : Set M)
h₂ :
  ∀ (b : Stream' M) (n : M) (h : FP b.tail n)
    (ih : ∀ (p : { s : Set M // s ∈ U }), b.tail = Stream'.corec elem succ p → n ∈ (↑p : Set M))
    (p : { s : Set M // s ∈ U }), b = Stream'.corec elem succ p → n ∈ (↑p : Set M)
⊢ ∀ (p : { s : Set M // s ∈ U }), a = Stream'.corec elem succ p → m ∈ (↑p : Set M)
have h₃ : ∀ (b : Stream' M) (n : M) (h : FP b.tail n)
  (ih : ∀ (p : { s : Set M // s ∈ U }), b.tail = Stream'.corec elem succ p → n ∈ (↑p : Set M))
  (p : { s : Set M // s ∈ U }), b = Stream'.corec elem succ p → b.head * n ∈ (↑p : Set M)
Tactic: induction h with
  | head' b =>
    rintro p rfl
    rw [Stream'.corec_eq, Stream'.head_cons]
    exact Set.inter_subset_left (Set.Nonempty.some_mem _)
  | tail' b n h ih =>
    rintro p rfl
    refine Set.inter_subset_left (ih (succ p) ?_)
    rw [Stream'.corec_eq, Stream'.tail_cons]
  | cons' b n h ih =>
    rintro p rfl
    have := Set.inter_subset_right (ih (succ p) ?_)
    · simpa only using this
    rw [Stream'.corec_eq, Stream'.tail_cons]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop (n + 1) a) ⊆ FP a
have succ : FP (Stream'.drop 1 (Stream'.drop n a)) ⊆ FP a
Tactic: rw [← Stream'.drop_drop]
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
n : ℕ
⊢ FP (Stream'.drop n a) ⊆ FP a
have zero : FP (Stream'.drop 0 a) ⊆ FP (Stream'.drop 0 a)
Tactic: induction n with
  | zero => rfl
  | succ n ih =>
    rw [← Stream'.drop_drop]
    exact _root_.trans (FP.tail _) ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
n : ℕ
zero : FP (Stream'.drop 0 a) ⊆ FP (Stream'.drop 0 a)
⊢ FP (Stream'.drop n a) ⊆ FP a
have succ : ∀ (n : ℕ) (ih : FP (Stream'.drop n a) ⊆ FP a), FP (Stream'.drop (n + 1) a) ⊆ FP a
Tactic: induction n with
  | zero => rfl
  | succ n ih =>
    rw [← Stream'.drop_drop]
    exact _root_.trans (FP.tail _) ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i : ℕ
⊢ a.get i ∈ FP a
have zero : ∀ (a : Stream' M), a.get 0 ∈ FP a
Tactic: induction i generalizing a with
  | zero => exact FP.head _
  | succ i ih => exact FP.tail _ _ (ih _)
Cleared hypotheses: a, i
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i : ℕ
zero : ∀ (a : Stream' M), a.get 0 ∈ FP a
⊢ a.get i ∈ FP a
have succ : ∀ (i : ℕ) (ih : ∀ (a : Stream' M), a.get i ∈ FP a) (a : Stream' M), a.get (i + 1) ∈ FP a
Tactic: induction i generalizing a with
  | zero => exact FP.head _
  | succ i ih => exact FP.tail _ _ (ih _)
Cleared hypotheses: a, i
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ a.get i * a.get j ∈ FP a
have refine : a.get i * a.get j ∈ FP (Stream'.drop i a)
Tactic: refine FP_drop_subset_FP _ i ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ a.get i * a.get j ∈ FP (Stream'.drop i a)
have rw : (Stream'.drop i a).head * a.get j ∈ FP (Stream'.drop i a)
Tactic: rw [← Stream'.head_drop]
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ (Stream'.drop i a).head * a.get j ∈ FP (Stream'.drop i a)
have h : FP (Stream'.drop i a).tail (a.get j)
Tactic: apply FP.cons
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ FP (Stream'.drop i a).tail (a.get j)
have h : ∀ (d : ℕ) (hd : j = i.succ + d), FP (Stream'.drop i a).tail (a.get j)
Tactic: rcases Nat.exists_eq_add_of_le (Nat.succ_le_of_lt ij) with ⟨d, hd⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (hypothesis)
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = i.succ + d
⊢ FP (Stream'.drop i a).tail (a.get j)
have this : (Stream'.drop i a).tail.get d ∈ FP (Stream'.drop i a).tail
Tactic: have := FP.singleton (a.drop i).tail d
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (hypothesis)
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = i.succ + d
this : (Stream'.drop i a).tail.get d ∈ FP (Stream'.drop i a).tail
⊢ FP (Stream'.drop i a).tail (a.get j)
have this₁ : a.get (i + (1 + d)) ∈ FP (Stream'.drop 1 (Stream'.drop i a))
Tactic: rw [Stream'.tail_eq_drop, Stream'.get_drop, Stream'.get_drop] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = i.succ + d
this : a.get (i + (1 + d)) ∈ FP (Stream'.drop 1 (Stream'.drop i a))
⊢ FP (Stream'.drop i a).tail (a.get j)
have h : j = i + (1 + d)
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : Stream' M
s : Finset ℕ
hs : s.Nonempty
⊢ ∏ i ∈ s, a.get i ∈ FP a
have refine : ∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)
Tactic: refine FP_drop_subset_FP _ (s.min' hs) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : Stream' M
s : Finset ℕ
hs : s.Nonempty
⊢ ∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)
have H : ∀ (s : Finset ℕ)
  (ih :
    ∀ s_1 ∈ s,
      ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a))
  (hs : s.Nonempty), ∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)
Tactic: induction s using Finset.eraseInduction with | H s ih => _
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
⊢ ∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)
have H : (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)
Tactic: rw [← Finset.mul_prod_erase _ _ (s.min'_mem hs), ← Stream'.head_drop]
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)
have H : ∀ (h : s.erase (s.min' hs) = ∅),
  (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)
Tactic: rcases (s.erase (s.min' hs)).eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
H :
  ∀ (h : s.erase (s.min' hs) = ∅),
    (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)
have H₁ : ∀ (h : (s.erase (s.min' hs)).Nonempty),
  (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)
Tactic: rcases (s.erase (s.min' hs)).eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : s.erase (s.min' hs) = ∅
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)
have H : (Stream'.drop (s.min' hs) a).head ∈ FP (Stream'.drop (s.min' hs) a)
Tactic: rw [h, Finset.prod_empty, mul_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)
have H : FP (Stream'.drop (s.min' hs) a).tail (∏ x ∈ s.erase (s.min' hs), a.get x)
Tactic: apply FP.cons
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ FP (Stream'.drop (s.min' hs) a).tail (∏ x ∈ s.erase (s.min' hs), a.get x)
have H : FP (Stream'.drop (1 + s.min' hs) a) (∏ x ∈ s.erase (s.min' hs), a.get x)
Tactic: rw [Stream'.tail_eq_drop, Stream'.drop_drop, add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ FP (Stream'.drop (1 + s.min' hs) a) (∏ x ∈ s.erase (s.min' hs), a.get x)
have H : FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)
Tactic: refine Set.mem_of_subset_of_mem ?_ (ih _ (s.min'_mem hs) h)
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
⊢ FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)
have this : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h
Tactic: have : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h :=
      Nat.succ_le_of_lt (Finset.min'_lt_of_mem_erase_min' _ _ <| Finset.min'_mem _ _)
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
this : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h
⊢ FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)
have H : ∀ (d : ℕ) (hd : (s.erase (s.min' hs)).min' h = s.min' hs + 1 + d),
  FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)
Tactic: obtain ⟨d, hd⟩ := Nat.exists_eq_add_of_le this
-- Lean 4 proof step from Mathlib.Combinatorics.Hindman (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
this : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h
d : ℕ
hd : (s.erase (s.min' hs)).min' h = s.min' hs + 1 + d
⊢ FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)
have H : FP (Stream'.drop d (Stream'.drop (1 + s.min' hs) a)) ⊆ FP (Stream'.drop (1 + s.min' hs) a)
Tactic: rw [hd, ← Stream'.drop_drop, add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (goal)
Goal:
X : Type u_1
inst : Fintype X
f_1 : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
f : ↥(prefixed s)
n : Fin (Fintype.card.{u_1} ↥s)
⊢ Membership.mem (α := X) s ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X) ⟨(↑n : ℕ), ⋯⟩ : X)
have rw : (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X))
        ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X) (⟨(↑n : ℕ), sorry⟩ : Fin (Fintype.card X)))) :
    ℕ) <
  #s
Tactic: rw [mem_prefixed.1 f.2]
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (hypothesis)
Goal:
X : Type u_1
inst : Fintype X
f_1 : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : ↥sᶜ
⊢ (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ) - #s < Fintype.card.{u_1} ↥sᶜ
have this : ¬(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ) < #s
Tactic: have := (mem_prefixed.1 f.2 x).not.1 (Finset.mem_compl.1 x.2)
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (goal)
Goal:
X : Type u_1
inst : Fintype X
f_1 : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : ↥sᶜ
this : ¬(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ) < #s
⊢ (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ) - #s < Fintype.card.{u_1} ↥sᶜ
have simp : ∀ (this : #s ≤ (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ)),
  (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ) - #s < Fintype.card X - #s
Tactic: simp at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (goal)
Goal:
X : Type u_1
inst : Fintype X
f_1 : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
f : ↥(prefixed s)
n : Fin (Fintype.card.{u_1} ↥sᶜ)
⊢ Membership.mem (α := X) sᶜ
    ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X) (⟨(↑n : ℕ) + #s, ⋯⟩ : Fin (Fintype.card X)) : X)
have rw : ¬(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X))
          ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X)
            (⟨(↑n : ℕ) + #s, sorry⟩ : Fin (Fintype.card X)))) :
      ℕ) <
    #s
Tactic: rw [s.mem_compl, mem_prefixed.1 f.2]
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (hypothesis)
Goal:
X : Type u_1
inst : Fintype X
f_1 : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : X
hx : x ∈ sᶜ
⊢ (fun (n : Fin (Fintype.card.{u_1} ↥sᶜ)) ↦
        (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ)
            ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X)
              (⟨(↑n : ℕ) + #s, ⋯⟩ : Fin (Fintype.card X)))
            ⋯ :
          ↥sᶜ))
      ((fun (x : ↥sᶜ) ↦
          (⟨(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ) - #s, ⋯⟩ :
            Fin (Fintype.card.{u_1} ↥sᶜ)))
        (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x hx)) =
    Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x hx
have hx₁ : #s ≤ (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) x) : ℕ)
Tactic: rw [s.mem_compl, mem_prefixed.1 f.2, not_lt] at hx
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (goal)
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
x : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
hn : ¬(↑n : ℕ) < #s
⊢ (↑n : ℕ) - #s < Fintype.card.{u_1} ↥sᶜ
have simp : (↑n : ℕ) - #s < Fintype.card X - #s
Tactic: simp
-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (goal)
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
x_1 : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
⊢ (fun (n : Fin (Fintype.card X)) ↦
        (if hn : (↑n : ℕ) < #s then
            (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s) (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card.{u_1} ↥s))) : X)
          else (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ) ⟨(↑n : ℕ) - #s, ⋯⟩) : X) :
          X))
      ((fun (x : X) ↦
          (if hx : x ∈ s then
              Fin.castLE (n := Fintype.card.{u_1} ↥s) ⋯
                ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
            else
              Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) ⋯
                (Fin.addNat ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x ⋯))
                  #s) :
            Fin (Fintype.card X)))
        x) =
    x
have pos : ∀ (hx : x ∈ s),
  (fun (n : Fin (Fintype.card X)) ↦
        (if hn : (↑n : ℕ) < #s then
            (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s) (⟨(↑n : ℕ), sorry⟩ : Fin (Fintype.card.{u_1} ↥s))) : X)
          else (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ) ⟨(↑n : ℕ) - #s, sorry⟩) : X) :
          X))
      ((fun (x : X) ↦
          (if hx : x ∈ s then
              Fin.castLE (n := Fintype.card.{u_1} ↥s) sorry
                ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
            else
              Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) sorry
                (Fin.addNat ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x sorry))
                  #s) :
            Fin (Fintype.card X)))
        x) =
    x
Tactic: by_cases hx : x ∈ s