Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop (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
he : ¬M.Coloop e
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:
rw [coloop_iff_diff_cl, not_not] at he
State after:
α : 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 : 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)

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 : 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:
by_contra! hcon
State after:
α : 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 : 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}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
⊢ False

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 : 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}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
⊢ False
Tactic:
have hB : U.ExtIndep e B := hBmax.1
State after:
α : 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 : 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}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
⊢ False

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 : 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}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
⊢ False
Tactic:
have hIeE := hI.diff_singleton_indep.subset_ground
State after:
α : 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 : 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}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
⊢ False

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 : 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}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
⊢ False
Tactic:
have hBeE := hB.diff_singleton_indep.subset_ground
State after:
α : 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 : 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}
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
⊢ False

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 : 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}
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
⊢ False
Tactic:
have hss : B \ {e} ⊆ (I ∪ B) \ {e} := diff_subset_diff_left subset_union_right
State after:
α : 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 : 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}
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}
⊢ False

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 : 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}
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}
⊢ False
Tactic:
have hIBe : I ∪ B ⊆ insert e M.E :=
  union_subset hI.subset_insert_ground hB.subset_insert_ground
State after:
α : 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 : 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}
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
⊢ False

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 : 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}
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
⊢ False
Tactic:
have hIBe' : (I ∪ B) \ {e} ⊆ M.E := by rwa [diff_singleton_subset_iff]
State after:
α : 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 : 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}
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
⊢ False

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 : 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}
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 : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
⊢ False
Tactic:
have hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E} := by
  simp only [ext_iff, mem_setOf_eq, iff_self_and]
  exact  fun _ ↦ ExtIndep.subset_insert_ground
State after:
α : 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 : 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}
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 : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
⊢ False

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 : 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}
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 : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
⊢ False
Tactic:
rw [hrw, U.maximal_extIndep_iff Subset.rfl hI hI.subset_insert_ground] at hInmax
State after:
α : 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 : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
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 : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
⊢ False

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 : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
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 : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
⊢ False
Tactic:
rw [hrw, U.maximal_extIndep_iff Subset.rfl hB hB.subset_insert_ground] at hBmax
State after:
α : 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 : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
⊢ False

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 : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
⊢ False
Tactic:
rw [U.maximal_extIndep_iff hIBe hI subset_union_left] at hImax
State after:
α : 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

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
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

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.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
Tactic:
simp only [mem_singleton_iff, insert_diff_of_mem, he, not_false_eq_true, diff_singleton_eq_self,
  cl_ground, hU, iff_true, mem_insert_iff, or_false, not_true_eq_false, and_false, imp_false,
  and_true, not_or, not_and, not_not, mem_union, and_self_left,
  ← spanning_iff_cl hBeE, ← spanning_iff_cl hIeE, ← hyperplane_iff_covBy] at hBmax hInmax
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.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
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
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
⊢ False

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.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
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
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
⊢ False
Tactic:
obtain (hsp | hsp) := em <| M.Spanning ((I ∪ B) \ {e})
State after:
case inr.inl
α : 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
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
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : M.Spanning ((I ∪ B) \ {e})
⊢ False

case inr.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
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
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
⊢ False

State before:
case inr.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
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
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
⊢ False
Tactic:
obtain (⟨hBsp, -⟩ | ⟨hBhp, heB⟩) := hBmax
State after:
case inr.inr.inl.intro
α : 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
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBsp : M.Spanning (B \ {e})
⊢ False

case inr.inr.inr.intro
α : 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
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
⊢ False

