case inl
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
h : Set.Finite s
⊢ ncard s ≤ ncard t

case inr
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
h : Set.Infinite s
⊢ ncard s ≤ ncard t
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard s ≤ ncard t
cases' s.finite_or_infinite with h h
case h.e'_3
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
h : Set.Infinite s
⊢ ncard s = 0
case inr
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
h : Set.Infinite s
⊢ ncard s ≤ ncard t
convert Nat.zero_le _
no goals
case h.e'_3
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
h : Set.Infinite s
⊢ ncard s = 0
rw [h.ncard]
case inl
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
h : Set.Finite s
this : Finite ↑s
⊢ ncard s ≤ ncard t
case inl
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
h : Set.Finite s
⊢ ncard s ≤ ncard t
haveI := h.to_subtype
case inl
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
h : Set.Finite s
this : Finite ↑s
⊢ Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
case inl
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
h : Set.Finite s
this : Finite ↑s
⊢ ncard s ≤ ncard t
rw [ncard_eq_toFinset_card _ ht, ncard_eq_toFinset_card _ (toFinite s)]
no goals
case inl
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
h : Set.Finite s
this : Finite ↑s
⊢ Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
exact Finset.card_le_card_of_inj_on f (by simpa) (by simpa)
no goals
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
h : Set.Finite s
this : Finite ↑s
⊢ ∀ (a : α), a ∈ Finite.toFinset (_ : Set.Finite s) → f a ∈ Finite.toFinset ht
simpa
no goals
α : Type u_2
β : Type u_1
s t✝ : Set α
a b x y : α
f✝ : α → β
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
h : Set.Finite s
this : Finite ↑s
⊢ ∀ (a₁ : α),
    a₁ ∈ Finite.toFinset (_ : Set.Finite s) →
      ∀ (a₂ : α), a₂ ∈ Finite.toFinset (_ : Set.Finite s) → f a₁ = f a₂ → a₁ = a₂
simpa