awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
haveI :
  ∀ (this : DecidableEq ι),
    #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)

Tactic:
haveI := Classical.decEq ι
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this : DecidableEq ι
simp : ∀ ⦃a : ι⦄, a ∈ s → ∀ (x : a ∈ (↑s : Set ι)ᶜ), Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)ᶜ) a ⋯ ∉ s'
⊢ Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')

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

Premises used: Finset.mem_image, not_exists, exists_eq_right, SetCoe.exists, exists_and_right, Finset.disjoint_left
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this : DecidableEq ι
x : ι
hx : x ∈ s
hc : x ∈ (↑s : Set ι)ᶜ
_ : Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)ᶜ) x ⋯ ∈ s' → False
⊢ Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)ᶜ) x ⋯ ∉ s'

Tactic:
_
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this : DecidableEq ι
x : ι
hx : x ∈ s
hc : x ∈ (↑s : Set ι)ᶜ
h : Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)ᶜ) x ⋯ ∈ s'
⊢ False

Tactic:
absurd hx hc

Premises used: absurd
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this : DecidableEq ι
x : ι
hx : x ∈ s
hc : x ∈ (↑s : Set ι)ᶜ
h : Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)ᶜ) x ⋯ ∈ s'
⊢ False

Tactic:
exact absurd hx hc

Premises used: absurd
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this : DecidableEq ι
⊢ Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')

Tactic:
have disj : Disjoint s (s'.image fun z => z.1) := by
    simp only [disjoint_left, not_exists, mem_image, SetCoe.exists, exists_and_right,
      exists_eq_right]
    intro x hx hc _
    exact absurd hx hc
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
⊢ #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s

Tactic:
simp [disj, card_image_of_injective _ Subtype.coe_injective, Nat.add_sub_cancel_left]

Premises used: Nat.add_sub_cancel_left, Finset.card_image_of_injective, Subtype.coe_injective
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
⊢ #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s

Tactic:
have : #s' = #(s ∪ s'.image fun z => z.1) - #s := by
    simp [disj, card_image_of_injective _ Subtype.coe_injective, Nat.add_sub_cancel_left]
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
rw :
  #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #(s.biUnion t) ≤
    card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
⊢ #s' ≤ card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)

Tactic:
rw [this, hus]
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
⊢ #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #(s.biUnion t) ≤
    card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)

Tactic:
(Nat.sub_le_sub_right (ht _) _).trans ?_

Premises used: Nat.sub_le_sub_right, LE.le.trans
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
refine :
  #((s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t) - #(s.biUnion t) ≤
    card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
⊢ #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #(s.biUnion t) ≤
    card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)

Tactic:
refine (Nat.sub_le_sub_right (ht _) _).trans ?_

Premises used: Nat.sub_le_sub_right, LE.le.trans
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
rw :
  #((s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t \ s.biUnion t) ≤
    card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)
rw₁ : s.biUnion t ⊆ (s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t
⊢ #((s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t) - #(s.biUnion t) ≤
    card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)

Tactic:
rw [← card_sdiff_of_subset]

