Theorem: Matroid.Iso.right_eq_empty (Matroid/Equiv.lean)

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : emptyOn α ≂ N
⊢ N = emptyOn β
Tactic:
rw [← ground_eq_empty_iff]
State after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : emptyOn α ≂ N
⊢ N.E = ∅

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : emptyOn α ≂ N
⊢ N.E = ∅
Tactic:
have h := e.toEquiv
State after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : emptyOn α ≂ N
h : ↑(emptyOn α).E ≃ ↑N.E
⊢ N.E = ∅

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : emptyOn α ≂ N
h : ↑(emptyOn α).E ≃ ↑N.E
⊢ N.E = ∅
Tactic:
simp only [emptyOn_ground] at h
State after:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : emptyOn α ≂ N
h : ↑∅ ≃ ↑N.E
⊢ N.E = ∅

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : emptyOn α ≂ N
h : ↑∅ ≃ ↑N.E
⊢ N.E = ∅
Tactic:
exact isEmpty_coe_sort.mp h.symm.isEmpty
State after:
no goals