Theorem: Set.Finite.encard_eq_iff_nonempty_equiv (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:
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 β
ht : t.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 β
ht : t.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 β
ht : t.Finite
h✝ : Nonempty α
⊢ s.encard = t.encard ↔ Nonempty (↑s ≃ ↑t)
Tactic:
refine ⟨fun h ↦ ?_, fun ⟨e⟩ ↦ encard_congr e⟩
State after:
case inr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.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 β
ht : t.Finite
h✝ : Nonempty α
h : s.encard = t.encard
⊢ Nonempty (↑s ≃ ↑t)
Tactic:
obtain ⟨f, hf⟩ := ht.exists_bijOn_of_encard_eq h.symm
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
h✝ : Nonempty α
h : s.encard = t.encard
f : β → α
hf : BijOn f t s
⊢ Nonempty (↑s ≃ ↑t)

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
h✝ : Nonempty α
h : s.encard = t.encard
f : β → α
hf : BijOn f t s
⊢ Nonempty (↑s ≃ ↑t)
Tactic:
exact Nonempty.intro <| (hf.equiv _).symm
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
h✝ : IsEmpty α
⊢ s.encard = t.encard ↔ Nonempty (↑s ≃ ↑t)
Tactic:
simp only [s.eq_empty_of_isEmpty, eq_comm (a := (0 : ℕ∞)), encard_empty, encard_eq_zero]
State after:
case inl
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ t = ∅ ↔ Nonempty (↑∅ ≃ ↑t)

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

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

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

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

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

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

case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ Nonempty (↑∅ ≃ ↑t) → t = ∅
Tactic:
exact ⟨Equiv.equivOfIsEmpty _ _⟩
State after:
case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ Nonempty (↑∅ ≃ ↑t) → t = ∅

State before:
case inl.mpr
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
s : Set α
t : Set β
ht : t.Finite
h✝ : IsEmpty α
⊢ Nonempty (↑∅ ≃ ↑t) → t = ∅
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 β
ht : t.Finite
h✝ : IsEmpty α
e : ↑∅ ≃ ↑t
⊢ t = ∅

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