awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
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 ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card.{u} ↥s ≤ n
t' : ↥s → Finset α := fun (x' : ↥s) ↦ t (↑x' : ι)
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s : Set ι)ᶜ
t'' : (↑ι'' : Type u) → Finset α := fun (a'' : (↑ι'' : Type u)) ↦ t (↑a'' : ι) \ s.biUnion t
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have rcases : ∀ (f'' : (↑ι'' : Type u) → α) (hf'' : Function.Injective f'') (hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x),
  ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Tactic: rcases ih t'' card_ι''_le (hall_cond_of_compl hus ht) with ⟨f'', hf'', hsf''⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (hypothesis)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
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 ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card.{u} ↥s ≤ n
t' : ↥s → Finset α := fun (x' : ↥s) ↦ t (↑x' : ι)
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s : Set ι)ᶜ
t'' : (↑ι'' : Type u) → Finset α := fun (a'' : (↑ι'' : Type u)) ↦ t (↑a'' : ι) \ s.biUnion t
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
x'' : ι
hx'' : x'' ∉ s
⊢ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
have h : f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∈ t'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
Tactic: have h := hsf'' ⟨x'', hx''⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (hypothesis)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
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 ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card.{u} ↥s ≤ n
t' : ↥s → Finset α := fun (x' : ↥s) ↦ t (↑x' : ι)
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s : Set ι)ᶜ
t'' : (↑ι'' : Type u) → Finset α := fun (a'' : (↑ι'' : Type u)) ↦ t (↑a'' : ι) \ s.biUnion t
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
x'' : ι
hx'' : x'' ∉ s
h : f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∈ t'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
⊢ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
have h₁ : f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∈ t (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') : ι) ∧
  f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
Tactic: rw [mem_sdiff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (hypothesis)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
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 ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card.{u} ↥s ≤ n
t' : ↥s → Finset α := fun (x' : ↥s) ↦ t (↑x' : ι)
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s : Set ι)ᶜ
t'' : (↑ι'' : Type u) → Finset α := fun (a'' : (↑ι'' : Type u)) ↦ t (↑a'' : ι) \ s.biUnion t
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
Tactic: have f''_notMem_biUnion : ∀ (x'') (hx'' : x'' ∉ s), f'' ⟨x'', hx''⟩ ∉ s.biUnion t := by
    intro x'' hx''
    have h := hsf'' ⟨x'', hx''⟩
    rw [mem_sdiff] at h
    exact h.2
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (hypothesis)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
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 ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card.{u} ↥s ≤ n
t' : ↥s → Finset α := fun (x' : ↥s) ↦ t (↑x' : ι)
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s : Set ι)ᶜ
t'' : (↑ι'' : Type u) → Finset α := fun (a'' : (↑ι'' : Type u)) ↦ t (↑a'' : ι) \ s.biUnion t
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have im_disj : ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
  f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
Tactic: have im_disj :
      ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s), f' ⟨x', hx'⟩ ≠ f'' ⟨x'', hx''⟩ := by
    grind
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
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 ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card.{u} ↥s ≤ n
t' : ↥s → Finset α := fun (x' : ↥s) ↦ t (↑x' : ι)
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s : Set ι)ᶜ
t'' : (↑ι'' : Type u) → Finset α := fun (a'' : (↑ι'' : Type u)) ↦ t (↑a'' : ι) \ s.biUnion t
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
im_disj :
  ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have refine_1 : Function.Injective.{u + 1, v + 1} (β := α) fun (x : ι) ↦
  if h : x ∈ s then f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h)
  else f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x h)
Tactic: refine ⟨fun x => if h : x ∈ s then f' ⟨x, h⟩ else f'' ⟨x, h⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
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 ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card.{u} ↥s ≤ n
t' : ↥s → Finset α := fun (x' : ↥s) ↦ t (↑x' : ι)
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s : Set ι)ᶜ
t'' : (↑ι'' : Type u) → Finset α := fun (a'' : (↑ι'' : Type u)) ↦ t (↑a'' : ι) \ s.biUnion t
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
im_disj :
  ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
refine_1 :
  Function.Injective.{u + 1, v + 1} (β := α) fun (x : ι) ↦
    if h : x ∈ s then f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h)
    else f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x h)
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have refine_2 : ∀ (x : ι),
  (fun (x : ι) ↦
        (if h : x ∈ s then f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h)
          else f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x h) :
          α))
      x ∈
    t x
