no goals
α : Type u_1
β : Type ?u.133040
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
i : ℕ
h₁ : i ≤ ncard s
⊢ i + ncard ∅ ≤ ncard s
simpa
no goals
α : Type u_1
β : Type ?u.133040
s✝ t✝ : Set α
a b x y : α
f : α → β
s : Set α
i : ℕ
h₁ : i ≤ ncard s
t : Set α
ht : ∅ ⊆ t ∧ t ⊆ s ∧ ncard t = i + ncard ∅
⊢ ncard t = i
simpa using ht.2.2