awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Hall.Finite
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)
neg :
  ∀ (he : s' = ∅), #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)

Tactic:
by_cases! he : s'.Nonempty

Premises used: Finset.Nonempty
-- Module: Mathlib.Combinatorics.Hall.Finite
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
h : Eq (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (↑z : ι)) s') univ
⊢ False

Tactic:
simpa [← h] using mem_univ x

Premises used: Finset.mem_univ
-- Module: Mathlib.Combinatorics.Hall.Finite
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
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
⊢ #s' < card.{v} (α := α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι))

Tactic:
convert! ha he fun h => by simpa [← h] using mem_univ x using 2
-- Module: Mathlib.Combinatorics.Hall.Finite
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
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
⊢ (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:
ext x
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x_1 : ι
a : α
s' : Finset (↑{x' : ι | x' ≠ x_1} : Type u)
this : DecidableEq ι
ha :
  s'.Nonempty →
    Ne (α := Finset ι) (image (fun (z : (↑{x' : ι | x' ≠ x_1} : Type u)) ↦ (↑z : ι)) s') univ →
      #s' < #(Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x_1} : Type u)) ↦ (↑z : ι)) s') t)
he : s'.Nonempty
x : α
⊢ Membership.mem (γ := Finset α) (s'.biUnion fun (x : (↑{x' : ι | x' ≠ x_1} : Type u)) ↦ t (↑x : ι)) x ↔
    x ∈ Finset.biUnion (image (fun (z : (↑{x' : ι | x' ≠ x_1} : Type u)) ↦ (↑z : ι)) s') t

Tactic:
simp only [mem_image, mem_biUnion, SetCoe.exists, exists_and_right,
        exists_eq_right]

Premises used: Finset.mem_image, exists_eq_right, SetCoe.exists, exists_and_right, Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.Hall.Finite
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 : ι))

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]
-- Module: Mathlib.Combinatorics.Hall.Finite
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 : #s' ≤ #(erase (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x' : ι)) a)
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)

Tactic:
rw [← erase_biUnion]

Premises used: Finset.erase_biUnion
-- Module: Mathlib.Combinatorics.Hall.Finite
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)
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)
⊢ #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

Premises used: Finset.biUnion, Subtype.val
-- Module: Mathlib.Combinatorics.Hall.Finite
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
pos : #s' ≤ card.{v} (α := α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι)) - 1
⊢ #s' ≤ #(erase (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x' : ι)) a)

Tactic:
rw [card_erase_of_mem hb]

Premises used: Finset.card_erase_of_mem
-- Module: Mathlib.Combinatorics.Hall.Finite
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' ≤ card.{v} (α := α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι)) - 1

Tactic:
Nat.le_sub_one_of_lt ha'

Premises used: Nat.le_sub_one_of_lt
-- Module: Mathlib.Combinatorics.Hall.Finite
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' ≤ card.{v} (α := α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι)) - 1

Tactic:
exact Nat.le_sub_one_of_lt ha'

Premises used: Nat.le_sub_one_of_lt
-- Module: Mathlib.Combinatorics.Hall.Finite
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 : ι)
neg : #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)

Tactic:
rw [erase_eq_of_notMem hb]

Premises used: Finset.erase_eq_of_notMem
-- Module: Mathlib.Combinatorics.Hall.Finite
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' ≤ card.{v} (α := α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι))

Tactic:
Nat.le_of_lt ha'

Premises used: Nat.le_of_lt
-- Module: Mathlib.Combinatorics.Hall.Finite
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' ≤ card.{v} (α := α) (s'.biUnion fun (x_1 : (↑{x' : ι | x' ≠ x} : Type u)) ↦ t (↑x_1 : ι))

Tactic:
exact Nat.le_of_lt ha'