Tactic: refine ⟨fun x => if h : x ∈ s then f' ⟨x, h⟩ else f'' ⟨x, h⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
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 ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card.{u} ↥s ≤ n
t' : ↥s → Finset α := fun (x' : ↥s) ↦ t (↑x' : ι)
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s : Set ι)ᶜ
t'' : (↑ι'' : Type u) → Finset α := fun (a'' : (↑ι'' : Type u)) ↦ t (↑a'' : ι) \ s.biUnion t
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
im_disj :
  ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
x : ι
⊢ (if h : x ∈ s then f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h)
    else f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x h)) ∈
    t x
have pos : ∀ (h : x ∈ s), f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h) ∈ t x
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
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 ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card.{u} ↥s ≤ n
t' : ↥s → Finset α := fun (x' : ↥s) ↦ t (↑x' : ι)
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s : Set ι)ᶜ
t'' : (↑ι'' : Type u) → Finset α := fun (a'' : (↑ι'' : Type u)) ↦ t (↑a'' : ι) \ s.biUnion t
card_ι''_le : Fintype.card.{u} (↑ι'' : Type u) ≤ n
f'' : (↑ι'' : Type u) → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : (↑ι'' : Type u)), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'') ∉ s.biUnion t
im_disj :
  ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s),
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x' hx') ≠ f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x'' hx'')
x : ι
pos : ∀ (h : x ∈ s), f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h) ∈ t x
⊢ (if h : x ∈ s then f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h)
    else f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x h)) ∈
    t x
have neg : ∀ (h : x ∉ s), f'' (Subtype.mk (p := fun (x : ι) ↦ x ∈ ι'') x h) ∈ t x
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have intro : ∀ (val : Fintype ι), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have intro : ∀ (m : ℕ) (hn : Fintype.card ι = m), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Tactic: generalize hn : Fintype.card ι = m
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val : Fintype ι
m : ℕ
hn : Fintype.card ι = m
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have intro : ∀ (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 α} [Finite ι] (ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)) (val : Fintype ι)
  (hn : Fintype.card ι = n), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Tactic: induction m using Nat.strongRecOn generalizing ι with | ind n ih => _
Cleared hypotheses: ι, t, inst_1, ht, val, m, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
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
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have 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
Tactic: rcases n with (_ | n)
Cleared hypotheses: n, ih, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
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
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have 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
Tactic: rcases n with (_ | n)
Cleared hypotheses: n, ih, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (hypothesis)
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
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have hn₁ : IsEmpty ι
Tactic: rw [Fintype.card_eq_zero_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (hypothesis)
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
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have 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
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
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
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
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have pos : ∀ (h : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)),
  ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Tactic: by_cases! h : ∀ s : Finset ι, s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
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
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have neg : ∀ (h : ∃ (s : Finset ι), s.Nonempty ∧ s ≠ univ ∧ #(s.biUnion t) ≤ #s),
  ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Tactic: by_cases! h : ∀ s : Finset ι, s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
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
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have neg : ∀ (s : Finset ι) (sne : s.Nonempty) (snu : s ≠ univ) (sle : #(s.biUnion t) ≤ #s),
  ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Tactic: rcases h with ⟨s, sne, snu, sle⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
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
have mp : (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) → ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
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
⊢ (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) ↔ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have mpr : (∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x) → ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
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 ι
⊢ #s ≤ #(s.biUnion t)
have mpr : #(image f s) ≤ #(s.biUnion t)
Tactic: rw [← card_image_of_injective s hf₁]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
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 ι
⊢ #(image f s) ≤ #(s.biUnion t)
have mpr : image f s ⊆ s.biUnion t
Tactic: apply card_le_card
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
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 : α
⊢ a ∈ image f s → a ∈ s.biUnion t
have mpr : (∃ a_1 ∈ s, f a_1 = a) → ∃ a_2 ∈ s, a ∈ t a_2
Tactic: rw [mem_image, mem_biUnion]
-- 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), m * m' ∈ FP a
have 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
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), m * m' ∈ FP a
have h : ∀ m' ∈ FP (Stream'.drop (n + 1) a), m * m' ∈ FP a
Tactic: use n + 1