no goals
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
as : List α
⊢ card (map f as) ≤ card as
induction as with
| nil => simp
| cons a as ih =>
  cases Decidable.em (f a ∈ map f as) with
  | inl h =>
    rw [map, card_cons_of_mem h]
    apply Nat.le_trans ih (card_le_card_cons ..)
  | inr h =>
    have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
    rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
    exact Nat.add_le_add_right ih _
no goals
case nil
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
⊢ card (map f []) ≤ card []
simp
no goals
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
⊢ card (map f (a :: as)) ≤ card (a :: as)
cases Decidable.em (f a ∈ map f as) with
| inl h =>
  rw [map, card_cons_of_mem h]
  apply Nat.le_trans ih (card_le_card_cons ..)
| inr h =>
  have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
  rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
  exact Nat.add_le_add_right ih _
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : f a ∈ map f as
⊢ card (map f as) ≤ card (a :: as)
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : f a ∈ map f as
⊢ card (map f (a :: as)) ≤ card (a :: as)
rw [map, card_cons_of_mem h]
no goals
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : f a ∈ map f as
⊢ card (map f as) ≤ card (a :: as)
apply Nat.le_trans ih (card_le_card_cons ..)
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : ¬f a ∈ map f as
this : ¬a ∈ as
⊢ card (map f (a :: as)) ≤ card (a :: as)
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : ¬f a ∈ map f as
⊢ card (map f (a :: as)) ≤ card (a :: as)
have : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : ¬f a ∈ map f as
this : ¬a ∈ as
⊢ card (map f as) + 1 ≤ card as + 1
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : ¬f a ∈ map f as
this : ¬a ∈ as
⊢ card (map f (a :: as)) ≤ card (a :: as)
rw [map, card_cons_of_not_mem h, card_cons_of_not_mem this]
no goals
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : card (map f as) ≤ card as
h : ¬f a ∈ map f as
this : ¬a ∈ as
⊢ card (map f as) + 1 ≤ card as + 1
exact Nat.add_le_add_right ih _