Theorem: Matroid.ModularCut.maximal_extIndep_iff (Matroid/Extension.lean)

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ X} ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ I ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
have hss : I \ {e} ⊆ X \ {e} := diff_subset_diff_left hIX
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ X} ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ I ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ X} ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ I ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
have hX' : X \ {e} ⊆ M.E := by simpa
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ X} ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ I ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ X} ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ I ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
rw [mem_maximals_iff_forall_insert (fun _ _ ht hst ↦ ⟨ht.1.subset hst, hst.trans ht.2⟩)]
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
⊢ ((U.ExtIndep e I ∧ I ⊆ X) ∧ ∀ x ∉ I, ¬(U.ExtIndep e (insert x I) ∧ insert x I ⊆ X)) ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ I ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
⊢ ((U.ExtIndep e I ∧ I ⊆ X) ∧ ∀ x ∉ I, ¬(U.ExtIndep e (insert x I) ∧ insert x I ⊆ X)) ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ I ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
simp only [hI, hIX, and_self, insert_subset_iff, and_true, not_and, true_and, imp_not_comm]
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
⊢ (∀ x ∉ I, x ∈ X → ¬U.ExtIndep e (insert x I)) ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
⊢ (∀ x ∉ I, x ∈ X → ¬U.ExtIndep e (insert x I)) ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
refine ⟨fun h ↦ ?_, fun h x hxI hi hind ↦ ?_⟩
State after:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h : ∀ x ∉ I, x ∈ X → ¬U.ExtIndep e (insert x I)
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U

case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
⊢ False

State before:
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
⊢ False
Tactic:
by_cases heI : e ∈ I
State after:
case pos
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∈ I
⊢ False

case neg
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
⊢ False

State before:
case neg
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
⊢ False
Tactic:
simp only [heI, not_false_eq_true, diff_singleton_eq_self, false_iff, not_not, false_and,
  and_false, or_false] at h
State after:
case neg
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
⊢ False

State before:
case neg
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
⊢ False
Tactic:
obtain (rfl | hne) := eq_or_ne e x
State after:
case neg.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hxI : e ∉ I
hi : e ∈ X
hind : U.ExtIndep e (insert e I)
⊢ False

case neg.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ False

State before:
case neg.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ False
Tactic:
rw [extIndep_iff_of_not_mem heI] at hI
State after:
case neg.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ False

State before:
case neg.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ False
Tactic:
rw [extIndep_iff_of_not_mem (by simp [heI, hne]), hI.insert_indep_iff_of_not_mem hxI, h.1] at hind
State after:
case neg.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (X \ {e})
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ False

State before:
case neg.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (X \ {e})
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ False
Tactic:
refine not_mem_of_mem_diff_cl hind ⟨hi, hne.symm⟩
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
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
⊢ X \ {e} ⊆ M.E
Tactic:
simpa
State after:
no goals

State before:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h : ∀ x ∉ I, x ∈ X → ¬U.ExtIndep e (insert x I)
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
simp only [ExtIndep, insert_subset_iff, hIX, and_true, imp_not_comm, not_or, not_and,
  not_not] at h
State after:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U

State before:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
obtain (heI | heI) := em (e ∈ I)
State after:
case refine_1.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U

case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∉ I
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U

State before:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∉ I
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
simp only [mem_insert_iff, heI, or_false] at h
State after:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U

State before:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
have hXI : M.cl (X \ {e}) = M.cl (I \ {e}) := by
  refine (M.cl_subset_cl hss).antisymm' (M.cl_subset_cl_of_subset_cl fun x hx ↦ ?_)
  rw [hI.diff_singleton_indep.mem_cl_iff', and_iff_right (hX' hx), mem_diff, and_iff_left hx.2,
    diff_singleton_eq_self heI]
  exact fun h' ↦ by_contra fun hxI ↦ by simp [(h x hxI hx.1).1 h'] at hx
State after:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
hXI : M.cl (X \ {e}) = M.cl (I \ {e})
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U

State before:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
hXI : M.cl (X \ {e}) = M.cl (I \ {e})
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
simp only [heI, not_false_eq_true, diff_singleton_eq_self, hXI, false_iff, not_imp_not,
  true_and, false_and, and_false, or_false]
State after:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
hXI : M.cl (X \ {e}) = M.cl (I \ {e})
⊢ e ∈ X → ¬M.cl I ∉ U

