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

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : M.Nonempty
⊢ N.Nonempty
Tactic:
obtain ⟨x,hx⟩ := M.ground_nonempty
State after:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : M.Nonempty
x : α
hx : x ∈ M.E
⊢ N.Nonempty

State before:
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : M.Nonempty
x : α
hx : x ∈ M.E
⊢ N.Nonempty
Tactic:
exact ⟨e ⟨x,hx⟩, Subtype.coe_prop (e ⟨x, hx⟩)⟩
State after:
no goals