-- Mathlib/Data/Finset/Card.lean
lemma card_le_card_of_injective {f : s → t} (hf : f.Injective) : #s ≤ #t

Proof state:
case inr.intro.hf
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : { x // x ∈ s } → { x // x ∈ t }
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a => ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
⊢ ∀ a ∈ s, f' a ∈ t

Tactic:
aesop

Result:
no goals

Proof state:
case inr.intro.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : { x // x ∈ s } → { x // x ∈ t }
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a => ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
⊢ Set.InjOn f' ↑s

Tactic:
intro a₁ ha₁ a₂ ha₂ haa

Result:
case inr.intro.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : { x // x ∈ s } → { x // x ∈ t }
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a => ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ ↑s
a₂ : α
ha₂ : a₂ ∈ ↑s
haa : f' a₁ = f' a₂
⊢ a₁ = a₂

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : { x // x ∈ s } → { x // x ∈ t }
hf : Injective f
⊢ #s ≤ #t

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀⟩

Result:
case inl
α : Type u_1
β : Type u_2
t : Finset β
f : { x // x ∈ ∅ } → { x // x ∈ t }
hf : Injective f
⊢ #∅ ≤ #t

case inr.intro
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : { x // x ∈ s } → { x // x ∈ t }
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
⊢ #s ≤ #t

Proof state:
case inl
α : Type u_1
β : Type u_2
t : Finset β
f : { x // x ∈ ∅ } → { x // x ∈ t }
hf : Injective f
⊢ #∅ ≤ #t

Tactic:
simp

Result:
no goals

Proof state:
case inr.intro.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : { x // x ∈ s } → { x // x ∈ t }
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a => ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
haa : f (if h : True then ⟨a₁, ⋯⟩ else ⟨a₀, ha₀⟩) = f (if h : True then ⟨a₂, ⋯⟩ else ⟨a₀, ha₀⟩)
⊢ a₁ = a₂

Tactic:
exact Subtype.ext_iff.mp (hf haa)

Result:
no goals

Proof state:
case inr.intro.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : { x // x ∈ s } → { x // x ∈ t }
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a => ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
haa : f' a₁ = f' a₂
⊢ a₁ = a₂

Tactic:
simp only [f', ha₁, ha₂, ← Subtype.ext_iff] at haa

Result:
case inr.intro.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : { x // x ∈ s } → { x // x ∈ t }
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a => ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
haa : f (if h : True then ⟨a₁, ⋯⟩ else ⟨a₀, ha₀⟩) = f (if h : True then ⟨a₂, ⋯⟩ else ⟨a₀, ha₀⟩)
⊢ a₁ = a₂

Proof state:
case inr.intro.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : { x // x ∈ s } → { x // x ∈ t }
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a => ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ ↑s
a₂ : α
ha₂ : a₂ ∈ ↑s
haa : f' a₁ = f' a₂
⊢ a₁ = a₂

Tactic:
rw [mem_coe] at ha₁ ha₂

Result:
case inr.intro.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : { x // x ∈ s } → { x // x ∈ t }
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a => ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
haa : f' a₁ = f' a₂
⊢ a₁ = a₂

Proof state:
case inr.intro
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : { x // x ∈ s } → { x // x ∈ t }
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a => ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
⊢ #s ≤ #t

Tactic:
apply card_le_card_of_injOn f'

Result:
case inr.intro.hf
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : { x // x ∈ s } → { x // x ∈ t }
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a => ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
⊢ ∀ a ∈ s, f' a ∈ t

case inr.intro.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : { x // x ∈ s } → { x // x ∈ t }
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a => ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
⊢ Set.InjOn f' ↑s

Proof state:
case inr.intro
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : { x // x ∈ s } → { x // x ∈ t }
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
⊢ #s ≤ #t

Tactic:
let f' : α → β := fun a => f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩)

Result:
case inr.intro
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : { x // x ∈ s } → { x // x ∈ t }
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a => ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
⊢ #s ≤ #t