awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
mp mp₁ mp₂ :
  ∀ (this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')),
    ∃ (f : ι → α), Injective f ∧ ∀ (x : ι), f x ∈ t x
mp₃ :
  ∀ (this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι'))
    (u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j) (hu : u ∈ (hallMatchingsFunctor t).sections),
    ∃ (f : ι → α), Injective f ∧ ∀ (x : ι), f x ∈ t x
mp₄ :
  (this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')) →
    (u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j) → (hu : u ∈ (hallMatchingsFunctor t).sections) → ι → α
mp₅ :
  ∀ (this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι'))
    (u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j) (hu : u ∈ (hallMatchingsFunctor t).sections),
    Injective.{u + 1, v + 1} (β := α) fun (i : ι) ↦
      (↑(u (Opposite.op {i})) : ↥(Opposite.unop (Opposite.op {i})) → α)
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) (Opposite.unop (Opposite.op {i})) x) i ⋯)
⊢ ∃ (f : ι → α), Injective f ∧ ∀ (x : ι), f x ∈ t x
have mp₆ : ∀ (this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι'))
  (u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j) (hu : u ∈ (hallMatchingsFunctor t).sections) (x : ι),
  Membership.mem (α := α) (t x)
    ((↑(u (Opposite.op {x})) : ↥(Opposite.unop (Opposite.op {x})) → α)
        (Subtype.mk (p := fun (x_1 : ι) ↦ Membership.mem (γ := Finset ι) (Opposite.unop (Opposite.op {x})) x_1) x sorry) :
      α)
Tactic: classical
      haveI : ∀ ι' : (Finset ι)ᵒᵖ, Finite ((hallMatchingsFunctor t).obj ι') := by
        intro ι'
        rw [hallMatchingsFunctor]
        infer_instance
      -- Apply the compactness argument
      obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (hallMatchingsFunctor t)
      -- Interpret the resulting section of the inverse limit
      refine ⟨?_, ?_, ?_⟩
      · -- Build the matching function from the section
        exact fun i =>
          (u (Opposite.op ({i} : Finset ι))).val ⟨i, by simp only [mem_singleton]⟩
      · -- Show that it is injective
        intro i i'
        have subi : ({i} : Finset ι) ⊆ {i, i'} := by simp
        have subi' : ({i'} : Finset ι) ⊆ {i, i'} := by simp
        rw [← Finset.le_iff_subset] at subi subi'
        simp only
        rw [← hu (CategoryTheory.homOfLE subi).op, ← hu (CategoryTheory.homOfLE subi').op]
        let uii' := u (Opposite.op ({i, i'} : Finset ι))
        exact fun h => Subtype.mk_eq_mk.mp (uii'.property.1 h)
      · -- Show that it maps each index to the corresponding finite set
        intro i
        apply (u (Opposite.op ({i} : Finset ι))).property.2
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ #s ≤ #(s.biUnion t)
have mpr : #(image f s) ≤ #(s.biUnion t)
Tactic: rw [← Finset.card_image_of_injective s hf₁]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : 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 Finset.card_le_card
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
A : Finset α
⊢ R.image (↑A : Set α) = (↑(A.biUnion fun (a : α) ↦ (R.image {a}).toFinset) : Set β)
have h : ∀ (x : β), x ∈ R.image (↑A : Set α) ↔ x ∈ (↑(A.biUnion fun (a : α) ↦ (R.image {a}).toFinset) : Set β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (hypothesis)
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
A : Finset α
⊢ Fintype (↑(R.image (↑A : Set α)) : Type v)
have h : R.image (↑A : Set α) = (↑(A.biUnion fun (a : α) ↦ (R.image {a}).toFinset) : Set β)
Tactic: have h : R.image A = (A.biUnion fun a => (R.image {a}).toFinset : Set β) := by
    ext
    simp [SetRel.image]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
A : Finset α
h : R.image (↑A : Set α) = (↑(A.biUnion fun (a : α) ↦ (R.image {a}).toFinset) : Set β)
⊢ Fintype (↑(R.image (↑A : Set α)) : Type v)
have rw : Fintype (↑(↑(A.biUnion fun (a : α) ↦ (R.image {a}).toFinset) : Set β) : Type v)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
r' : (a : α) → Finset β := fun (a : α) ↦ (R.image {a}).toFinset
A : Finset α
⊢ card.{v} (↑(R.image (↑A : Set α)) : Type v) = #(A.biUnion r')
have rw : #(R.image (↑A : Set α)).toFinset = #(A.biUnion r')
Tactic: rw [← Set.toFinset_card]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
r' : (a : α) → Finset β := fun (a : α) ↦ (R.image {a}).toFinset
A : Finset α
⊢ #(R.image (↑A : Set α)).toFinset = #(A.biUnion r')
have h : (R.image (↑A : Set α)).toFinset = A.biUnion r'
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
r' : (a : α) → Finset β := fun (a : α) ↦ (R.image {a}).toFinset
A : Finset α
⊢ (R.image (↑A : Set α)).toFinset = A.biUnion r'
have h : ∀ (b : β), b ∈ (R.image (↑A : Set α)).toFinset ↔ b ∈ A.biUnion r'
Tactic: ext b
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (hypothesis)
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
r' : (a : α) → Finset β := fun (a : α) ↦ (R.image {a}).toFinset
⊢ (∀ (A : Finset α), #A ≤ card.{v} (↑(R.image (↑A : Set α)) : Type v)) ↔
    ∃ (f : α → β), Injective f ∧ ∀ (x : α), (x, f x) ∈ R
have h : ∀ (A : Finset α), card.{v} (↑(R.image (↑A : Set α)) : Type v) = #(A.biUnion r')
Tactic: have h : ∀ A : Finset α, Fintype.card (R.image A) = #(A.biUnion r') := by
    intro A
    rw [← Set.toFinset_card]
    apply congr_arg
    ext b
    simp [r', SetRel.image]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (hypothesis)
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
r' : (a : α) → Finset β := fun (a : α) ↦ (R.image {a}).toFinset
h : ∀ (A : Finset α), card.{v} (↑(R.image (↑A : Set α)) : Type v) = #(A.biUnion r')
⊢ (∀ (A : Finset α), #A ≤ card.{v} (↑(R.image (↑A : Set α)) : Type v)) ↔
    ∃ (f : α → β), Injective f ∧ ∀ (x : α), (x, f x) ∈ R
have h' : ∀ (f : α → β) (x : α), (x, f x) ∈ R ↔ f x ∈ r' x
Tactic: have h' : ∀ (f : α → β) (x), x ~[R] f x ↔ f x ∈ r' x := by simp [r', SetRel.image]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq β
R : SetRel α β
inst_1 : (a : α) → Fintype (↑(R.image {a}) : Type v)
r' : (a : α) → Finset β := fun (a : α) ↦ (R.image {a}).toFinset
h : ∀ (A : Finset α), card.{v} (↑(R.image (↑A : Set α)) : Type v) = #(A.biUnion r')
h' : ∀ (f : α → β) (x : α), (x, f x) ∈ R ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), #A ≤ card.{v} (↑(R.image (↑A : Set α)) : Type v)) ↔
    ∃ (f : α → β), Injective f ∧ ∀ (x : α), (x, f x) ∈ R
have simp : (∀ (A : Finset α), #A ≤ #(A.biUnion r')) ↔ ∃ (f : α → β), Injective f ∧ ∀ (x : α), f x ∈ r' x
Tactic: simp only [h, h']
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Fintype β
r : α → β → Prop
inst_1 : DecidableRel r
⊢ (∀ (A : Finset α), #A ≤ Finset.card.{v} (α := β) {b : β | ∃ a ∈ A, r a b}) ↔
    ∃ (f : α → β), Injective f ∧ ∀ (x : α), r x (f x)
have haveI : ∀ (this : DecidableEq β),
  (∀ (A : Finset α), #A ≤ Finset.card.{v} (α := β) {b : β | ∃ a ∈ A, r a b}) ↔
    ∃ (f : α → β), Injective f ∧ ∀ (x : α), r x (f x)
Tactic: haveI := Classical.decEq β
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Fintype β
r : α → β → Prop
inst_1 : DecidableRel r
this : DecidableEq β
r' : (a : α) → Finset β := fun (a : α) ↦ {b : β | r a b}
A : Finset α
⊢ {b : β | ∃ a ∈ A, r a b} = A.biUnion r'
have h : ∀ (b : β), Membership.mem (γ := Finset β) {b : β | ∃ a ∈ A, r a b} b ↔ b ∈ A.biUnion r'
Tactic: ext b
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (hypothesis)
Goal:
α : Type u
β : Type v
inst : Fintype β
r : α → β → Prop
inst_1 : DecidableRel r
this : DecidableEq β
r' : (a : α) → Finset β := fun (a : α) ↦ {b : β | r a b}
⊢ (∀ (A : Finset α), #A ≤ Finset.card.{v} (α := β) {b : β | ∃ a ∈ A, r a b}) ↔
    ∃ (f : α → β), Injective f ∧ ∀ (x : α), r x (f x)
have h : ∀ (A : Finset α), {b : β | ∃ a ∈ A, r a b} = A.biUnion r'
Tactic: have h : ∀ A : Finset α, ({b | ∃ a ∈ A, r a b} : Finset _) = A.biUnion r' := by
    intro A
    ext b
    simp [r']
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (hypothesis)
Goal:
α : Type u
β : Type v
inst : Fintype β
r : α → β → Prop
inst_1 : DecidableRel r
this : DecidableEq β
r' : (a : α) → Finset β := fun (a : α) ↦ {b : β | r a b}
h : ∀ (A : Finset α), {b : β | ∃ a ∈ A, r a b} = A.biUnion r'
⊢ (∀ (A : Finset α), #A ≤ Finset.card.{v} (α := β) {b : β | ∃ a ∈ A, r a b}) ↔
    ∃ (f : α → β), Injective f ∧ ∀ (x : α), r x (f x)
have h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
Tactic: have h' : ∀ (f : α → β) (x), r x (f x) ↔ f x ∈ r' x := by simp [r']
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Fintype β
r : α → β → Prop
inst_1 : DecidableRel r
this : DecidableEq β
r' : (a : α) → Finset β := fun (a : α) ↦ {b : β | r a b}
h : ∀ (A : Finset α), {b : β | ∃ a ∈ A, r a b} = A.biUnion r'
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), #A ≤ Finset.card.{v} (α := β) {b : β | ∃ a ∈ A, r a b}) ↔
    ∃ (f : α → β), Injective f ∧ ∀ (x : α), r x (f x)
have simp_rw : (∀ (A : Finset α), #A ≤ #(A.biUnion r')) ↔ ∃ (f : α → β), Injective f ∧ ∀ (x : α), f x ∈ r' x
Tactic: simp_rw [h, h']
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)
have haveI : ∀ (this : DecidableEq ι),
  #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)
Tactic: haveI := Classical.decEq ι
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (hypothesis)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
this : DecidableEq ι
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)
have ha₁ : Finset.Nonempty (α := ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') →
  Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
    card (α := ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') <
      #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)
Tactic: specialize ha (s'.image fun z => z.1)
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (hypothesis)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
this : DecidableEq ι
ha :
  Finset.Nonempty (α := ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
      card (α := ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') <
        #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)
have ha₁ : s'.Nonempty →
  Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
    #s' < #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)
Tactic: rw [image_nonempty, Finset.card_image_of_injective s' Subtype.coe_injective] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
this : DecidableEq ι
ha :
  s'.Nonempty →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
      #s' < #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)
have pos : ∀ (he : s'.Nonempty),
  #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)
Tactic: by_cases! he : s'.Nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
this : DecidableEq ι
ha :
  s'.Nonempty →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
      #s' < #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)
pos :
  ∀ (he : s'.Nonempty),
    #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)
have neg : ∀ (he : s' = ∅), #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)
Tactic: by_cases! he : s'.Nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
this : DecidableEq ι
ha :
  s'.Nonempty →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
      #s' < #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)
he : s'.Nonempty
⊢ #s' < card.{v} (α := α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι))
have h : (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι)) =
  Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t
Tactic: convert! ha he fun h => by simpa [← h] using mem_univ x using 2
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
this : DecidableEq ι
ha :
  s'.Nonempty →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
      #s' < #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)
he : s'.Nonempty
⊢ (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι)) =
    Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t
have h : ∀ (x_1 : α),
  Membership.mem (γ := Finset α) (s'.biUnion fun (x_2 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_2 : ι)) x_1 ↔
    x_1 ∈ Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t
Tactic: ext x
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (hypothesis)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
this : DecidableEq ι
ha :
  s'.Nonempty →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
      #s' < #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)
he : s'.Nonempty
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)
have ha' : #s' < card.{v} (α := α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι))
Tactic: have ha' : #s' < #(s'.biUnion fun x => t x) := by
      convert! ha he fun h => by simpa [← h] using mem_univ x using 2
      ext x
      simp only [mem_image, mem_biUnion, SetCoe.exists, exists_and_right,
        exists_eq_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
this : DecidableEq ι
ha :
  s'.Nonempty →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
      #s' < #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)
he : s'.Nonempty
ha' : #s' < card.{v} (α := α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι))
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)
have pos : #s' ≤ #(erase (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x' : ι)) a)
Tactic: rw [← erase_biUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
this : DecidableEq ι
ha :
  s'.Nonempty →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
      #s' < #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)
he : s'.Nonempty
ha' : #s' < card.{v} (α := α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι))
⊢ #s' ≤ #(erase (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x' : ι)) a)
have pos : ∀ (hb : Membership.mem (γ := Finset α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι)) a),
  #s' ≤ #(erase (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x' : ι)) a)
Tactic: by_cases hb : a ∈ s'.biUnion fun x => t x
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
this : DecidableEq ι
ha :
  s'.Nonempty →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
      #s' < #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)
he : s'.Nonempty
ha' : #s' < card.{v} (α := α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι))
pos :
  ∀ (hb : Membership.mem (γ := Finset α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι)) a),
    #s' ≤ #(erase (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x' : ι)) a)
⊢ #s' ≤ #(erase (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x' : ι)) a)
have neg : ∀ (hb : a ∉ s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι)),
  #s' ≤ #(erase (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x' : ι)) a)
Tactic: by_cases hb : a ∈ s'.biUnion fun x => t x
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
this : DecidableEq ι
ha :
  s'.Nonempty →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
      #s' < #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)
he : s'.Nonempty
ha' : #s' < card.{v} (α := α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι))
hb : Membership.mem (γ := Finset α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι)) a
⊢ #s' ≤ #(erase (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x' : ι)) a)
have pos : #s' ≤ card.{v} (α := α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι)) - 1
Tactic: rw [card_erase_of_mem hb]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
this : DecidableEq ι
ha :
  s'.Nonempty →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
      #s' < #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)
he : s'.Nonempty
ha' : #s' < card.{v} (α := α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι))
hb : a ∉ s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι)
⊢ #s' ≤ #(erase (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x' : ι)) a)
have neg : #s' ≤ card.{v} (α := α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι))
Tactic: rw [erase_eq_of_notMem hb]
-- Lean 4 proof step from Mathlib.Combinatorics.Hall.Finite (goal)
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
s' : Finset (↑{x' : ι | x' ≠ x} : Type u)
this : DecidableEq ι
ha :
  s'.Nonempty →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ →
      #s' < #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') t)
he : s' = ∅
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)
have neg : ∀
  (ha :
    Finset.Nonempty.{u} (α := (↑{x' : ι | x' ≠ x} : Type u)) ∅ →
      Ne.{u + 1} (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) ∅) univ →
        card.{u} (α := (↑{x' : ι | x' ≠ x} : Type u)) ∅ <
          #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) ∅) t)),
  card.{u} (α := (↑{x' : ι | x' ≠ x} : Type u)) ∅ ≤
    card.{v} (α := α) (Finset.biUnion ∅ fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)
Tactic: subst s'
Cleared hypotheses: s', ha, he
-- 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 + 1
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
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have this : Nonempty ι
Tactic: haveI : Nonempty ι := Fintype.card_pos_iff.mp (hn.symm ▸ Nat.succ_pos _)
-- 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 + 1
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
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this : Nonempty ι
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have haveI : ∀ (this : DecidableEq ι), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Tactic: haveI := Classical.decEq ι