no goals
α : Type u_1
β : Type ?u.11853
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
⊢ ncard s ≤ ncard (insert a s)
classical
refine'
  s.finite_or_infinite.elim (fun h ↦ _) (fun h ↦ by (rw [h.ncard]; exact Nat.zero_le _))
rw [ncard_insert_eq_ite h]; split_ifs <;> simp
α : Type u_1
β : Type ?u.11853
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
h : Set.Finite s
⊢ ncard s ≤ ncard (insert a s)
α : Type u_1
β : Type ?u.11853
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
⊢ ncard s ≤ ncard (insert a s)
refine'
  s.finite_or_infinite.elim (fun h ↦ _) (fun h ↦ by (rw [h.ncard]; exact Nat.zero_le _))
α : Type u_1
β : Type ?u.11853
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
h : Set.Finite s
⊢ ncard s ≤ if a ∈ s then ncard s else ncard s + 1
α : Type u_1
β : Type ?u.11853
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
h : Set.Finite s
⊢ ncard s ≤ ncard (insert a s)
rw [ncard_insert_eq_ite h]
no goals
α : Type u_1
β : Type ?u.11853
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
h : Set.Finite s
⊢ ncard s ≤ if a ∈ s then ncard s else ncard s + 1
split_ifs <;> simp
no goals
α : Type u_1
β : Type ?u.11853
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
h : Set.Infinite s
⊢ ncard s ≤ ncard (insert a s)
(rw [h.ncard]; exact Nat.zero_le _)
α : Type u_1
β : Type ?u.11853
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
h : Set.Infinite s
⊢ 0 ≤ ncard (insert a s)
α : Type u_1
β : Type ?u.11853
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
h : Set.Infinite s
⊢ ncard s ≤ ncard (insert a s)
rw [h.ncard]
no goals
α : Type u_1
β : Type ?u.11853
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
h : Set.Infinite s
⊢ 0 ≤ ncard (insert a s)
exact Nat.zero_le _