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 β
ht : t.Finite
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
Tactic:
obtain (hs | hs) := s.finite_or_infinite
State after:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Finite
⊢ 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 β
ht : t.Finite
hs : s.Infinite
⊢ 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 β
ht : t.Finite
hs : s.Infinite
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
Tactic:
rw [hs.encard_eq, top_le_iff, encard_eq_top_iff, Set.Infinite, iff_true_intro ht,
  not_true, false_iff]
State after:
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
⊢ ¬Nonempty (↑s ↪ ↑t)

State before:
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
⊢ ¬Nonempty (↑s ↪ ↑t)
Tactic:
rintro ⟨e⟩
State after:
case inr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
e : ↑s ↪ ↑t
⊢ False

State before:
case inr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
e : ↑s ↪ ↑t
⊢ False
Tactic:
have hle := e.enccard_le
State after:
case inr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
e : ↑s ↪ ↑t
hle : s.encard ≤ t.encard
⊢ False

State before:
case inr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
e : ↑s ↪ ↑t
hle : s.encard ≤ t.encard
⊢ False
Tactic:
rw [hs.encard_eq, top_le_iff, encard_eq_top_iff] at hle
State after:
case inr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
e : ↑s ↪ ↑t
hle : t.Infinite
⊢ False

State before:
case inr.intro
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
hs : s.Infinite
e : ↑s ↪ ↑t
hle : t.Infinite
⊢ False
Tactic:
exact hle ht
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 β
ht : t.Finite
hs : s.Finite
⊢ s.encard ≤ t.encard ↔ Nonempty (↑s ↪ ↑t)
Tactic:
exact hs.encard_le_iff_nonempty_embedding
State after:
no goals