Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax :
  ¬(M.cl (I \ {e}) = M.cl (insert e M.E \ {e}) ∧ ((e ∈ I ↔ M.cl (insert e M.E \ {e}) ∈ U) → e ∉ insert e M.E) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (insert e M.E \ {e})) ∧ e ∈ I ∧ M.cl (insert e M.E \ {e}) ∈ U)
hBmax :
  M.cl (B \ {e}) = M.cl (insert e M.E \ {e}) ∧ ((e ∈ B ↔ M.cl (insert e M.E \ {e}) ∈ U) → e ∉ insert e M.E) ∨
    (M.cl (B \ {e}) ⋖[M] M.cl (insert e M.E \ {e})) ∧ e ∈ B ∧ M.cl (insert e M.E \ {e}) ∈ U
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax :
  M.cl (I \ {e}) = M.cl ((I ∪ B) \ {e}) ∧ ((e ∈ I ↔ M.cl ((I ∪ B) \ {e}) ∈ U) → e ∉ I ∪ B) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl ((I ∪ B) \ {e})) ∧ e ∈ I ∧ M.cl ((I ∪ B) \ {e}) ∈ U
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
⊢ False
Tactic:
obtain (rfl | hU) := U.eq_bot_or_ground_mem
Proof state after:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hI : ⊥.ExtIndep e I
hInmax :
  ¬(M.cl (I \ {e}) = M.cl (insert e M.E \ {e}) ∧ ((e ∈ I ↔ M.cl (insert e M.E \ {e}) ∈ ⊥) → e ∉ insert e M.E) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (insert e M.E \ {e})) ∧ e ∈ I ∧ M.cl (insert e M.E \ {e}) ∈ ⊥)
hBmax :
  M.cl (B \ {e}) = M.cl (insert e M.E \ {e}) ∧ ((e ∈ B ↔ M.cl (insert e M.E \ {e}) ∈ ⊥) → e ∉ insert e M.E) ∨
    (M.cl (B \ {e}) ⋖[M] M.cl (insert e M.E \ {e})) ∧ e ∈ B ∧ M.cl (insert e M.E \ {e}) ∈ ⊥
hcon : ∀ x ∈ B \ I, ¬⊥.ExtIndep e (insert x I)
hB : ⊥.ExtIndep e B
hImax :
  M.cl (I \ {e}) = M.cl ((I ∪ B) \ {e}) ∧ ((e ∈ I ↔ M.cl ((I ∪ B) \ {e}) ∈ ⊥) → e ∉ I ∪ B) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl ((I ∪ B) \ {e})) ∧ e ∈ I ∧ M.cl ((I ∪ B) \ {e}) ∈ ⊥
hrw : {J | ⊥.ExtIndep e J} = {J | ⊥.ExtIndep e J ∧ J ⊆ insert e M.E}
⊢ False

case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax :
  ¬(M.cl (I \ {e}) = M.cl (insert e M.E \ {e}) ∧ ((e ∈ I ↔ M.cl (insert e M.E \ {e}) ∈ U) → e ∉ insert e M.E) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (insert e M.E \ {e})) ∧ e ∈ I ∧ M.cl (insert e M.E \ {e}) ∈ U)
hBmax :
  M.cl (B \ {e}) = M.cl (insert e M.E \ {e}) ∧ ((e ∈ B ↔ M.cl (insert e M.E \ {e}) ∈ U) → e ∉ insert e M.E) ∨
    (M.cl (B \ {e}) ⋖[M] M.cl (insert e M.E \ {e})) ∧ e ∈ B ∧ M.cl (insert e M.E \ {e}) ∈ U
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax :
  M.cl (I \ {e}) = M.cl ((I ∪ B) \ {e}) ∧ ((e ∈ I ↔ M.cl ((I ∪ B) \ {e}) ∈ U) → e ∉ I ∪ B) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl ((I ∪ B) \ {e})) ∧ e ∈ I ∧ M.cl ((I ∪ B) \ {e}) ∈ U
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
⊢ False