Theorem: Matroid.ModularCut.extIndep_aug (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
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)
Tactic:
obtain (he | he) := em' (M.Coloop e)
State after:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : ¬M.Coloop e
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)

case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : M.Coloop e
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)

State before:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : M.Coloop e
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)
Tactic:
have hrw : (U.delete {e}).ExtIndep e = U.ExtIndep e := by
  ext; simp [ExtIndep, he.mem_cl_iff_mem, ModularCut.mem_delete_elem_iff]
State after:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : M.Coloop e
hrw : (U.delete {e}).ExtIndep e = U.ExtIndep e
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)

State before:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : M.Coloop e
hrw : (U.delete {e}).ExtIndep e = U.ExtIndep e
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)
Tactic:
simp_rw [← hrw] at hInmax hBmax hI ⊢
State after:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.Coloop e
hrw : (U.delete {e}).ExtIndep e = U.ExtIndep e
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (U.delete {e}).ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (U.delete {e}).ExtIndep e I}
hI : (U.delete {e}).ExtIndep e I
⊢ ∃ x ∈ B \ I, (U.delete {e}).ExtIndep e (insert x I)

State before:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.Coloop e
hrw : (U.delete {e}).ExtIndep e = U.ExtIndep e
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (U.delete {e}).ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (U.delete {e}).ExtIndep e I}
hI : (U.delete {e}).ExtIndep e I
⊢ ∃ x ∈ B \ I, (U.delete {e}).ExtIndep e (insert x I)
Tactic:
exact (U.delete {e}).extIndep_aug_of_not_coloop (fun h ↦ h.mem_ground.2 rfl) hI hInmax hBmax
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✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : ¬M.Coloop e
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)
Tactic:
exact U.extIndep_aug_of_not_coloop he hI hInmax hBmax
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : M.Coloop e
⊢ (U.delete {e}).ExtIndep e = U.ExtIndep e
Tactic:
ext
State after:
case h.a
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : M.Coloop e
x✝ : Set α
⊢ (U.delete {e}).ExtIndep e x✝ ↔ U.ExtIndep e x✝

State before:
case h.a
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : M.Coloop e
x✝ : Set α
⊢ (U.delete {e}).ExtIndep e x✝ ↔ U.ExtIndep e x✝
Tactic:
simp [ExtIndep, he.mem_cl_iff_mem, ModularCut.mem_delete_elem_iff]
State after:
no goals