Premises used: Nat.le_of_lt
-- Module: Mathlib.Combinatorics.Hall.Finite
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' = ∅
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)
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑{x' : ι | x' ≠ x} : Type u)) ↦ (t (↑x' : ι)).erase a)

Tactic:
subst s'
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
ι : Type u
α : Type v
inst : DecidableEq α
t : ι → Finset α
inst_1 : Fintype ι
x : ι
a : α
this : DecidableEq ι
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:
simp
-- Module: Mathlib.Combinatorics.Hall.Finite
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)
⊢ Nonempty ι

Tactic:
haveI : Nonempty ι := Fintype.card_pos_iff.mp (hn.symm ▸ Nat.succ_pos _)
-- Module: Mathlib.Combinatorics.Hall.Finite
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 ι
haveI : ∀ (this : DecidableEq ι), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
haveI := Classical.decEq ι
-- Module: Mathlib.Combinatorics.Hall.Finite
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_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
rw : 0 < #(t x)
⊢ (t x).Nonempty

Tactic:
rw [← Finset.card_pos]

Premises used: Finset.card_pos
-- Module: Mathlib.Combinatorics.Hall.Finite
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_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
⊢ LT.lt (α := ℕ) 0 1

Tactic:
Nat.one_pos

Premises used: Nat.one_pos
-- Module: Mathlib.Combinatorics.Hall.Finite
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_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
⊢ 1 ≤ #(Finset.biUnion {x} t)

Tactic:
ht {x}

Premises used: Finset.card, Multiset.card, Singleton.singleton
-- Module: Mathlib.Combinatorics.Hall.Finite
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_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
rw rw₁ : #(t x) = #(t x)
⊢ #(Finset.biUnion {x} t) = #(t x)

Tactic:
rw [Finset.singleton_biUnion]

Premises used: Finset.singleton_biUnion
-- Module: Mathlib.Combinatorics.Hall.Finite
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_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
_ : #(Finset.biUnion {x} t) = #(t x)
⊢ 0 < #(t x)

Tactic:
calc
      0 < 1 := Nat.one_pos
      _ ≤ #(.biUnion {x} t) := ht {x}
      _ = (t x).card := by rw [Finset.singleton_biUnion]

Premises used: Nat.one_pos, Finset.card, Singleton.singleton
-- Module: Mathlib.Combinatorics.Hall.Finite
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_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
⊢ (t x).Nonempty

Tactic:
have tx_ne : (t x).Nonempty := by
    rw [← Finset.card_pos]
    calc
      0 < 1 := Nat.one_pos
      _ ≤ #(.biUnion {x} t) := ht {x}
      _ = (t x).card := by rw [Finset.singleton_biUnion]
-- Module: Mathlib.Combinatorics.Hall.Finite
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_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
tx_ne : (t x).Nonempty
choose : ∀ (y : α) (hy : y ∈ t x), ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
choose y hy using tx_ne
-- Module: Mathlib.Combinatorics.Hall.Finite
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_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' : ι | x' ≠ x}
t' : (↑ι' : Type u) → Finset α := fun (x' : (↑ι' : Type u)) ↦ (t (↑x' : ι)).erase y
rw : n + 1 - 1 = n
rw₁ : n + 0 = n
rw₂ rw₃ : n = n
⊢ Fintype.card ι - 1 = n

Tactic:
rw [hn, Nat.add_succ_sub_one, add_zero]

Premises used: Nat.add_succ_sub_one, add_zero
-- Module: Mathlib.Combinatorics.Hall.Finite
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_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' : ι | x' ≠ x}
t' : (↑ι' : Type u) → Finset α := fun (x' : (↑ι' : Type u)) ↦ (t (↑x' : ι)).erase y
⊢ Fintype.card.{u} (↑ι' : Type u) = n

Tactic:
have card_ι' : Fintype.card ι' = n :=
    calc
      Fintype.card ι' = Fintype.card ι - 1 := Set.card_ne_eq _
      _ = n := by rw [hn, Nat.add_succ_sub_one, add_zero]
-- Module: Mathlib.Combinatorics.Hall.Finite
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_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' : ι | x' ≠ x}
t' : (↑ι' : Type u) → Finset α := fun (x' : (↑ι' : Type u)) ↦ (t (↑x' : ι)).erase y
card_ι' : Fintype.card.{u} (↑ι' : Type u) = n
rcases :
  ∀ (f' : (↑ι' : Type u) → α) (hfinj : Function.Injective f') (hfr : ∀ (x : (↑ι' : Type u)), f' x ∈ t' x),
    ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
rcases ih t' card_ι'.le (hall_cond_of_erase y ha) with ⟨f', hfinj, hfr⟩

Premises used: Eq.le, HallMarriageTheorem.hall_cond_of_erase
-- Module: Mathlib.Combinatorics.Hall.Finite
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_1 : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' : ι | x' ≠ x}
t' : (↑ι' : Type u) → Finset α := fun (x' : (↑ι' : Type u)) ↦ (t (↑x' : ι)).erase y
card_ι' : Fintype.card.{u} (↑ι' : Type u) = n
f' : (↑ι' : Type u) → α
hfinj : Function.Injective f'
hfr : ∀ (x : (↑ι' : Type u)), f' x ∈ t' x
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
⟨fun z => if h : z = x then y else f' ⟨z, h⟩, ?_, ?_⟩

Premises used: dite, Subtype.mk, And.intro, Exists.intro, Eq