State before:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
hXI : M.cl (X \ {e}) = M.cl (I \ {e})
⊢ e ∈ X → ¬M.cl I ∉ U
Tactic:
intro heX
State after:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
hXI : M.cl (X \ {e}) = M.cl (I \ {e})
heX : e ∈ X
⊢ ¬M.cl I ∉ U

State before:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
hXI : M.cl (X \ {e}) = M.cl (I \ {e})
heX : e ∈ X
⊢ ¬M.cl I ∉ U
Tactic:
rw [extIndep_iff_of_not_mem heI] at hI
State after:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
hXI : M.cl (X \ {e}) = M.cl (I \ {e})
heX : e ∈ X
⊢ ¬M.cl I ∉ U

State before:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
hXI : M.cl (X \ {e}) = M.cl (I \ {e})
heX : e ∈ X
⊢ ¬M.cl I ∉ U
Tactic:
simpa [heI, hI] using (h e heI heX).2
State after:
no goals

State before:
case refine_1.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
rw [extIndep_iff_of_mem heI] at hI
State after:
case refine_1.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U

State before:
case refine_1.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
obtain (hcl | hcl) := em (M.cl (X \ {e}) ∈ U)
State after:
case refine_1.inl.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U

case refine_1.inl.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∉ U
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U

State before:
case refine_1.inl.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∉ U
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
simp only [heI, hcl, iff_false, not_true_eq_false, not_false_eq_true, implies_true, and_true,
  and_false, or_false]
State after:
case refine_1.inl.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∉ U
⊢ M.cl (I \ {e}) = M.cl (X \ {e})

State before:
case refine_1.inl.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∉ U
⊢ M.cl (I \ {e}) = M.cl (X \ {e})
Tactic:
refine (M.cl_subset_cl hss).antisymm (M.cl_subset_cl_of_subset_cl fun x hx ↦
  by_contra fun hxcl ↦ hcl ?_)
State after:
case refine_1.inl.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
⊢ M.cl (X \ {e}) ∈ U

State before:
case refine_1.inl.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
⊢ M.cl (X \ {e}) ∈ U
Tactic:
have hxI : x ∉ I := by simpa [hx.2] using not_mem_of_mem_diff_cl ⟨(hX' hx), hxcl⟩
State after:
case refine_1.inl.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
hxI : x ∉ I
⊢ M.cl (X \ {e}) ∈ U

State before:
case refine_1.inl.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
hxI : x ∉ I
⊢ M.cl (X \ {e}) ∈ U
Tactic:
replace h := show M.cl (insert x (I \ {e})) ∈ U by
  simpa [hxI, hx.1, heI, ← insert_diff_singleton_comm hx.2, hI.1.insert_indep_iff,
    hX' hx, hxcl] using h x
State after:
case refine_1.inl.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
hxI : x ∉ I
h : M.cl (insert x (I \ {e})) ∈ U
⊢ M.cl (X \ {e}) ∈ U

State before:
case refine_1.inl.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
hxI : x ∉ I
h : M.cl (insert x (I \ {e})) ∈ U
⊢ M.cl (X \ {e}) ∈ U
Tactic:
exact U.cl_superset_mem' h (insert_subset hx hss)
State after:
no goals

State before:
case refine_1.inl.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
simp only [heI, hcl, not_true_eq_false, imp_false, and_self, and_true]
State after:
case refine_1.inl.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ e ∉ X ∨ (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e}))

State before:
case refine_1.inl.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ e ∉ X ∨ (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e}))
Tactic:
refine .inr <| U.covBy_of_maximal_cl (M.cl_subset_cl hss) hcl hI.2 fun x ⟨hx, hxcl⟩ ↦ ?_
State after:
case refine_1.inl.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
⊢ M.cl (insert x (I \ {e})) ∈ U

State before:
case refine_1.inl.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
⊢ M.cl (insert x (I \ {e})) ∈ U
Tactic:
specialize h x
State after:
case refine_1.inl.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
h :
  x ∉ I →
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
⊢ M.cl (insert x (I \ {e})) ∈ U

State before:
case refine_1.inl.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
h :
  x ∉ I →
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
⊢ M.cl (insert x (I \ {e})) ∈ U
Tactic:
have hxI : x ∉ I := by simpa [hx.2] using not_mem_of_mem_diff_cl ⟨hX' hx, hxcl⟩
State after:
case refine_1.inl.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
h :
  x ∉ I →
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
hxI : x ∉ I
⊢ M.cl (insert x (I \ {e})) ∈ U

