Theorem: Matroid.ModularCut.ExtIndep.diff_singleton_indep (Matroid/Extension.lean)

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : U.ExtIndep e I
⊢ M.Indep (I \ {e})
Tactic:
obtain (h | h) := h
State after:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : M.Indep I ∧ e ∉ I
⊢ M.Indep (I \ {e})

case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U ∧ e ∈ I
⊢ M.Indep (I \ {e})

State before:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : M.Indep I ∧ e ∉ I
⊢ M.Indep (I \ {e})

case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U ∧ e ∈ I
⊢ M.Indep (I \ {e})
Tactic:
exact h.1.diff _
State after:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U ∧ e ∈ I
⊢ M.Indep (I \ {e})

State before:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U ∧ e ∈ I
⊢ M.Indep (I \ {e})
Tactic:
exact h.1
State after:
no goals