State before:
case inr.inr.inr.intro
α : 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
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
⊢ False
Tactic:
have hclcl : M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e}) := by
  refine by_contra fun hne ↦ hsp <| ?_
  rw [← cl_spanning_iff hIBe']
  have hssu := (M.cl_subset_cl hss).ssubset_of_ne hne
  exact hBhp.spanning_of_ssuperset hssu
State after:
case inr.inr.inr.intro
α : 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
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hclcl : M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
⊢ False

State before:
case inr.inr.inr.intro
α : 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
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hclcl : M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
⊢ False
Tactic:
rw [extIndep_iff_of_mem heB] at hB
State after:
case inr.inr.inr.intro
α : 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
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : M.Indep (B \ {e}) ∧ M.cl (B \ {e}) ∉ U
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hclcl : M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
⊢ False

State before:
case inr.inr.inr.intro
α : 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
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : M.Indep (B \ {e}) ∧ M.cl (B \ {e}) ∉ U
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hclcl : M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
⊢ False
Tactic:
replace hImax := show M.cl (I \ {e}) = M.cl (B \ {e}) ∧ e ∈ I by
  simpa [heB, ← hclcl, hB.2] using hImax
State after:
case inr.inr.inr.intro
α : 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
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : M.Indep (B \ {e}) ∧ M.cl (B \ {e}) ∉ U
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
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hclcl : M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
hImax : M.cl (I \ {e}) = M.cl (B \ {e}) ∧ e ∈ I
⊢ False

State before:
case inr.inr.inr.intro
α : 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
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : M.Indep (B \ {e}) ∧ M.cl (B \ {e}) ∉ U
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
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hclcl : M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
hImax : M.cl (I \ {e}) = M.cl (B \ {e}) ∧ e ∈ I
⊢ False
Tactic:
replace hInmax := show ¬M.Hyperplane (M.cl (I \ {e})) by simpa [hImax.2] using hInmax
State after:
case inr.inr.inr.intro
α : 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
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : M.Indep (B \ {e}) ∧ M.cl (B \ {e}) ∉ U
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
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hclcl : M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
hImax : M.cl (I \ {e}) = M.cl (B \ {e}) ∧ e ∈ I
hInmax : ¬M.Hyperplane (M.cl (I \ {e}))
⊢ False

State before:
case inr.inr.inr.intro
α : 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
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : M.Indep (B \ {e}) ∧ M.cl (B \ {e}) ∉ U
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
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hclcl : M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
hImax : M.cl (I \ {e}) = M.cl (B \ {e}) ∧ e ∈ I
hInmax : ¬M.Hyperplane (M.cl (I \ {e}))
⊢ False
Tactic:
exact hInmax <| (hImax.1.symm ▸ hBhp)
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
he : M.cl (M.E \ {e}) = M.E
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}
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
⊢ (I ∪ B) \ {e} ⊆ M.E
Tactic:
rwa [diff_singleton_subset_iff]
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
he : M.cl (M.E \ {e}) = M.E
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}
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
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
Tactic:
rw [mem_maximals_iff_forall_insert (fun _ _ ht hst ↦ ⟨ht.1.subset hst, hst.trans ht.2⟩),
  and_iff_right hI, and_iff_right subset_union_left]
State after:
α : 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 : 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}
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
⊢ ∀ x ∉ I, ¬(U.ExtIndep e (insert x I) ∧ insert x I ⊆ I ∪ B)

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 : 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}
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
⊢ ∀ x ∉ I, ¬(U.ExtIndep e (insert x I) ∧ insert x I ⊆ I ∪ B)
Tactic:
intro x hxI h'
State after:
α : 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 : 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}
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
x : α
hxI : x ∉ I
h' : U.ExtIndep e (insert x I) ∧ insert x I ⊆ I ∪ B
⊢ False

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 : 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}
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
x : α
hxI : x ∉ I
h' : U.ExtIndep e (insert x I) ∧ insert x I ⊆ I ∪ B
⊢ False
Tactic:
rw [insert_subset_iff, mem_union, or_iff_right hxI] at h'
State after:
α : 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 : 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}
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
x : α
hxI : x ∉ I
h' : U.ExtIndep e (insert x I) ∧ x ∈ B ∧ I ⊆ I ∪ B
⊢ False

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 : 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}
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
x : α
hxI : x ∉ I
h' : U.ExtIndep e (insert x I) ∧ x ∈ B ∧ I ⊆ I ∪ B
⊢ False
Tactic:
exact hcon x ⟨h'.2.1, hxI⟩ h'.1
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
he : M.cl (M.E \ {e}) = M.E
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}
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 : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
⊢ {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
Tactic:
simp only [ext_iff, mem_setOf_eq, iff_self_and]
State after:
α : 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 : 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}
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 : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
⊢ ∀ (x : Set α), U.ExtIndep e x → x ⊆ insert e M.E

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 : 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}
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 : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
⊢ ∀ (x : Set α), U.ExtIndep e x → x ⊆ insert e M.E
Tactic:
exact  fun _ ↦ ExtIndep.subset_insert_ground
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
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
Tactic:
replace hBmax := show M.Spanning (B \ {e}) ∧ e ∈ B by
  simpa [← spanning_iff_cl hBeE, he] using hBmax
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}) ∈ ⊥)
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}
hBmax : M.Spanning (B \ {e}) ∧ e ∈ B
⊢ False

