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

State before:
α : Type u_1
M✝ N : Matroid α
e f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
⊢ Nonempty (N ≤i M) ↔ Nonempty (N ≤i M.simplification)
Tactic:
refine ⟨fun ⟨e⟩ ↦ ?_, fun ⟨e⟩ ↦ ⟨e.trans M.simplification_restriction.minor.isoMinor⟩⟩
State after:
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
x✝ : Nonempty (N ≤i M)
e : N ≤i M
⊢ Nonempty (N ≤i M.simplification)

State before:
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
x✝ : Nonempty (N ≤i M)
e : N ≤i M
⊢ Nonempty (N ≤i M.simplification)
Tactic:
obtain ⟨M₀, hM₀, ⟨i, -⟩⟩ := e.exists_iso
State after:
case intro.intro.intro
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
x✝ : Nonempty (N ≤i M)
e : N ≤i M
M₀ : Matroid β
hM₀ : M₀ ≤m M
i : N ≂ M₀
⊢ Nonempty (N ≤i M.simplification)

State before:
case intro.intro.intro
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
x✝ : Nonempty (N ≤i M)
e : N ≤i M
M₀ : Matroid β
hM₀ : M₀ ≤m M
i : N ≂ M₀
⊢ Nonempty (N ≤i M.simplification)
Tactic:
obtain ⟨M', hM₀M', hM'⟩ := hM₀.exists_minor_isSimplification (hN.of_iso i)
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
x✝ : Nonempty (N ≤i M)
e : N ≤i M
M₀ : Matroid β
hM₀ : M₀ ≤m M
i : N ≂ M₀
M' : Matroid β
hM₀M' : M₀ ≤m M'
hM' : M'.IsSimplification M
⊢ Nonempty (N ≤i M.simplification)

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
β : Type u_2
hN : N.Simple
M : Matroid β
x✝ : Nonempty (N ≤i M)
e : N ≤i M
M₀ : Matroid β
hM₀ : M₀ ≤m M
i : N ≂ M₀
M' : Matroid β
hM₀M' : M₀ ≤m M'
hM' : M'.IsSimplification M
⊢ Nonempty (N ≤i M.simplification)
Tactic:
exact ⟨i.isoMinor.trans
  (hM₀M'.isoMinor.trans (hM'.iso (M.simplification_isSimplification)).isoMinor)⟩
State after:
no goals