State before:
case refine_1.inl.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
h :
  x ∉ I →
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
hxI : x ∉ I
⊢ M.cl (insert x (I \ {e})) ∈ U
Tactic:
rw [← insert_diff_singleton_comm hx.2, hI.1.insert_indep_iff] at h
State after:
case refine_1.inl.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
h :
  x ∉ I →
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (x ∈ M.E \ M.cl (I \ {e}) ∨ x ∈ I \ {e} → e ∈ insert x I → M.cl (insert x (I \ {e})) ∈ U)
hxI : x ∉ I
⊢ M.cl (insert x (I \ {e})) ∈ U

State before:
case refine_1.inl.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
h :
  x ∉ I →
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (x ∈ M.E \ M.cl (I \ {e}) ∨ x ∈ I \ {e} → e ∈ insert x I → M.cl (insert x (I \ {e})) ∈ U)
hxI : x ∉ I
⊢ M.cl (insert x (I \ {e})) ∈ U
Tactic:
exact (h hxI hx.1).2 (.inl ⟨hX' hx, hxcl⟩) (.inr heI)
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
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
h :
  x ∉ I →
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
⊢ x ∉ I
Tactic:
simpa [hx.2] using not_mem_of_mem_diff_cl ⟨hX' hx, hxcl⟩
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
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
⊢ x ∉ I
Tactic:
simpa [hx.2] using not_mem_of_mem_diff_cl ⟨(hX' hx), hxcl⟩
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
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
hxI : x ∉ I
⊢ M.cl (insert x (I \ {e})) ∈ U
Tactic:
simpa [hxI, hx.1, heI, ← insert_diff_singleton_comm hx.2, hI.1.insert_indep_iff,
  hX' hx, hxcl] using h x
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
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
⊢ M.cl (X \ {e}) = M.cl (I \ {e})
Tactic:
refine (M.cl_subset_cl hss).antisymm' (M.cl_subset_cl_of_subset_cl fun x hx ↦ ?_)
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
x : α
hx : x ∈ X \ {e}
⊢ x ∈ M.cl (I \ {e})

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
x : α
hx : x ∈ X \ {e}
⊢ x ∈ M.cl (I \ {e})
Tactic:
rw [hI.diff_singleton_indep.mem_cl_iff', and_iff_right (hX' hx), mem_diff, and_iff_left hx.2,
  diff_singleton_eq_self heI]
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
x : α
hx : x ∈ X \ {e}
⊢ M.Indep (insert x I) → x ∈ I

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
x : α
hx : x ∈ X \ {e}
⊢ M.Indep (insert x I) → x ∈ I
Tactic:
exact fun h' ↦ by_contra fun hxI ↦ by simp [(h x hxI hx.1).1 h'] at hx
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
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
x : α
hx : x ∈ X \ {e}
h' : M.Indep (insert x I)
hxI : x ∉ I
⊢ False
Tactic:
simp [(h x hxI hx.1).1 h'] at hx
State after:
no goals

State before:
case pos
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∈ I
⊢ False
Tactic:
have hxe : x ≠ e := by rintro rfl; contradiction
State after:
case pos
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∈ I
hxe : x ≠ e
⊢ False

State before:
case pos
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∈ I
hxe : x ≠ e
⊢ False
Tactic:
rw [extIndep_iff_of_mem heI] at hI
State after:
case pos
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∈ I
hxe : x ≠ e
⊢ False

State before:
case pos
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∈ I
hxe : x ≠ e
⊢ False
Tactic:
rw [extIndep_iff_of_mem (.inr heI), ← insert_diff_singleton_comm hxe,
  hI.1.insert_indep_iff_of_not_mem (by simp [hxI, hxe])] at hind
State after:
case pos
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
⊢ False

State before:
case pos
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
⊢ False
Tactic:
simp only [hIX heI, heI, true_iff, true_implies, true_and] at h
State after:
case pos
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
h : M.cl (I \ {e}) = M.cl (X \ {e}) ∧ M.cl (X \ {e}) ∉ U ∨ (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ M.cl (X \ {e}) ∈ U
⊢ False

State before:
case pos
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
h : M.cl (I \ {e}) = M.cl (X \ {e}) ∧ M.cl (X \ {e}) ∉ U ∨ (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ M.cl (X \ {e}) ∈ U
⊢ False
Tactic:
obtain (⟨h_eq, -⟩ | ⟨hcv, h⟩) := h
State after:
case pos.inl.intro
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
h_eq : M.cl (I \ {e}) = M.cl (X \ {e})
⊢ False

case pos.inr.intro
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
hcv : M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})
h : M.cl (X \ {e}) ∈ U
⊢ False

State before:
case pos.inr.intro
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
hcv : M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})
h : M.cl (X \ {e}) ∈ U
⊢ False
Tactic:
rw [hcv.eq_cl_insert_of_mem_diff ⟨M.mem_cl_of_mem ⟨hi, hxe⟩, hind.1.2⟩,
  cl_insert_cl_eq_cl_insert] at h