State before:
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}) ∈ ⊥)
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}
hBmax : M.Spanning (B \ {e}) ∧ e ∈ B
⊢ False
Tactic:
replace hInmax := show M.Spanning (I \ {e}) → e ∉ I by
  simpa [← spanning_iff_cl hIeE, he] using hInmax
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
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}
hBmax : M.Spanning (B \ {e}) ∧ e ∈ B
hInmax : M.Spanning (I \ {e}) → e ∉ I
⊢ False

State before:
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
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}
hBmax : M.Spanning (B \ {e}) ∧ e ∈ B
hInmax : M.Spanning (I \ {e}) → e ∉ I
⊢ False
Tactic:
replace hImax := show M.Spanning (I \ {e}) ∧ e ∈ I by
  simpa [hBmax.2, he, hBmax.1.cl_superset_eq hss, ← spanning_iff_cl hIeE] using hImax
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
hcon : ∀ x ∈ B \ I, ¬⊥.ExtIndep e (insert x I)
hB : ⊥.ExtIndep e B
hrw : {J | ⊥.ExtIndep e J} = {J | ⊥.ExtIndep e J ∧ J ⊆ insert e M.E}
hBmax : M.Spanning (B \ {e}) ∧ e ∈ B
hInmax : M.Spanning (I \ {e}) → e ∉ I
hImax : M.Spanning (I \ {e}) ∧ e ∈ I
⊢ False

State before:
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
hcon : ∀ x ∈ B \ I, ¬⊥.ExtIndep e (insert x I)
hB : ⊥.ExtIndep e B
hrw : {J | ⊥.ExtIndep e J} = {J | ⊥.ExtIndep e J ∧ J ⊆ insert e M.E}
hBmax : M.Spanning (B \ {e}) ∧ e ∈ B
hInmax : M.Spanning (I \ {e}) → e ∉ I
hImax : M.Spanning (I \ {e}) ∧ e ∈ I
⊢ False
Tactic:
exact hInmax hImax.1 hImax.2
State after:
no goals

State before:
α : 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}
⊢ M.Spanning (B \ {e}) ∧ e ∈ B
Tactic:
simpa [← spanning_iff_cl hBeE, he] using hBmax
State after:
no goals

State before:
α : 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}) ∈ ⊥)
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}
hBmax : M.Spanning (B \ {e}) ∧ e ∈ B
⊢ M.Spanning (I \ {e}) → e ∉ I
Tactic:
simpa [← spanning_iff_cl hIeE, he] using hInmax
State after:
no goals

State before:
α : 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
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}
hBmax : M.Spanning (B \ {e}) ∧ e ∈ B
hInmax : M.Spanning (I \ {e}) → e ∉ I
⊢ M.Spanning (I \ {e}) ∧ e ∈ I
Tactic:
simpa [hBmax.2, he, hBmax.1.cl_superset_eq hss, ← spanning_iff_cl hIeE] using hImax
State after:
no goals

State before:
case inr.inl
α : 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
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
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : M.Spanning ((I ∪ B) \ {e})
⊢ False
Tactic:
obtain (heI | heI) := em (e ∈ I)
State after:
case inr.inl.inl
α : 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
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
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : M.Spanning ((I ∪ B) \ {e})
heI : e ∈ I
⊢ False

case inr.inl.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
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
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : M.Spanning ((I ∪ B) \ {e})
heI : e ∉ I
⊢ False

State before:
case inr.inl.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
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
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : M.Spanning ((I ∪ B) \ {e})
heI : e ∉ I
⊢ False
Tactic:
replace hInmax := show ¬ M.Spanning (I \ {e}) by simpa [heI, hU] using hInmax
State after:
case inr.inl.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
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
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hsp : M.Spanning ((I ∪ B) \ {e})
heI : e ∉ I
hInmax : ¬M.Spanning (I \ {e})
⊢ False

State before:
case inr.inl.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
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
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hsp : M.Spanning ((I ∪ B) \ {e})
heI : e ∉ I
hInmax : ¬M.Spanning (I \ {e})
⊢ False
Tactic:
replace hImax := show M.cl (I \ {e}) = M.E by simpa [hsp.cl_eq, heI, he, hU] using hImax
State after:
case inr.inl.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
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
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hsp : M.Spanning ((I ∪ B) \ {e})
heI : e ∉ I
hInmax : ¬M.Spanning (I \ {e})
hImax : M.cl (I \ {e}) = M.E
⊢ False

