Theorem: Fin.nonempty_embedding_iff_le_encard (Matroid/ForMathlib/Card.lean)

State before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ Nonempty (Fin n ↪ ↑s) ↔ ↑n ≤ s.encard
Tactic:
refine ⟨fun ⟨i⟩ ↦ ?_, fun h ↦ ?_⟩
State after:
case refine_1
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
x✝ : Nonempty (Fin n ↪ ↑s)
i : Fin n ↪ ↑s
⊢ ↑n ≤ s.encard

case refine_2
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : ↑n ≤ s.encard
⊢ Nonempty (Fin n ↪ ↑s)

State before:
case refine_2
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : ↑n ≤ s.encard
⊢ Nonempty (Fin n ↪ ↑s)
Tactic:
obtain ⟨t, hts, hcard⟩ := exists_subset_encard_eq h
State after:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
hcard : t.encard = ↑n
⊢ Nonempty (Fin n ↪ ↑s)

State before:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
hcard : t.encard = ↑n
⊢ Nonempty (Fin n ↪ ↑s)
Tactic:
have ht : t.Finite := finite_of_encard_eq_coe hcard
State after:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
hcard : t.encard = ↑n
ht : t.Finite
⊢ Nonempty (Fin n ↪ ↑s)

State before:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
hcard : t.encard = ↑n
ht : t.Finite
⊢ Nonempty (Fin n ↪ ↑s)
Tactic:
rw [← ht.cast_ncard_eq, Nat.cast_inj, ncard_eq_toFinset_card t ht] at hcard
State after:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
ht : t.Finite
hcard : ht.toFinset.card = n
⊢ Nonempty (Fin n ↪ ↑s)

State before:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
ht : t.Finite
hcard : ht.toFinset.card = n
⊢ Nonempty (Fin n ↪ ↑s)
Tactic:
refine ⟨(Finset.equivFinOfCardEq hcard).symm.toEmbedding.trans ?_ ⟩
State after:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
ht : t.Finite
hcard : ht.toFinset.card = n
⊢ { x // x ∈ ht.toFinset } ↪ ↑s

State before:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
ht : t.Finite
hcard : ht.toFinset.card = n
⊢ { x // x ∈ ht.toFinset } ↪ ↑s
Tactic:
simp only [Finite.mem_toFinset]
State after:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
ht : t.Finite
hcard : ht.toFinset.card = n
⊢ { x // x ∈ t } ↪ ↑s

State before:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
s t✝ : Set α
n : ℕ
h : ↑n ≤ s.encard
t : Set α
hts : t ⊆ s
ht : t.Finite
hcard : ht.toFinset.card = n
⊢ { x // x ∈ t } ↪ ↑s
Tactic:
exact embeddingOfSubset t s hts
State after:
no goals

State before:
case refine_1
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
x✝ : Nonempty (Fin n ↪ ↑s)
i : Fin n ↪ ↑s
⊢ ↑n ≤ s.encard
Tactic:
convert ((Equiv.Set.univ (Fin n)).toEmbedding.trans i).enccard_le
State after:
case h.e'_3
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
x✝ : Nonempty (Fin n ↪ ↑s)
i : Fin n ↪ ↑s
⊢ ↑n = univ.encard

State before:
case h.e'_3
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
x✝ : Nonempty (Fin n ↪ ↑s)
i : Fin n ↪ ↑s
⊢ ↑n = univ.encard
Tactic:
simp [encard_univ]
State after:
no goals