State after:
case pos.inr.intro
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
hcv : M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})
h : M.cl (insert x (I \ {e})) ∈ U
⊢ False

State before:
case pos.inr.intro
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
hcv : M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})
h : M.cl (insert x (I \ {e})) ∈ U
⊢ False
Tactic:
exact hind.2 h
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
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∈ I
⊢ x ≠ e
Tactic:
rintro rfl
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
f : α
U : M.ModularCut
hIX : I ⊆ X
x : α
hxI : x ∉ I
hi : x ∈ X
hX : X ⊆ insert x M.E
hI : U.ExtIndep x I
hss : I \ {x} ⊆ X \ {x}
hX' : X \ {x} ⊆ M.E
h :
  M.cl (I \ {x}) = M.cl (X \ {x}) ∧ (x ∈ X → ¬(x ∈ I ↔ M.cl (X \ {x}) ∈ U)) ∨
    (M.cl (I \ {x}) ⋖[M] M.cl (X \ {x})) ∧ x ∈ I ∧ M.cl (X \ {x}) ∈ U
hind : U.ExtIndep x (insert x I)
heI : x ∈ I
⊢ False

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
f : α
U : M.ModularCut
hIX : I ⊆ X
x : α
hxI : x ∉ I
hi : x ∈ X
hX : X ⊆ insert x M.E
hI : U.ExtIndep x I
hss : I \ {x} ⊆ X \ {x}
hX' : X \ {x} ⊆ M.E
h :
  M.cl (I \ {x}) = M.cl (X \ {x}) ∧ (x ∈ X → ¬(x ∈ I ↔ M.cl (X \ {x}) ∈ U)) ∨
    (M.cl (I \ {x}) ⋖[M] M.cl (X \ {x})) ∧ x ∈ I ∧ M.cl (X \ {x}) ∈ U
hind : U.ExtIndep x (insert x I)
heI : x ∈ I
⊢ False
Tactic:
contradiction
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
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : M.Indep (insert x (I \ {e})) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
⊢ x ∉ I \ {e}
Tactic:
simp [hxI, hxe]
State after:
no goals

State before:
case pos.inl.intro
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
h_eq : M.cl (I \ {e}) = M.cl (X \ {e})
⊢ False
Tactic:
exact not_mem_of_mem_diff_cl (h_eq ▸ hind.1) <| by simp [hi, hxe]
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
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
h_eq : M.cl (I \ {e}) = M.cl (X \ {e})
⊢ x ∈ X \ {e}
Tactic:
simp [hi, hxe]
State after:
no goals

State before:
case neg.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hxI : e ∉ I
hi : e ∈ X
hind : U.ExtIndep e (insert e I)
⊢ False
Tactic:
rw [extIndep_iff_of_mem (.inl rfl)] at hind
State after:
case neg.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hxI : e ∉ I
hi : e ∈ X
hind : M.Indep (insert e I \ {e}) ∧ M.cl (insert e I \ {e}) ∉ U
⊢ False

State before:
case neg.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hxI : e ∉ I
hi : e ∈ X
hind : M.Indep (insert e I \ {e}) ∧ M.cl (insert e I \ {e}) ∉ U
⊢ False
Tactic:
simp only [mem_singleton_iff, insert_diff_of_mem, hxI, not_false_eq_true,
  diff_singleton_eq_self, h.1] at hind
State after:
case neg.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hxI : e ∉ I
hi : e ∈ X
hind : M.Indep I ∧ M.cl (X \ {e}) ∉ U
⊢ False

State before:
case neg.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hxI : e ∉ I
hi : e ∈ X
hind : M.Indep I ∧ M.cl (X \ {e}) ∉ U
⊢ False
Tactic:
exact hind.2 <| h.2 hi
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
hX : X ⊆ insert e M.E
hI : M.Indep I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ e ∉ insert x I
Tactic:
simp [heI, hne]
State after:
no goals