awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ :
  ∀ (this : Membership.mem (γ := Set M) {m : M | elem p * m ∈ (↑p : Set M)} n),
    (Stream'.corec elem succ p).head * n ∈ (↑p : Set M)
h₂ : (Stream'.corec elem succ p).tail = Stream'.corec elem succ (succ p)
⊢ (Stream'.corec elem succ p).head * n ∈ (↑p : Set M)

Tactic:
have := Set.inter_subset_right (ih (succ p) ?_)
-- 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)
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:
simpa only using this
-- 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
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)
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)
⊢ ∀ (p : { s : Set M // s ∈ U }), a = Stream'.corec elem succ p → m ∈ (↑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]

Premises used: Set.inter_subset_left, Stream'.corec_eq, Set.Nonempty.some_mem, Stream'.head_cons, rfl, Stream'.tail_cons
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
s : Set (Set M)
sfin : s.Finite
scov : FP a ⊆ ⋃₀ s
⊢ ∃ c ∈ s, ∃ (b : Stream' M), FP b ⊆ c

Tactic:
let ⟨U, idem, aU⟩ := exists_idempotent_ultrafilter_le_FP a
  let ⟨c, cs, hc⟩ := (Ultrafilter.finite_sUnion_mem_iff sfin).mp (mem_of_superset aU scov)
  ⟨c, cs, exists_FP_of_large U idem c hc⟩

Premises used: Hindman.exists_idempotent_ultrafilter_le_FP, Hindman.FP, Membership.mem, Exists, Hindman.exists_FP_of_large, HasSubset.Subset, _private.0.Hindman.FP_partition_regular.match_1, _private.0.Hindman.FP_partition_regular.match_2, And, And.intro, Exists.intro, Iff.mp, Ultrafilter.finite_sUnion_mem_iff, Filter.mem_of_superset
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
inst_1 : Nonempty M
s : Set (Set M)
sfin : s.Finite
scov : ⊤ ⊆ ⋃₀ s
⊢ ∃ c ∈ s, ∃ (a : Stream' M), FP a ⊆ c

Tactic:
let ⟨U, hU⟩ :=
    exists_idempotent_of_compact_t2_of_continuous_mul_left (@Ultrafilter.continuous_mul_left M _)
  let ⟨c, c_s, hc⟩ := (Ultrafilter.finite_sUnion_mem_iff sfin).mp (mem_of_superset univ_mem scov)
  ⟨c, c_s, exists_FP_of_large U hU c hc⟩

Premises used: exists_idempotent_of_compact_t2_of_continuous_mul_left, Hindman.FP, Membership.mem, Exists, Hindman.exists_FP_of_large, HasSubset.Subset, _private.0.Hindman.exists_FP_of_finite_cover.match_1, _private.0.Hindman.FP_partition_regular.match_1, And, And.intro, Exists.intro, Iff.mp, Filter.univ_mem, Ultrafilter.finite_sUnion_mem_iff, Ultrafilter.continuous_mul_left, Filter.mem_of_superset
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
⊢ FP (Stream'.drop 0 a) ⊆ FP (Stream'.drop 0 a)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
succ : FP (Stream'.drop 1 (Stream'.drop n a)) ⊆ FP a
⊢ FP (Stream'.drop (n + 1) a) ⊆ FP a

Tactic:
rw [← Stream'.drop_drop]

Premises used: Stream'.drop_drop
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop 1 (Stream'.drop n a)) ⊆ FP a

Tactic:
_root_.trans (FP.tail _) ih

Premises used: Hindman.FP.tail, trans
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop 1 (Stream'.drop n a)) ⊆ FP a

Tactic:
exact _root_.trans (FP.tail _) ih

Premises used: trans
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
n : ℕ
zero : FP (Stream'.drop 0 a) ⊆ FP (Stream'.drop 0 a)
succ : ∀ (n : ℕ) (ih : FP (Stream'.drop n a) ⊆ FP a), FP (Stream'.drop (n + 1) a) ⊆ FP a
⊢ FP (Stream'.drop n a) ⊆ FP a

Tactic:
induction n with
  | zero => rfl
  | succ n ih =>
    rw [← Stream'.drop_drop]
    exact _root_.trans (FP.tail _) ih

Premises used: Stream'.drop_drop
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
⊢ a.get 0 ∈ FP a

Tactic:
FP.head _

Premises used: Set.Mem, Hindman.FP.head
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
⊢ a.get 0 ∈ FP a

Tactic:
exact FP.head _

Premises used: Hindman.FP.head
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
i : ℕ
ih : ∀ (a : Stream' M), a.get i ∈ FP a
a : Stream' M
⊢ a.get (i + 1) ∈ FP a

Tactic:
FP.tail _ _ (ih _)

Premises used: Hindman.FP.tail
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
i : ℕ
ih : ∀ (a : Stream' M), a.get i ∈ FP a
a : Stream' M
⊢ a.get (i + 1) ∈ FP a

Tactic:
exact FP.tail _ _ (ih _)

Premises used: Hindman.FP.tail
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i : ℕ
zero : ∀ (a : Stream' M), a.get 0 ∈ FP a
succ : ∀ (i : ℕ) (ih : ∀ (a : Stream' M), a.get i ∈ FP a) (a : Stream' M), a.get (i + 1) ∈ FP a
⊢ a.get i ∈ FP a

Tactic:
induction i generalizing a with
  | zero => exact FP.head _
  | succ i ih => exact FP.tail _ _ (ih _)

Premises used: Hindman.FP.head
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
⊢ a.get i * a.get j ∈ FP a

Tactic:
FP_drop_subset_FP _ i ?_

Premises used: Hindman.FP_drop_subset_FP
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
refine : a.get i * a.get j ∈ FP (Stream'.drop i a)
⊢ a.get i * a.get j ∈ FP a

Tactic:
refine FP_drop_subset_FP _ i ?_

Premises used: Hindman.FP_drop_subset_FP
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
rw : (Stream'.drop i a).head * a.get j ∈ FP (Stream'.drop i a)
⊢ a.get i * a.get j ∈ FP (Stream'.drop i a)

Tactic:
rw [← Stream'.head_drop]

Premises used: Stream'.head_drop
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
h : FP (Stream'.drop i a).tail (a.get j)
⊢ (Stream'.drop i a).head * a.get j ∈ FP (Stream'.drop i a)

Tactic:
apply FP.cons

Premises used: Hindman.FP.cons
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
h : ∀ (d : ℕ) (hd : j = i.succ + d), FP (Stream'.drop i a).tail (a.get j)
⊢ 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⟩

Premises used: Nat.succ_le_of_lt, Nat.exists_eq_add_of_le
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = i.succ + d
⊢ (Stream'.drop i a).tail.get d ∈ FP (Stream'.drop i a).tail

Tactic:
have := FP.singleton (a.drop i).tail d
-- Module: Mathlib.Combinatorics.Hindman
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
⊢ 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

Premises used: Stream'.tail_eq_drop, Stream'.get_drop
-- Module: Mathlib.Combinatorics.Hindman
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))
⊢ a.get (i + (1 + d)) ∈ FP (Stream'.drop 1 (Stream'.drop i a))

Tactic:
this
-- Module: Mathlib.Combinatorics.Hindman
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))
h : j = i + (1 + d)
⊢ FP (Stream'.drop i a).tail (a.get j)

Tactic:
convert! this
-- Module: Mathlib.Combinatorics.Hindman
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))
⊢ j = i + (1 + d)

Tactic:
lia
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : CommMonoid M
a : Stream' M
s : Finset ℕ
hs : s.Nonempty
⊢ ∏ i ∈ s, a.get i ∈ FP a

Tactic:
FP_drop_subset_FP _ (s.min' hs) ?_

Premises used: Finset.min', Hindman.FP_drop_subset_FP
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : CommMonoid M
a : Stream' M
s : Finset ℕ
hs : s.Nonempty
refine : ∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)
⊢ ∏ i ∈ s, a.get i ∈ FP a

Tactic:
refine FP_drop_subset_FP _ (s.min' hs) ?_

Premises used: Finset.min', Hindman.FP_drop_subset_FP
-- Module: Mathlib.Combinatorics.Hindman
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)

Tactic:
_
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : CommMonoid M
a : Stream' M
s : Finset ℕ
hs : s.Nonempty
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)
⊢ ∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
induction s using Finset.eraseInduction with | H s ih => _

Premises used: Finset.eraseInduction
-- Module: Mathlib.Combinatorics.Hindman
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 : (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)
⊢ ∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
rw [← Finset.mul_prod_erase _ _ (s.min'_mem hs), ← Stream'.head_drop]

Premises used: Finset.min'_mem, Finset.mul_prod_erase, Stream'.head_drop
-- Module: Mathlib.Combinatorics.Hindman
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)
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)
⊢ (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

Premises used: Finset.min', Finset.erase, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.Hindman
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) = ∅
H : (Stream'.drop (s.min' hs) a).head ∈ 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)

Tactic:
rw [h, Finset.prod_empty, mul_one]

Premises used: Finset.prod_empty, mul_one
-- Module: Mathlib.Combinatorics.Hindman
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 ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
FP.head _

Premises used: Hindman.FP.head
-- Module: Mathlib.Combinatorics.Hindman
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 ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
exact FP.head _

Premises used: Hindman.FP.head
-- Module: Mathlib.Combinatorics.Hindman
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
H : FP (Stream'.drop (s.min' hs) a).tail (∏ x ∈ s.erase (s.min' hs), a.get x)
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
apply FP.cons

Premises used: Hindman.FP.cons
-- Module: Mathlib.Combinatorics.Hindman
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
H : FP (Stream'.drop (1 + s.min' hs) a) (∏ x ∈ s.erase (s.min' hs), a.get x)
⊢ FP (Stream'.drop (s.min' hs) a).tail (∏ x ∈ s.erase (s.min' hs), a.get x)

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

Premises used: Stream'.tail_eq_drop, Stream'.drop_drop, add_comm
-- Module: Mathlib.Combinatorics.Hindman
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)

Tactic:
Set.mem_of_subset_of_mem ?_ (ih _ (s.min'_mem hs) h)

Premises used: Set.Mem, Finset.min'_mem, Set.mem_of_subset_of_mem
-- Module: Mathlib.Combinatorics.Hindman
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
H : FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)
⊢ FP (Stream'.drop (1 + s.min' hs) a) (∏ x ∈ s.erase (s.min' hs), a.get x)

Tactic:
refine Set.mem_of_subset_of_mem ?_ (ih _ (s.min'_mem hs) h)

Premises used: Finset.min'_mem, Set.mem_of_subset_of_mem
-- Module: Mathlib.Combinatorics.Hindman
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
⊢ 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 _ _)
-- Module: Mathlib.Combinatorics.Hindman
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
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)
⊢ 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

Premises used: Nat.exists_eq_add_of_le
-- Module: Mathlib.Combinatorics.Hindman
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
H : FP (Stream'.drop d (Stream'.drop (1 + s.min' hs) a)) ⊆ FP (Stream'.drop (1 + s.min' hs) a)
⊢ FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)

Tactic:
rw [hd, ← Stream'.drop_drop, add_comm]

Premises used: Stream'.drop_drop, add_comm
-- Module: Mathlib.Combinatorics.Hindman
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 d (Stream'.drop (1 + s.min' hs) a)) ⊆ FP (Stream'.drop (1 + s.min' hs) a)

Tactic:
apply FP_drop_subset_FP

Premises used: Hindman.FP_drop_subset_FP
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
inst_1 : DecidableEq X
⊢ card.{u_1} (Numbering X) = (card X)!

Tactic:
card_equiv (equivFin _)

Premises used: Fintype.card_equiv, Fintype.equivFin
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s t : Finset X
hs : f.IsPrefix s
ht : f.IsPrefix t
hst : #s ≤ #t
⊢ s ⊆ t

Tactic:
fun a ha ↦ (ht a).mpr <| ((hs a).mp ha).trans_le hst

Premises used: Iff.mpr, LT.lt.trans_le, Iff.mp
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s : Finset X
inst_1 : DecidableEq X
⊢ Membership.mem (γ := Finset (Numbering X)) (prefixed s) f ↔ f.IsPrefix s

Tactic:
simp [prefixed]

Premises used: Numbering.prefixed
-- Module: Mathlib.Combinatorics.KatonaCircle
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)) : ℕ) < Fintype.card.{u_1} ↥s

Tactic:
simp [← mem_prefixed.1 f.2 x]

Premises used: Iff.mp, Numbering.mem_prefixed, Subtype.val, Subtype.property
-- Module: Mathlib.Combinatorics.KatonaCircle
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)
⊢ Fintype.card.{u_1} ↥s ≤ Fintype.card X

Tactic:
simpa using s.card_le_univ

Premises used: Finset.card_le_univ
-- Module: Mathlib.Combinatorics.KatonaCircle
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)
rw :
  (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X))
          ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X) (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card X)))) :
      ℕ) <
    #s
⊢ Membership.mem (α := X) s ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X) ⟨(↑n : ℕ), ⋯⟩ : X)

Tactic:
rw [mem_prefixed.1 f.2]

Premises used: Iff.mp, Numbering.mem_prefixed, Subtype.property
-- Module: Mathlib.Combinatorics.KatonaCircle
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)
⊢ (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X))
          ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X) (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card X)))) :
      ℕ) <
    #s

Tactic:
simpa using n.2

Premises used: Fin.isLt
-- Module: Mathlib.Combinatorics.KatonaCircle
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
⊢ (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))
      ((fun (x : ↥s) ↦
          (⟨(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ), ⋯⟩ : Fin (Fintype.card.{u_1} ↥s)))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Combinatorics.KatonaCircle
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)
⊢ (fun (x : ↥s) ↦
        (⟨(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ), ⋯⟩ : Fin (Fintype.card.{u_1} ↥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))
        n) =
    n

Tactic:
simp
-- Module: Mathlib.Combinatorics.KatonaCircle
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

Tactic:
have := (mem_prefixed.1 f.2 x).not.1 (Finset.mem_compl.1 x.2)
-- Module: Mathlib.Combinatorics.KatonaCircle
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
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
⊢ (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ) - #s < Fintype.card.{u_1} ↥sᶜ

Tactic:
simp at this ⊢