Theorem: Matroid.isIso_emptyOn_emptyOn (Matroid/Old/_Equiv.lean)

State before:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M✝ : Matroid α✝
N✝ : Matroid β✝
B I D X Y : Set α✝
M : Matroid α✝
N : Matroid β✝
α : Type u_7
β : Type u_8
⊢ emptyOn α ≂ emptyOn β
Tactic:
rw [isIso_emptyOn_iff]
State after:
no goals