case intro
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
cases nonempty_fintype ι
case intro.h
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
hn : Fintype.card ι = n
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
case intro
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
induction' hn : Fintype.card ι using Nat.strong_induction_on with n ih generalizing ι
case intro.h.zero
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
ih :
  ∀ (m : ℕ),
    m < Nat.zero →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.zero
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

case intro.h.succ
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
n✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n✝ →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.succ n✝
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
case intro.h
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
hn : Fintype.card ι = n
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
rcases n with (_ | _)
case intro.h.zero
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
ih :
  ∀ (m : ℕ),
    m < Nat.zero →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : IsEmpty ι
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
case intro.h.zero
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
ih :
  ∀ (m : ℕ),
    m < Nat.zero →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.zero
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
rw [Fintype.card_eq_zero_iff] at hn
no goals
case intro.h.zero
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
ih :
  ∀ (m : ℕ),
    m < Nat.zero →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : IsEmpty ι
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
exact ⟨isEmptyElim, isEmptyElim, isEmptyElim⟩
case intro.h.succ
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
n✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n✝ →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.succ n✝
ih' :
  ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n✝ →
      (∀ (s' : Finset ι'), card s' ≤ card (Finset.biUnion s' t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
case intro.h.succ
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
n✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n✝ →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.succ n✝
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
have ih' : ∀ (ι' : Type u) [Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ _ →
    (∀ s' : Finset ι', s'.card ≤ (s'.biUnion t').card) →
    ∃ f : ι' → α, Function.Injective f ∧ ∀ x, f x ∈ t' x := by
  intro ι' _ _ hι' ht'
  exact ih _ (Nat.lt_succ_of_le hι') ht' _ rfl
case pos
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
n✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n✝ →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.succ n✝
ih' :
  ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n✝ →
      (∀ (s' : Finset ι'), card s' ≤ card (Finset.biUnion s' t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
h : ∀ (s : Finset ι), Finset.Nonempty s → s ≠ univ → card s < card (Finset.biUnion s t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

case neg
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
n✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n✝ →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.succ n✝
ih' :
  ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n✝ →
      (∀ (s' : Finset ι'), card s' ≤ card (Finset.biUnion s' t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
h : ¬∀ (s : Finset ι), Finset.Nonempty s → s ≠ univ → card s < card (Finset.biUnion s t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
case intro.h.succ
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
n✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n✝ →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.succ n✝
ih' :
  ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n✝ →
      (∀ (s' : Finset ι'), card s' ≤ card (Finset.biUnion s' t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
by_cases h : ∀ s : Finset ι, s.Nonempty → s ≠ univ → s.card < (s.biUnion t).card
ι✝ : Type u
α : Type v
inst✝³ : DecidableEq α
t✝ : ι✝ → Finset α
inst✝² : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝¹ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
n✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n✝ →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.succ n✝
ι' : Type u
inst✝ : Fintype ι'
t'✝ : ι' → Finset α
hι' : Fintype.card ι' ≤ ?m.46478 ι' t'✝
ht' : ∀ (s' : Finset ι'), card s' ≤ card (Finset.biUnion s' t'✝)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t'✝ x
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
n✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n✝ →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.succ n✝
⊢ ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ ?m.46478 ι' t' →
      (∀ (s' : Finset ι'), card s' ≤ card (Finset.biUnion s' t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
intro ι' _ _ hι' ht'
no goals
ι✝ : Type u
α : Type v
inst✝³ : DecidableEq α
t✝ : ι✝ → Finset α
inst✝² : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝¹ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
n✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n✝ →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.succ n✝
ι' : Type u
inst✝ : Fintype ι'
t'✝ : ι' → Finset α
hι' : Fintype.card ι' ≤ ?m.46478 ι' t'✝
ht' : ∀ (s' : Finset ι'), card s' ≤ card (Finset.biUnion s' t'✝)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t'✝ x
exact ih _ (Nat.lt_succ_of_le hι') ht' _ rfl
no goals
case pos
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
n✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n✝ →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.succ n✝
ih' :
  ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n✝ →
      (∀ (s' : Finset ι'), card s' ≤ card (Finset.biUnion s' t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
h : ∀ (s : Finset ι), Finset.Nonempty s → s ≠ univ → card s < card (Finset.biUnion s t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
refine' hall_hard_inductive_step_A hn ht (@fun ι' => ih' ι') h
case neg
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
n✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n✝ →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.succ n✝
ih' :
  ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n✝ →
      (∀ (s' : Finset ι'), card s' ≤ card (Finset.biUnion s' t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
h : ∃ s, Finset.Nonempty s ∧ s ≠ univ ∧ card (Finset.biUnion s t) ≤ card s
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
case neg
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
n✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n✝ →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.succ n✝
ih' :
  ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n✝ →
      (∀ (s' : Finset ι'), card s' ≤ card (Finset.biUnion s' t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
h : ¬∀ (s : Finset ι), Finset.Nonempty s → s ≠ univ → card s < card (Finset.biUnion s t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
push_neg  at h
case neg.intro.intro.intro
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
n✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n✝ →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.succ n✝
ih' :
  ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n✝ →
      (∀ (s' : Finset ι'), card s' ≤ card (Finset.biUnion s' t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
sne : Finset.Nonempty s
snu : s ≠ univ
sle : card (Finset.biUnion s t) ≤ card s
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
case neg
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
n✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n✝ →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.succ n✝
ih' :
  ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n✝ →
      (∀ (s' : Finset ι'), card s' ≤ card (Finset.biUnion s' t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
h : ∃ s, Finset.Nonempty s ∧ s ≠ univ ∧ card (Finset.biUnion s t) ≤ card s
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
rcases h with ⟨s, sne, snu, sle⟩
no goals
case neg.intro.intro.intro
ι✝ : Type u
α : Type v
inst✝² : DecidableEq α
t✝ : ι✝ → Finset α
inst✝¹ : Finite ι✝
ht✝ : ∀ (s : Finset ι✝), card s ≤ card (Finset.biUnion s t✝)
val✝¹ : Fintype ι✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)
val✝ : Fintype ι
n✝ : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n✝ →
      ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι],
        (∀ (s : Finset ι), card s ≤ card (Finset.biUnion s t)) →
          ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = Nat.succ n✝
ih' :
  ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n✝ →
      (∀ (s' : Finset ι'), card s' ≤ card (Finset.biUnion s' t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
sne : Finset.Nonempty s
snu : s ≠ univ
sle : card (Finset.biUnion s t) ≤ card s
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
exact hall_hard_inductive_step_B hn ht (@fun ι' => ih' ι')
  s sne snu (Nat.le_antisymm (ht _) sle)