Theorem: Matroid.IsSimplification.exists_of_strictRestriction (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
hN : N.IsSimplification M
hNM : N <r M
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E
Tactic:
obtain ⟨e, heM, heN⟩ := exists_of_ssubset hNM.ssubset
State after:
case intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
hN : N.IsSimplification M
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E

State before:
case intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
hN : N.IsSimplification M
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E
Tactic:
obtain (he | he) := M.loop_or_nonloop e
State after:
case intro.intro.inl
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
hN : N.IsSimplification M
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Loop e
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E

case intro.intro.inr
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
hN : N.IsSimplification M
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E

State before:
case intro.intro.inr
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
hN : N.IsSimplification M
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E
Tactic:
obtain ⟨f, hN⟩ := hN
State after:
case intro.intro.inr.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
f : M.parallelClasses.RepFun
hN : N = M ↾ ⇑f '' {e | M.Nonloop e}
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E

State before:
case intro.intro.inr.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
f : M.parallelClasses.RepFun
hN : N = M ↾ ⇑f '' {e | M.Nonloop e}
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E
Tactic:
refine .inr ⟨e, f e, f.rel_apply he, heM, heN, ?_⟩
State after:
case intro.intro.inr.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
f : M.parallelClasses.RepFun
hN : N = M ↾ ⇑f '' {e | M.Nonloop e}
⊢ f e ∈ N.E

State before:
case intro.intro.inr.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
f : M.parallelClasses.RepFun
hN : N = M ↾ ⇑f '' {e | M.Nonloop e}
⊢ f e ∈ N.E
Tactic:
simp only [hN, restrict_ground_eq, mem_image, mem_setOf_eq]
State after:
case intro.intro.inr.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
f : M.parallelClasses.RepFun
hN : N = M ↾ ⇑f '' {e | M.Nonloop e}
⊢ ∃ x, M.Nonloop x ∧ f x = f e

State before:
case intro.intro.inr.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Nonloop e
f : M.parallelClasses.RepFun
hN : N = M ↾ ⇑f '' {e | M.Nonloop e}
⊢ ∃ x, M.Nonloop x ∧ f x = f e
Tactic:
exact ⟨e, he, rfl⟩
State after:
no goals

State before:
case intro.intro.inl
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
hN : N.IsSimplification M
hNM : N <r M
e : α
heM : e ∈ M.E
heN : e ∉ N.E
he : M.Loop e
⊢ (∃ e, M.Loop e ∧ e ∉ N.E) ∨ ∃ e f, M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E
Tactic:
exact .inl ⟨e, he, heN⟩
State after:
no goals