no goals
α : Type u_1
β : Type ?u.137499
s t : Set α
a b x y : α
f : α → β
n : ℕ
hst : 2 * n < ncard (s ∪ t)
⊢ ∃ r, n < ncard r ∧ (r ⊆ s ∨ r ⊆ t)
classical
have hu := Finite_of_ncard_ne_zero ((Nat.zero_le _).trans_lt hst).ne.symm
rw [ncard_eq_toFinset_card _ hu,
  Finite.toFinset_union (hu.subset (subset_union_left _ _))
    (hu.subset (subset_union_right _ _))] at hst
obtain ⟨r', hnr', hr'⟩ := Finset.exists_subset_or_subset_of_two_mul_lt_card hst
exact ⟨r', by simpa, by simpa using hr'⟩
α : Type u_1
β : Type ?u.137499
s t : Set α
a b x y : α
f : α → β
n : ℕ
hst : 2 * n < ncard (s ∪ t)
hu : Set.Finite (s ∪ t)
⊢ ∃ r, n < ncard r ∧ (r ⊆ s ∨ r ⊆ t)
α : Type u_1
β : Type ?u.137499
s t : Set α
a b x y : α
f : α → β
n : ℕ
hst : 2 * n < ncard (s ∪ t)
⊢ ∃ r, n < ncard r ∧ (r ⊆ s ∨ r ⊆ t)
have hu := Finite_of_ncard_ne_zero ((Nat.zero_le _).trans_lt hst).ne.symm
α : Type u_1
β : Type ?u.137499
s t : Set α
a b x y : α
f : α → β
n : ℕ
hu : Set.Finite (s ∪ t)
hst : 2 * n < Finset.card (Finite.toFinset (_ : Set.Finite s) ∪ Finite.toFinset (_ : Set.Finite t))
⊢ ∃ r, n < ncard r ∧ (r ⊆ s ∨ r ⊆ t)
α : Type u_1
β : Type ?u.137499
s t : Set α
a b x y : α
f : α → β
n : ℕ
hst : 2 * n < ncard (s ∪ t)
hu : Set.Finite (s ∪ t)
⊢ ∃ r, n < ncard r ∧ (r ⊆ s ∨ r ⊆ t)
rw [ncard_eq_toFinset_card _ hu,
  Finite.toFinset_union (hu.subset (subset_union_left _ _))
    (hu.subset (subset_union_right _ _))] at hst
case intro.intro
α : Type u_1
β : Type ?u.137499
s t : Set α
a b x y : α
f : α → β
n : ℕ
hu : Set.Finite (s ∪ t)
hst : 2 * n < Finset.card (Finite.toFinset (_ : Set.Finite s) ∪ Finite.toFinset (_ : Set.Finite t))
r' : Finset α
hnr' : n < Finset.card r'
hr' : r' ⊆ Finite.toFinset (_ : Set.Finite s) ∨ r' ⊆ Finite.toFinset (_ : Set.Finite t)
⊢ ∃ r, n < ncard r ∧ (r ⊆ s ∨ r ⊆ t)
α : Type u_1
β : Type ?u.137499
s t : Set α
a b x y : α
f : α → β
n : ℕ
hu : Set.Finite (s ∪ t)
hst : 2 * n < Finset.card (Finite.toFinset (_ : Set.Finite s) ∪ Finite.toFinset (_ : Set.Finite t))
⊢ ∃ r, n < ncard r ∧ (r ⊆ s ∨ r ⊆ t)
obtain ⟨r', hnr', hr'⟩ := Finset.exists_subset_or_subset_of_two_mul_lt_card hst
no goals
case intro.intro
α : Type u_1
β : Type ?u.137499
s t : Set α
a b x y : α
f : α → β
n : ℕ
hu : Set.Finite (s ∪ t)
hst : 2 * n < Finset.card (Finite.toFinset (_ : Set.Finite s) ∪ Finite.toFinset (_ : Set.Finite t))
r' : Finset α
hnr' : n < Finset.card r'
hr' : r' ⊆ Finite.toFinset (_ : Set.Finite s) ∨ r' ⊆ Finite.toFinset (_ : Set.Finite t)
⊢ ∃ r, n < ncard r ∧ (r ⊆ s ∨ r ⊆ t)
exact ⟨r', by simpa, by simpa using hr'⟩
no goals
α : Type u_1
β : Type ?u.137499
s t : Set α
a b x y : α
f : α → β
n : ℕ
hu : Set.Finite (s ∪ t)
hst : 2 * n < Finset.card (Finite.toFinset (_ : Set.Finite s) ∪ Finite.toFinset (_ : Set.Finite t))
r' : Finset α
hnr' : n < Finset.card r'
hr' : r' ⊆ Finite.toFinset (_ : Set.Finite s) ∨ r' ⊆ Finite.toFinset (_ : Set.Finite t)
⊢ n < ncard ↑r'
simpa
no goals
α : Type u_1
β : Type ?u.137499
s t : Set α
a b x y : α
f : α → β
n : ℕ
hu : Set.Finite (s ∪ t)
hst : 2 * n < Finset.card (Finite.toFinset (_ : Set.Finite s) ∪ Finite.toFinset (_ : Set.Finite t))
r' : Finset α
hnr' : n < Finset.card r'
hr' : r' ⊆ Finite.toFinset (_ : Set.Finite s) ∨ r' ⊆ Finite.toFinset (_ : Set.Finite t)
⊢ ↑r' ⊆ s ∨ ↑r' ⊆ t
simpa using hr'