State before:
case inr.inl.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
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
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hsp : M.Spanning ((I ∪ B) \ {e})
heI : e ∉ I
hInmax : ¬M.Spanning (I \ {e})
hImax : M.cl (I \ {e}) = M.E
⊢ False
Tactic:
rw [spanning_iff_cl hIeE] at hInmax
State after:
case inr.inl.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
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
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hsp : M.Spanning ((I ∪ B) \ {e})
heI : e ∉ I
hInmax : ¬M.cl (I \ {e}) = M.E
hImax : M.cl (I \ {e}) = M.E
⊢ False

State before:
case inr.inl.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
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
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hsp : M.Spanning ((I ∪ B) \ {e})
heI : e ∉ I
hInmax : ¬M.cl (I \ {e}) = M.E
hImax : M.cl (I \ {e}) = M.E
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case inr.inl.inl
α : 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
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
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : M.Spanning ((I ∪ B) \ {e})
heI : e ∈ I
⊢ False
Tactic:
replace hImax := show M.Hyperplane (M.cl (I \ {e})) by
  simpa [hsp.cl_eq, heI, hU, ← hyperplane_iff_covBy] using hImax
State after:
case inr.inl.inl
α : 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
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
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : M.Spanning ((I ∪ B) \ {e})
heI : e ∈ I
hImax : M.Hyperplane (M.cl (I \ {e}))
⊢ False

State before:
case inr.inl.inl
α : 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
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
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : M.Spanning ((I ∪ B) \ {e})
heI : e ∈ I
hImax : M.Hyperplane (M.cl (I \ {e}))
⊢ False
Tactic:
exact hInmax.2 hImax heI
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
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
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
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : M.Spanning ((I ∪ B) \ {e})
heI : e ∈ I
⊢ M.Hyperplane (M.cl (I \ {e}))
Tactic:
simpa [hsp.cl_eq, heI, hU, ← hyperplane_iff_covBy] using hImax
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
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
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
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : M.Spanning ((I ∪ B) \ {e})
heI : e ∉ I
⊢ ¬M.Spanning (I \ {e})
Tactic:
simpa [heI, hU] using hInmax
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
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
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
hBmax : M.Spanning (B \ {e}) ∧ (e ∈ B → False ∧ e ∉ M.E) ∨ M.Hyperplane (M.cl (B \ {e})) ∧ e ∈ B
hsp : M.Spanning ((I ∪ B) \ {e})
heI : e ∉ I
hInmax : ¬M.Spanning (I \ {e})
⊢ M.cl (I \ {e}) = M.E
Tactic:
simpa [hsp.cl_eq, heI, he, hU] using hImax
State after:
no goals

State before:
case inr.inr.inl.intro
α : 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
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBsp : M.Spanning (B \ {e})
⊢ False
Tactic:
exact hsp <| hBsp.superset hss hIBe'
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
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
⊢ M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
Tactic:
refine by_contra fun hne ↦ hsp <| ?_
State after:
α : 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
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hne : ¬M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
⊢ M.Spanning ((I ∪ B) \ {e})

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
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hne : ¬M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
⊢ M.Spanning ((I ∪ B) \ {e})
Tactic:
rw [← cl_spanning_iff hIBe']
State after:
α : 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
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hne : ¬M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
⊢ M.Spanning (M.cl ((I ∪ B) \ {e}))

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
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hne : ¬M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
⊢ M.Spanning (M.cl ((I ∪ B) \ {e}))
Tactic:
have hssu := (M.cl_subset_cl hss).ssubset_of_ne hne
State after:
α : 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
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hne : ¬M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
hssu : M.cl (B \ {e}) ⊂ M.cl ((I ∪ B) \ {e})
⊢ M.Spanning (M.cl ((I ∪ B) \ {e}))

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
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hne : ¬M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
hssu : M.cl (B \ {e}) ⊂ M.cl ((I ∪ B) \ {e})
⊢ M.Spanning (M.cl ((I ∪ B) \ {e}))
Tactic:
exact hBhp.spanning_of_ssuperset hssu
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
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : M.Indep (B \ {e}) ∧ M.cl (B \ {e}) ∉ U
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
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hclcl : M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
⊢ M.cl (I \ {e}) = M.cl (B \ {e}) ∧ e ∈ I
Tactic:
simpa [heB, ← hclcl, hB.2] using hImax
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
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : M.Indep (B \ {e}) ∧ M.cl (B \ {e}) ∉ U
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
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hclcl : M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
hImax : M.cl (I \ {e}) = M.cl (B \ {e}) ∧ e ∈ I
⊢ ¬M.Hyperplane (M.cl (I \ {e}))
Tactic:
simpa [hImax.2] using hInmax
State after:
no goals