Theorem: Matroid.Simple.of_iso (Matroid/Simple.lean)

State before:
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
⊢ N.Simple
Tactic:
obtain (h | h) := isEmpty_or_nonempty β
State after:
case inl
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
h : IsEmpty β
⊢ N.Simple

case inr
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
h : Nonempty β
⊢ N.Simple

State before:
case inr
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
h : Nonempty β
⊢ N.Simple
Tactic:
obtain ⟨f, hf, rfl⟩ := i.exists_eq_map
State after:
case inr.intro.intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
h : Nonempty β
f : α → β
hf : InjOn f M.E
i : M ≂ M.map f hf
⊢ (M.map f hf).Simple

State before:
case inr.intro.intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
β : Type u_2
hM : M.Simple
h : Nonempty β
f : α → β
hf : InjOn f M.E
i : M ≂ M.map f hf
⊢ (M.map f hf).Simple
Tactic:
exact hM.map hf
State after:
no goals

State before:
case inl
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
h : IsEmpty β
⊢ N.Simple
Tactic:
rw [eq_emptyOn N]
State after:
case inl
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
h : IsEmpty β
⊢ (emptyOn β).Simple

State before:
case inl
α : Type u_1
M N✝ : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
N : Matroid β
hM : M.Simple
i : M ≂ N
h : IsEmpty β
⊢ (emptyOn β).Simple
Tactic:
infer_instance
State after:
no goals