Theorem: Matroid.IsIso.empty_or_nonempty_iso (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 β
h : M ≂ N
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Tactic:
obtain (⟨rfl,rfl⟩ | ⟨⟨e⟩⟩) := h
State after:
case 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 α
⊢ emptyOn α = emptyOn α ∧ emptyOn β = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty ((emptyOn α).Iso (emptyOn β))

case 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 β
e : M.Iso N
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)

State before:
case 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 β
e : M.Iso N
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Tactic:
cases isEmpty_or_nonempty α
State after:
case inr.intro.inl
α : 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 β
e : M.Iso N
h✝ : IsEmpty α
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)

case inr.intro.inr
α : 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 β
e : M.Iso N
h✝ : Nonempty α
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)

State before:
case inr.intro.inr
α : 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 β
e : M.Iso N
h✝ : Nonempty α
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Tactic:
cases isEmpty_or_nonempty β
State after:
case inr.intro.inr.inl
α : 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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)

case inr.intro.inr.inr
α : 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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)

State before:
case inr.intro.inr.inr
α : 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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Tactic:
right
State after:
case inr.intro.inr.inr.h
α : 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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)

State before:
case inr.intro.inr.inr.h
α : 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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Tactic:
exact ⟨by assumption, by assumption, ⟨e⟩⟩
State after:
no goals

State before:
case 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 α
⊢ emptyOn α = emptyOn α ∧ emptyOn β = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty ((emptyOn α).Iso (emptyOn β))
Tactic:
exact Or.inl ⟨rfl,rfl⟩
State after:
no goals

State before:
case inr.intro.inl
α : 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 β
e : M.Iso N
h✝ : IsEmpty α
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Tactic:
left
State after:
case inr.intro.inl.h
α : 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 β
e : M.Iso N
h✝ : IsEmpty α
⊢ M = emptyOn α ∧ N = emptyOn β

State before:
case inr.intro.inl.h
α : 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 β
e : M.Iso N
h✝ : IsEmpty α
⊢ M = emptyOn α ∧ N = emptyOn β
Tactic:
obtain rfl := eq_emptyOn M
State after:
case inr.intro.inl.h
α : 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 α
N : Matroid β
h✝ : IsEmpty α
e : (emptyOn α).Iso N
⊢ emptyOn α = emptyOn α ∧ N = emptyOn β

State before:
case inr.intro.inl.h
α : 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 α
N : Matroid β
h✝ : IsEmpty α
e : (emptyOn α).Iso N
⊢ emptyOn α = emptyOn α ∧ N = emptyOn β
Tactic:
simp [isIso_emptyOn_iff.1 e.symm.isIso]
State after:
no goals

State before:
case inr.intro.inr.inl
α : 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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ M = emptyOn α ∧ N = emptyOn β ∨ Nonempty α ∧ Nonempty β ∧ Nonempty (M.Iso N)
Tactic:
left
State after:
case inr.intro.inr.inl.h
α : 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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ M = emptyOn α ∧ N = emptyOn β

State before:
case inr.intro.inr.inl.h
α : 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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ M = emptyOn α ∧ N = emptyOn β
Tactic:
obtain rfl := eq_emptyOn N
State after:
case inr.intro.inr.inl.h
α : 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 α
h✝¹ : Nonempty α
h✝ : IsEmpty β
e : M.Iso (emptyOn β)
⊢ M = emptyOn α ∧ emptyOn β = emptyOn β

State before:
case inr.intro.inr.inl.h
α : 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 α
h✝¹ : Nonempty α
h✝ : IsEmpty β
e : M.Iso (emptyOn β)
⊢ M = emptyOn α ∧ emptyOn β = emptyOn β
Tactic:
simp [isIso_emptyOn_iff.1 e.isIso]
State after:
no goals

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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ Nonempty α
Tactic:
assumption
State after:
no goals

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 β
e : M.Iso N
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ Nonempty β
Tactic:
assumption
State after:
no goals