Theorem: Matroid.isIso_emptyOn_iff (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 β✝
M : Matroid α
β : Type u_7
⊢ M ≂ emptyOn β ↔ M = emptyOn α
Tactic:
constructor
State after:
case mp
α : 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 β✝
M : Matroid α
β : Type u_7
⊢ M ≂ emptyOn β → M = emptyOn α

case mpr
α : 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 β✝
M : Matroid α
β : Type u_7
⊢ M = emptyOn α → M ≂ emptyOn β

State before:
case mpr
α : 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 β✝
M : Matroid α
β : Type u_7
⊢ M = emptyOn α → M ≂ emptyOn β
Tactic:
rintro rfl
State after:
case mpr
α : 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
⊢ emptyOn α ≂ emptyOn β

State before:
case mpr
α : 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
⊢ emptyOn α ≂ emptyOn β
Tactic:
exact Or.inl ⟨rfl, rfl⟩
State after:
no goals

State before:
case mp
α : 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 β✝
M : Matroid α
β : Type u_7
⊢ M ≂ emptyOn β → M = emptyOn α
Tactic:
rintro (⟨rfl,-⟩ | ⟨⟨i⟩⟩ )
State after:
case mp.inl.intro
α : 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
⊢ emptyOn α = emptyOn α

case mp.inr.intro
α : 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 β✝
M : Matroid α
β : Type u_7
i : M.Iso (emptyOn β)
⊢ M = emptyOn α

State before:
case mp.inl.intro
α : 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
⊢ emptyOn α = emptyOn α

case mp.inr.intro
α : 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 β✝
M : Matroid α
β : Type u_7
i : M.Iso (emptyOn β)
⊢ M = emptyOn α
Tactic:
rfl
State after:
case mp.inr.intro
α : 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 β✝
M : Matroid α
β : Type u_7
i : M.Iso (emptyOn β)
⊢ M = emptyOn α

State before:
case mp.inr.intro
α : 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 β✝
M : Matroid α
β : Type u_7
i : M.Iso (emptyOn β)
⊢ M = emptyOn α
Tactic:
rw [← ground_eq_empty_iff, ← i.symm.image_ground]
State after:
case mp.inr.intro
α : 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 β✝
M : Matroid α
β : Type u_7
i : M.Iso (emptyOn β)
⊢ ↑i.symm.toPartialEquiv '' (emptyOn β).E = ∅

State before:
case mp.inr.intro
α : 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 β✝
M : Matroid α
β : Type u_7
i : M.Iso (emptyOn β)
⊢ ↑i.symm.toPartialEquiv '' (emptyOn β).E = ∅
Tactic:
simp
State after:
no goals