awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
hn : Fintype.card ι = n
intro :
  ∀
    (ih :
      ∀ m < 0,
        ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
          (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x)
    (hn : Fintype.card ι = 0), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
intro₁ :
  ∀ (n : ℕ)
    (ih :
      ∀ m < n + 1,
        ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
          (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x)
    (hn : Fintype.card ι = n + 1), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
rcases n with (_ | n)
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
ih :
  ∀ m < 0,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = 0
⊢ IsEmpty ι

Tactic:
rw [Fintype.card_eq_zero_iff] at hn

Premises used: Fintype.card_eq_zero_iff
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
ih :
  ∀ m < 0,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : IsEmpty ι
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
⟨isEmptyElim, isEmptyElim, isEmptyElim⟩

Premises used: isEmptyElim, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
ih :
  ∀ m < 0,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : IsEmpty ι
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
exact ⟨isEmptyElim, isEmptyElim, isEmptyElim⟩
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ι' : Type u
_ :
  ∀ [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
⊢ ∀ [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x

Tactic:
_
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ι' : Type u
inst_2 : Fintype ι'
_ :
  ∀ (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
⊢ ∀ (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x

Tactic:
_
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ι' : Type u
inst_2 : Fintype ι'
t' : ι' → Finset α
hι' : Fintype.card ι' ≤ n
ht' : ∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')
⊢ ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x

Tactic:
ih _ (Nat.lt_succ_of_le hι') ht' _ rfl

Premises used: Nat.lt_succ_of_le, rfl
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ι' : Type u
inst_2 : Fintype ι'
t' : ι' → Finset α
hι' : Fintype.card ι' ≤ n
ht' : ∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')
⊢ ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x

Tactic:
exact ih _ (Nat.lt_succ_of_le hι') ht' _ rfl

Premises used: Nat.lt_succ_of_le, rfl
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
⊢ ∀ (ι' : Type u) [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x

Tactic:
have ih' : ∀ (ι' : Type u) [Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n →
        (∀ s' : Finset ι', #s' ≤ #(s'.biUnion t')) →
        ∃ f : ι' → α, Function.Injective f ∧ ∀ x, f x ∈ t' x := by
      intro ι' _ _ hι' ht'
      exact ih _ (Nat.lt_succ_of_le hι') ht' _ rfl
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ih' :
  ∀ (ι' : Type u) [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
pos :
  ∀ (h : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)),
    ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
neg :
  ∀ (h : ∃ (s : Finset ι), s.Nonempty ∧ s ≠ univ ∧ #(s.biUnion t) ≤ #s),
    ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
by_cases! h : ∀ s : Finset ι, s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ih' :
  ∀ (ι' : Type u) [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
h : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
hall_hard_inductive_step_A hn ht (@fun ι' => ih' ι') h

Premises used: HallMarriageTheorem.hall_hard_inductive_step_A
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ih' :
  ∀ (ι' : Type u) [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
h : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
refine hall_hard_inductive_step_A hn ht (@fun ι' => ih' ι') h

Premises used: HallMarriageTheorem.hall_hard_inductive_step_A
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ih' :
  ∀ (ι' : Type u) [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
h : ∃ (s : Finset ι), s.Nonempty ∧ s ≠ univ ∧ #(s.biUnion t) ≤ #s
neg :
  ∀ (s : Finset ι) (sne : s.Nonempty) (snu : s ≠ univ) (sle : #(s.biUnion t) ≤ #s),
    ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
rcases h with ⟨s, sne, snu, sle⟩
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ih' :
  ∀ (ι' : Type u) [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
sne : s.Nonempty
snu : s ≠ univ
sle : #(s.biUnion t) ≤ #s
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
hall_hard_inductive_step_B hn ht (@fun ι' => ih' ι')
        s sne snu (Nat.le_antisymm (ht _) sle)

Premises used: HallMarriageTheorem.hall_hard_inductive_step_B, Nat.le_antisymm
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
      (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ih' :
  ∀ (ι' : Type u) [inst_2 : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ (f : ι' → α), Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
sne : s.Nonempty
snu : s ≠ univ
sle : #(s.biUnion t) ≤ #s
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
exact hall_hard_inductive_step_B hn ht (@fun ι' => ih' ι')
        s sne snu (Nat.le_antisymm (ht _) sle)

Premises used: HallMarriageTheorem.hall_hard_inductive_step_B, Nat.le_antisymm
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : Finite ι
inst_1 : DecidableEq α
t : ι → Finset α
mp : (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) → ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
mpr : (∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x) → ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
⊢ (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) ↔ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : Finite ι
inst_1 : DecidableEq α
t : ι → Finset α
⊢ (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) → ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
HallMarriageTheorem.hall_hard_inductive

Premises used: HallMarriageTheorem.hall_hard_inductive
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : Finite ι
inst_1 : DecidableEq α
t : ι → Finset α
⊢ (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) → ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
exact HallMarriageTheorem.hall_hard_inductive

Premises used: HallMarriageTheorem.hall_hard_inductive
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : Finite ι
inst_1 : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
mpr : #(image f s) ≤ #(s.biUnion t)
⊢ #s ≤ #(s.biUnion t)

Tactic:
rw [← card_image_of_injective s hf₁]

Premises used: Finset.card_image_of_injective
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : Finite ι
inst_1 : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
mpr : image f s ⊆ s.biUnion t
⊢ #(image f s) ≤ #(s.biUnion t)

Tactic:
apply card_le_card

Premises used: Finset.card_le_card
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : Finite ι
inst_1 : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
a : α
mpr : (∃ a_1 ∈ s, f a_1 = a) → ∃ a_2 ∈ s, a ∈ t a_2
⊢ a ∈ image f s → a ∈ s.biUnion t

Tactic:
rw [mem_image, mem_biUnion]

Premises used: Finset.mem_image, Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : Finite ι
inst_1 : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
x : ι
hx : x ∈ s
⊢ ∃ a ∈ s, f x ∈ t a

Tactic:
⟨x, hx, hf₂ x⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u_1
α : Type u_2
inst : Finite ι
inst_1 : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
x : ι
hx : x ∈ s
⊢ ∃ a ∈ s, f x ∈ t a

Tactic:
exact ⟨x, hx, hf₂ x⟩
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Mul M
U V : Ultrafilter M
p : M → Prop
⊢ (∀ᶠ (m : M) in (↑(U * V) : Filter M), p m) ↔ ∀ᶠ (m : M) in (↑U : Filter M), ∀ᶠ (m' : M) in (↑V : Filter M), p (m * m')

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
U V W : Ultrafilter M
p : M → Prop
⊢ (∀ᶠ (x : M) in (↑(U * V * W) : Filter M), p x) ↔ ∀ᶠ (x : M) in (↑(U * (V * W)) : Filter M), p x

Tactic:
simp [Ultrafilter.eventually_mul, mul_assoc]

Premises used: mul_assoc, Ultrafilter.eventually_mul
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Mul M
V : Ultrafilter M
⊢ Continuous (Y := Ultrafilter M) fun (x : Ultrafilter M) ↦ x * V

Tactic:
ultrafilterBasis_is_basis.continuous_iff.2 <| Set.forall_mem_range.mpr fun s ↦
    ultrafilter_isOpen_basic { m : M | ∀ᶠ m' in V, m * m' ∈ s }

Premises used: Iff.mpr, HMul.hMul, Set.forall_mem_range, Filter.Eventually, setOf, Membership.mem, ultrafilterBasis_is_basis, ultrafilter_isOpen_basic, TopologicalSpace.IsTopologicalBasis.continuous_iff, Ultrafilter.toFilter
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a : Stream' M
m : M
h : FP a.tail m
⊢ a.head ∈ FP a

Tactic:
FP.head' a

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

Tactic:
FP.tail' a m h

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

Tactic:
FP.cons' a m h

Premises used: Set.Mem, Hindman.FP.cons'
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a_1 : Stream' M
m : M
a : Stream' M
⊢ ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), a.head * m' ∈ FP a

Tactic:
⟨1, fun m hm => FP.cons a m hm⟩

Premises used: Hindman.FP.cons, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a_1 : Stream' M
m : M
a : Stream' M
⊢ ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), a.head * m' ∈ FP a

Tactic:
exact ⟨1, fun m hm => FP.cons a m hm⟩
-- Module: Mathlib.Combinatorics.Hindman
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
tail' :
  ∀ (n : ℕ) (hn : ∀ 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

Tactic:
obtain ⟨n, hn⟩ := ih
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a_1 : Stream' M
m_1 : M
a : Stream' M
m : M
h_1 : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
h : ∀ m' ∈ FP (Stream'.drop (n + 1) a), m * m' ∈ FP a
⊢ ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), m * m' ∈ FP a

Tactic:
use n + 1
-- Module: Mathlib.Combinatorics.Hindman
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)
⊢ m * m' ∈ FP a

Tactic:
FP.tail _ _ (hn _ hm')

Premises used: Hindman.FP.tail
-- Module: Mathlib.Combinatorics.Hindman
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)
⊢ m * m' ∈ FP a

Tactic:
exact FP.tail _ _ (hn _ hm')

Premises used: Hindman.FP.tail
-- Module: Mathlib.Combinatorics.Hindman
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
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
⊢ ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), a.head * m * m' ∈ FP a

Tactic:
obtain ⟨n, hn⟩ := ih
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a_1 : Stream' M
m_1 : M
a : Stream' M
m : M
h_1 : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
h : ∀ m' ∈ FP (Stream'.drop (n + 1) a), a.head * m * m' ∈ FP a
⊢ ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), a.head * m * m' ∈ FP a

Tactic:
use n + 1
-- Module: Mathlib.Combinatorics.Hindman
Goal:
M : Type u_1
inst : Semigroup M
a_1 : Stream' M
m_1 : M
a : Stream' M
m : M
h_1 : 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)
h : a.head * (m * m') ∈ FP a
⊢ a.head * m * m' ∈ FP a

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Combinatorics.Hindman
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

Tactic:
FP.cons _ _ (hn _ hm')

Premises used: Hindman.FP.cons
-- Module: Mathlib.Combinatorics.Hindman
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

Tactic:
exact FP.cons _ _ (hn _ hm')

Premises used: Hindman.FP.cons
-- Module: Mathlib.Combinatorics.Hindman
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
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
⊢ ∃ (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')

Premises used: mul_assoc, Hindman.FP.tail', Hindman.FP.cons', Hindman.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)}
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
refine_4 : ∀ x ∈ S, ∀ y ∈ S, x * y ∈ S
⊢ ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a

Tactic:
have h := exists_idempotent_in_compact_subsemigroup ?_ S ?_ ?_ ?_
-- 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)}
h : ∃ m ∈ S, m * m = m
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
⊢ ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a

Tactic:
rcases h with ⟨U, hU, U_idem⟩
-- 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
⊢ ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a

Tactic:
⟨U, U_idem, ?_⟩

Premises used: And.intro, Exists.intro
-- 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
refine_5 : ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a
⊢ ∃ (U : Ultrafilter M), U * U = U ∧ ∀ᶠ (m : M) in (↑U : Filter M), m ∈ FP a

Tactic:
refine ⟨U, U_idem, ?_⟩