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

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : U.ExtIndep e I
hJI : J ⊆ I
⊢ U.ExtIndep e J
Tactic:
obtain (heJ | heJ) := em (e ∈ J)
State after:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : U.ExtIndep e I
hJI : J ⊆ I
heJ : e ∈ J
⊢ U.ExtIndep e J

case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : U.ExtIndep e I
hJI : J ⊆ I
heJ : e ∉ J
⊢ U.ExtIndep e J

State before:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : U.ExtIndep e I
hJI : J ⊆ I
heJ : e ∉ J
⊢ U.ExtIndep e J
Tactic:
rw [extIndep_iff_of_not_mem heJ]
State after:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : U.ExtIndep e I
hJI : J ⊆ I
heJ : e ∉ J
⊢ M.Indep J

State before:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : U.ExtIndep e I
hJI : J ⊆ I
heJ : e ∉ J
⊢ M.Indep J
Tactic:
exact h.diff_singleton_indep.subset (subset_diff_singleton hJI heJ)
State after:
no goals

State before:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : U.ExtIndep e I
hJI : J ⊆ I
heJ : e ∈ J
⊢ U.ExtIndep e J
Tactic:
rw [extIndep_iff_of_mem (hJI heJ)] at h
State after:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hJI : J ⊆ I
heJ : e ∈ J
⊢ U.ExtIndep e J

State before:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hJI : J ⊆ I
heJ : e ∈ J
⊢ U.ExtIndep e J
Tactic:
rw [extIndep_iff_of_mem heJ, and_iff_right (h.1.subset (diff_subset_diff_left hJI))]
State after:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hJI : J ⊆ I
heJ : e ∈ J
⊢ M.cl (J \ {e}) ∉ U

State before:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hJI : J ⊆ I
heJ : e ∈ J
⊢ M.cl (J \ {e}) ∉ U
Tactic:
exact fun hJU ↦ h.2 <| U.cl_superset_mem' hJU <| diff_subset_diff_left hJI
State after:
no goals