Theorem: Set.Finite.encard_le_iff_nonempty_embedding (Matroid/ForMathlib/Other.lean)

State before:
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
Tactic:
cases isEmpty_or_nonempty β
State after:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)

case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : Nonempty β
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)

State before:
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : Nonempty β
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
Tactic:
refine ⟨fun h ↦ ?_, fun ⟨e⟩ ↦ e.enccard_le⟩
State after:
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : Nonempty β
h : s.encard ≤ t.encard
⊢ Nonempty (↑s ↪ ↑t)

State before:
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : Nonempty β
h : s.encard ≤ t.encard
⊢ Nonempty (↑s ↪ ↑t)
Tactic:
obtain ⟨f, hst, hf⟩ := hs.exists_injOn_of_encard_le h
State after:
case inr.intro.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f✝ : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : Nonempty β
h : s.encard ≤ t.encard
f : α → β
hst : s ⊆ f ⁻¹' t
hf : InjOn f s
⊢ Nonempty (↑s ↪ ↑t)

State before:
case inr.intro.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f✝ : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : Nonempty β
h : s.encard ≤ t.encard
f : α → β
hst : s ⊆ f ⁻¹' t
hf : InjOn f s
⊢ Nonempty (↑s ↪ ↑t)
Tactic:
exact ⟨codRestrict (s.restrict f) t (fun x ↦ by aesop), hf.injective.codRestrict _⟩
State after:
no goals

State before:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
Tactic:
simp only [t.eq_empty_of_isEmpty, encard_empty, nonpos_iff_eq_zero, encard_eq_zero]
State after:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ s = ∅ ↔ Nonempty (↑s ↪ ↑∅)

State before:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ s = ∅ ↔ Nonempty (↑s ↪ ↑∅)
Tactic:
constructor
State after:
case inl.mp
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ s = ∅ → Nonempty (↑s ↪ ↑∅)

case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ Nonempty (↑s ↪ ↑∅) → s = ∅

State before:
case inl.mp
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ s = ∅ → Nonempty (↑s ↪ ↑∅)

case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ Nonempty (↑s ↪ ↑∅) → s = ∅
Tactic:
rintro rfl
State after:
case inl.mp
α : Type u_1
β : Type u_2
s s₁ s₂ t✝ t' : Set α
f : α → β
t : Set β
h✝ : IsEmpty β
hs : ∅.Finite
⊢ Nonempty (↑∅ ↪ ↑∅)

case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ Nonempty (↑s ↪ ↑∅) → s = ∅

State before:
case inl.mp
α : Type u_1
β : Type u_2
s s₁ s₂ t✝ t' : Set α
f : α → β
t : Set β
h✝ : IsEmpty β
hs : ∅.Finite
⊢ Nonempty (↑∅ ↪ ↑∅)

case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ Nonempty (↑s ↪ ↑∅) → s = ∅
Tactic:
exact ⟨Embedding.ofIsEmpty⟩
State after:
case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ Nonempty (↑s ↪ ↑∅) → s = ∅

State before:
case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
⊢ Nonempty (↑s ↪ ↑∅) → s = ∅
Tactic:
rintro ⟨e⟩
State after:
case inl.mpr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
e : ↑s ↪ ↑∅
⊢ s = ∅

State before:
case inl.mpr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : IsEmpty β
e : ↑s ↪ ↑∅
⊢ s = ∅
Tactic:
exact isEmpty_coe_sort.1 e.toFun.isEmpty
State after:
no goals

State before:
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f✝ : α → β
s : Set α
t : Set β
hs : s.Finite
h✝ : Nonempty β
h : s.encard ≤ t.encard
f : α → β
hst : s ⊆ f ⁻¹' t
hf : InjOn f s
x : ↑s
⊢ s.restrict f x ∈ t
Tactic:
aesop
State after:
no goals