Premises used: Finset.card_sdiff_of_subset
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
a :
  (s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t \ s.biUnion t ⊆
    s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t
⊢ #((s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t \ s.biUnion t) ≤
    card.{v} (α := α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t (↑x' : ι) \ s.biUnion t)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t_1 : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t_1)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t_1)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
t : α
a :
  ∀ (x : ι),
    (x ∈ s ∨ ∃ a ∈ s', (↑a : ι) = x) →
      t ∈ t_1 x → (∀ (x : ι), ¬(x ∈ s ∧ t ∈ t_1 x)) → ∃ a ∈ s', t ∈ t_1 (↑a : ι) ∧ ∀ (x : ι), ¬(x ∈ s ∧ t ∈ t_1 x)
⊢ t ∈ (s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t_1 \ s.biUnion t_1 →
    Membership.mem (γ := Finset α) (s'.biUnion fun (x' : (↑(↑s : Set ι)ᶜ : Type u)) ↦ t_1 (↑x' : ι) \ s.biUnion t_1) t

Tactic:
simp only [mem_biUnion, mem_sdiff, not_exists, mem_image, and_imp, mem_union,
      exists_imp]

Premises used: Finset.mem_image, and_imp, not_exists, Finset.mem_sdiff, Finset.mem_union, exists_imp, Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t_1 : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t_1)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t_1)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
t : α
x : ι
hx : x ∈ s
rat : t ∈ t_1 x
hs : ∀ (x : ι), ¬(x ∈ s ∧ t ∈ t_1 x)
⊢ ∃ a ∈ s', t ∈ t_1 (↑a : ι) ∧ ∀ (x : ι), ¬(x ∈ s ∧ t ∈ t_1 x)

Tactic:
False.elim <| (hs x) <| And.intro hx rat

Premises used: False.elim, And.intro
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t_1 : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t_1)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t_1)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
t : α
x : ι
hx : x ∈ s
rat : t ∈ t_1 x
hs : ∀ (x : ι), ¬(x ∈ s ∧ t ∈ t_1 x)
⊢ ∃ a ∈ s', t ∈ t_1 (↑a : ι) ∧ ∀ (x : ι), ¬(x ∈ s ∧ t ∈ t_1 x)

Tactic:
exact False.elim <| (hs x) <| And.intro hx rat

Premises used: False.elim, And.intro
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t_1 : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t_1)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t_1)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
t : α
x' : (↑(↑s : Set ι)ᶜ : Type u)
hx' : x' ∈ s'
rat : t ∈ t_1 (↑x' : ι)
hs : ∀ (x : ι), ¬(x ∈ s ∧ t ∈ t_1 x)
w : (↑(↑s : Set ι)ᶜ : Type u)
left : x' ∈ s'
left₁ : t ∈ t_1 (↑x' : ι)
right : ∀ (x : ι), ¬(x ∈ s ∧ t ∈ t_1 x)
⊢ ∃ a ∈ s', t ∈ t_1 (↑a : ι) ∧ ∀ (x : ι), ¬(x ∈ s ∧ t ∈ t_1 x)

Tactic:
use x', hx', rat, hs
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
h : s ⊆ s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s'
⊢ s.biUnion t ⊆ (s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s').biUnion t

Tactic:
apply biUnion_subset_biUnion_of_subset_left

Premises used: Finset.biUnion_subset_biUnion_of_subset_left
-- Module: Mathlib.Combinatorics.Hall.Finite
Goal:
α : Type v
inst : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset (↑(↑s : Set ι)ᶜ : Type u)
this_1 : DecidableEq ι
disj : Disjoint s (image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s')
this : #s' = #(s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s') - #s
⊢ s ⊆ s ∪ image (fun (z : (↑(↑s : Set ι)ᶜ : Type u)) ↦ (↑z : ι)) s'

Tactic:
apply subset_union_left

Premises used: Finset.subset_union_left
-- 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
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
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
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
rw :
  ∀ (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 ι),
    ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
⊢ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
rw [Nat.add_one] at hn

Premises used: Nat.add_one
-- Module: Mathlib.Combinatorics.Hall.Finite
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 ι
a : Fintype.card.{u} ↥s < n.succ
⊢ Fintype.card.{u} ↥s ≤ n

Tactic:
apply Nat.le_of_lt_succ

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.Combinatorics.Hall.Finite
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 ι
⊢ Fintype.card.{u} ↥s = #s

Tactic:
Fintype.card_coe _

Premises used: Fintype.card_coe
-- Module: Mathlib.Combinatorics.Hall.Finite
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 ι
⊢ #s < Fintype.card ι

Tactic:
(card_lt_iff_ne_univ _).mpr hns

Premises used: Iff.mpr, Finset.card_lt_iff_ne_univ
-- Module: Mathlib.Combinatorics.Hall.Finite
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 ι
⊢ Fintype.card ι = n.succ

Tactic:
hn
-- Module: Mathlib.Combinatorics.Hall.Finite
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 ι
⊢ Fintype.card.{u} ↥s < n.succ

Tactic:
calc
      Fintype.card s = #s := Fintype.card_coe _
      _ < Fintype.card ι := (card_lt_iff_ne_univ _).mpr hns
      _ = n.succ := hn

Premises used: Iff.mpr, Finset.card_lt_iff_ne_univ, Membership.mem, Fintype.card, Subtype, Nat.succ, Fintype.card_coe
-- Module: Mathlib.Combinatorics.Hall.Finite
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 ι
⊢ Fintype.card.{u} ↥s ≤ n

Tactic:
have card_ι'_le : Fintype.card s ≤ n := by
    apply Nat.le_of_lt_succ
    calc
      Fintype.card s = #s := Fintype.card_coe _
      _ < Fintype.card ι := (card_lt_iff_ne_univ _).mpr hns
      _ = n.succ := hn
-- Module: Mathlib.Combinatorics.Hall.Finite
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' : ι)
rcases :
  ∀ (f' : ↥s → α) (hf' : Function.Injective f') (hsf' : ∀ (x : ↥s), 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_restrict ht) with ⟨f', hf', hsf'⟩

Premises used: HallMarriageTheorem.hall_cond_of_restrict
-- Module: Mathlib.Combinatorics.Hall.Finite
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
simp_rw : Fintype.card.{u} ↥sᶜ < Fintype.card ι
⊢ Fintype.card.{u} (↑ι'' : Type u) ≤ n

Tactic:
simp_rw [ι'', ← Nat.lt_succ_iff, ← hn, ← Finset.coe_compl, coe_sort_coe]

Premises used: Finset.coe_sort_coe, Finset.coe_compl, Nat.lt_succ_iff
-- Module: Mathlib.Combinatorics.Hall.Finite
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
rwa : #sᶜ < Fintype.card ι
rwa₁ rwa₂ rwa₃ rwa₄ : s.Nonempty
⊢ Fintype.card.{u} ↥sᶜ < Fintype.card ι

Tactic:
rwa [Fintype.card_coe, card_compl_lt_iff_nonempty]

Premises used: Finset.card_compl_lt_iff_nonempty, Fintype.card_coe
-- Module: Mathlib.Combinatorics.Hall.Finite
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
⊢ Fintype.card.{u} (↑ι'' : Type u) ≤ n

Tactic:
have card_ι''_le : Fintype.card ι'' ≤ n := by
    simp_rw [ι'', ← Nat.lt_succ_iff, ← hn, ← Finset.coe_compl, coe_sort_coe]
    rwa [Fintype.card_coe, card_compl_lt_iff_nonempty]
-- Module: Mathlib.Combinatorics.Hall.Finite
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
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
⊢ ∃ (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''⟩

Premises used: HallMarriageTheorem.hall_cond_of_compl