no goals
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
as : List α
⊢ inj_on f as → 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 =>
    intro inj_on'
    cases (exists_of_mem_map h) with
    | intro x hx =>
      have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
      have h1 : a ∈ as := this ▸ hx.1
      have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
      rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
  | inr h =>
    intro inj_on'
    have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
    have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
    rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
no goals
case nil
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
⊢ inj_on 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 : inj_on f as → card (map f as) = card as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
cases Decidable.em (f a ∈ map f as) with
| inl h =>
  intro inj_on'
  cases (exists_of_mem_map h) with
  | intro x hx =>
    have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
    have h1 : a ∈ as := this ▸ hx.1
    have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
    rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
| inr h =>
  intro inj_on'
  have h1 : a ∉ as := fun h'' ↦ h (mem_map_of_mem _ h'')
  have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
  rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
⊢ card (map f (a :: as)) = card (a :: as)
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
intro inj_on'
no goals
case cons.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
⊢ card (map f (a :: as)) = card (a :: as)
cases (exists_of_mem_map h) with
| intro x hx =>
  have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
  have h1 : a ∈ as := this ▸ hx.1
  have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
  rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
this : x = a
⊢ card (map f (a :: as)) = card (a :: as)
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
⊢ card (map f (a :: as)) = card (a :: as)
have : x = a := inj_on' (mem_cons_of_mem _ hx.1) (mem_cons_self ..) hx.2
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
this : x = a
h1 : a ∈ as
⊢ card (map f (a :: as)) = card (a :: as)
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
this : x = a
⊢ card (map f (a :: as)) = card (a :: as)
have h1 : a ∈ as := this ▸ hx.1
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
this : x = a
h1 : a ∈ as
h2 : inj_on f as
⊢ card (map f (a :: as)) = card (a :: as)
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
this : x = a
h1 : a ∈ as
⊢ card (map f (a :: as)) = card (a :: as)
have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
no goals
case cons.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : f a ∈ map f as
inj_on' : inj_on f (a :: as)
x : α
hx : x ∈ as ∧ f x = f a
this : x = a
h1 : a ∈ as
h2 : inj_on f as
⊢ card (map f (a :: as)) = card (a :: as)
rw [map, card_cons_of_mem h, ih h2, card_cons_of_mem h1]
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
inj_on' : inj_on f (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 : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
⊢ inj_on f (a :: as) → card (map f (a :: as)) = card (a :: as)
intro inj_on'
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
inj_on' : inj_on f (a :: as)
h1 : ¬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 : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
inj_on' : inj_on f (a :: as)
⊢ card (map f (a :: as)) = card (a :: as)
have h1 : 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 : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
inj_on' : inj_on f (a :: as)
h1 : ¬a ∈ as
h2 : inj_on f 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 : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
inj_on' : inj_on f (a :: as)
h1 : ¬a ∈ as
⊢ card (map f (a :: as)) = card (a :: as)
have h2 : inj_on f as := inj_on_of_subset inj_on' (subset_cons _ _)
no goals
case cons.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
as : List α
ih : inj_on f as → card (map f as) = card as
h : ¬f a ∈ map f as
inj_on' : inj_on f (a :: as)
h1 : ¬a ∈ as
h2 : inj_on f as
⊢ card (map f (a :: as)) = card (a :: as)
rw [map, card_cons_of_not_mem h, card_cons_of_not_mem h1, ih h2]