Theorem: Matroid.ModularCut.existsMaximalSubsetProperty (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
hXE : X ⊆ insert e M.E
⊢ ExistsMaximalSubsetProperty (U.ExtIndep e) X
Tactic:
intro I hI hIX
State after:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
⊢ (maximals (fun x x_1 => x ⊆ x_1) {Y | U.ExtIndep e Y ∧ I ⊆ Y ∧ Y ⊆ X}).Nonempty

State before:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
⊢ ∃ J, I ⊆ J ∧ J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
Tactic:
obtain ⟨J, hJ, hIJ⟩ :=
  hI.diff_singleton_indep.subset_basis_of_subset (diff_subset_diff_left hIX)
State after:
case intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
⊢ ∃ J, I ⊆ J ∧ J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}

State before:
case intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
⊢ ∃ J, I ⊆ J ∧ J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
Tactic:
obtain ⟨hJX, heJ⟩ : J ⊆ X ∧ e ∉ J := by simpa [subset_diff] using hJ.subset
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
⊢ ∃ J, I ⊆ J ∧ J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
⊢ ∃ J, I ⊆ J ∧ J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
Tactic:
have hJi : U.ExtIndep e J := .inl ⟨hJ.indep, heJ⟩
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
⊢ ∃ J, I ⊆ J ∧ J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
⊢ ∃ J, I ⊆ J ∧ J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
Tactic:
by_contra! hcon
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ False

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ False
Tactic:
have hconJe : e ∈ X → M.cl (X \ {e}) ∈ U := by
  refine fun heX ↦ by_contra fun hcl ↦ ?_
  have hind : U.ExtIndep e (insert e J) := by
    rw [extIndep_iff_of_mem (.inl rfl)]
    simpa [heJ, hJ.indep, hJ.cl_eq_cl]
  specialize hcon (insert e J) (by simpa using hIJ)
  rw [maximal_extIndep_iff  hXE hind (insert_subset heX hJX)] at hcon
  simp [heJ, hJ.cl_eq_cl, hcl] at hcon
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
⊢ False

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
⊢ False
Tactic:
have heI : e ∈ I := by
  refine by_contra fun heI ↦ ?_
  rw [diff_singleton_eq_self heI] at hIJ
  have h' : M.cl (X \ {e}) ∉ U ∧ e ∈ X := by
    simpa [maximal_extIndep_iff hXE hJi hJX, heJ, hJ.cl_eq_cl] using hcon J hIJ
  exact h'.1 <| hconJe h'.2
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
heI : e ∈ I
⊢ False

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
heI : e ∈ I
⊢ False
Tactic:
rw [extIndep_iff_of_mem heI] at hI
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
heI : e ∈ I
⊢ False

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
heI : e ∈ I
⊢ False
Tactic:
specialize hconJe (hIX heI)
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
⊢ False

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
⊢ False
Tactic:
obtain (rfl | hssu) := hIJ.eq_or_ssubset
State after:
case intro.intro.intro.inl
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hJ : M.Basis (I \ {e}) (X \ {e})
hIJ : I \ {e} ⊆ I \ {e}
hJX : I \ {e} ⊆ X
heJ : e ∉ I \ {e}
hJi : U.ExtIndep e (I \ {e})
⊢ False

case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
⊢ False

State before:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
⊢ False
Tactic:
refine hI.2 <| U.mem_of_ssubset_indep_of_forall_diff hJ.indep hssu (fun x hx ↦ ?_)
State after:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
⊢ M.cl (J \ {x}) ∈ U

State before:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
⊢ M.cl (J \ {x}) ∈ U
Tactic:
by_contra! hJu
State after:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
⊢ False

State before:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
⊢ False
Tactic:
have hxe : x ≠ e := by rintro rfl; simp [heJ] at hx
State after:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
⊢ False

State before:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
⊢ False
Tactic:
have hxJI : x ∈ J \ I := by simpa [hxe] using hx
State after:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
⊢ False

State before:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
⊢ False
Tactic:
set J' := insert e (J \ {x}) with hJ'
State after:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
⊢ False

State before:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
⊢ False
Tactic:
have hIeJx : I ⊆ J' := by
  simpa [hJ', insert_diff_singleton_comm hxe.symm, subset_diff, hxJI.2] using hIJ
State after:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
⊢ False

State before:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
⊢ False
Tactic:
have hJ'e : J' \ {e} = J \ {x} := by simp [hJ', insert_diff_self_of_not_mem, heJ]
State after:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
⊢ False

State before:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
⊢ False
Tactic:
specialize hcon J' hIeJx
State after:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon : J' ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ False

State before:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon : J' ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ False
Tactic:
have hind : U.ExtIndep e J' := by
  simp only [extIndep_iff_of_mem (show e ∈ J' from .inl rfl), hJ'e]
  exact ⟨hJ.indep.diff _, hJu⟩
State after:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon : J' ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hind : U.ExtIndep e J'
⊢ False

State before:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon : J' ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hind : U.ExtIndep e J'
⊢ False
Tactic:
have hJ'X : J' ⊆ X := insert_subset (hIX heI) (diff_subset.trans hJX)
State after:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon : J' ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hind : U.ExtIndep e J'
hJ'X : J' ⊆ X
⊢ False

State before:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon : J' ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hind : U.ExtIndep e J'
hJ'X : J' ⊆ X
⊢ False
Tactic:
have hconJ' : (M.cl (J \ {x}) = M.cl J → e ∈ X) ∧ ¬M.CovBy (M.cl (J \ {x})) (M.cl J) := by
  rw [maximal_extIndep_iff hXE hind hJ'X, iff_true_intro hconJe] at hcon
  simpa [hJ'e, ← hJ.cl_eq_cl, show e ∈ J' from .inl rfl] using hcon
State after:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon : J' ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hind : U.ExtIndep e J'
hJ'X : J' ⊆ X
hconJ' : (M.cl (J \ {x}) = M.cl J → e ∈ X) ∧ ¬(M.cl (J \ {x}) ⋖[M] M.cl J)
⊢ False

State before:
case intro.intro.intro.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon : J' ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hind : U.ExtIndep e J'
hJ'X : J' ⊆ X
hconJ' : (M.cl (J \ {x}) = M.cl J → e ∈ X) ∧ ¬(M.cl (J \ {x}) ⋖[M] M.cl J)
⊢ False
Tactic:
exact hconJ'.2 <| hJ.indep.cl_diff_covBy hxJI.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
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
hJ : ∃ J, I ⊆ J ∧ J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ (maximals (fun x x_1 => x ⊆ x_1) {Y | U.ExtIndep e Y ∧ I ⊆ Y ∧ Y ⊆ X}).Nonempty
Tactic:
obtain ⟨J, hIJ, hJ⟩ := hJ
State after:
case intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hIJ : I ⊆ J
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ (maximals (fun x x_1 => x ⊆ x_1) {Y | U.ExtIndep e Y ∧ I ⊆ Y ∧ Y ⊆ X}).Nonempty

State before:
case intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hIJ : I ⊆ J
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ (maximals (fun x x_1 => x ⊆ x_1) {Y | U.ExtIndep e Y ∧ I ⊆ Y ∧ Y ⊆ X}).Nonempty
Tactic:
refine ⟨J, ?_⟩
State after:
case intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hIJ : I ⊆ J
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | U.ExtIndep e Y ∧ I ⊆ Y ∧ Y ⊆ X}

State before:
case intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hIJ : I ⊆ J
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | U.ExtIndep e Y ∧ I ⊆ Y ∧ Y ⊆ X}
Tactic:
convert maximals_inter_subset (t := {K | I ⊆ K}) ⟨hJ, hIJ⟩ using 2
State after:
case h.e'_5.h.e'_3
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hIJ : I ⊆ J
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ {Y | U.ExtIndep e Y ∧ I ⊆ Y ∧ Y ⊆ X} = {K | U.ExtIndep e K ∧ K ⊆ X} ∩ {K | I ⊆ K}

State before:
case h.e'_5.h.e'_3
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hIJ : I ⊆ J
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ {Y | U.ExtIndep e Y ∧ I ⊆ Y ∧ Y ⊆ X} = {K | U.ExtIndep e K ∧ K ⊆ X} ∩ {K | I ⊆ K}
Tactic:
ext
State after:
case h.e'_5.h.e'_3.h
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hIJ : I ⊆ J
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
x✝ : Set α
⊢ x✝ ∈ {Y | U.ExtIndep e Y ∧ I ⊆ Y ∧ Y ⊆ X} ↔ x✝ ∈ {K | U.ExtIndep e K ∧ K ⊆ X} ∩ {K | I ⊆ K}

State before:
case h.e'_5.h.e'_3.h
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hIJ : I ⊆ J
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
x✝ : Set α
⊢ x✝ ∈ {Y | U.ExtIndep e Y ∧ I ⊆ Y ∧ Y ⊆ X} ↔ x✝ ∈ {K | U.ExtIndep e K ∧ K ⊆ X} ∩ {K | I ⊆ K}
Tactic:
simp only [mem_setOf_eq, mem_inter_iff]
State after:
case h.e'_5.h.e'_3.h
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hIJ : I ⊆ J
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
x✝ : Set α
⊢ U.ExtIndep e x✝ ∧ I ⊆ x✝ ∧ x✝ ⊆ X ↔ (U.ExtIndep e x✝ ∧ x✝ ⊆ X) ∧ I ⊆ x✝

State before:
case h.e'_5.h.e'_3.h
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hIJ : I ⊆ J
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
x✝ : Set α
⊢ U.ExtIndep e x✝ ∧ I ⊆ x✝ ∧ x✝ ⊆ X ↔ (U.ExtIndep e x✝ ∧ x✝ ⊆ X) ∧ I ⊆ x✝
Tactic:
tauto
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
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
⊢ J ⊆ X ∧ e ∉ J
Tactic:
simpa [subset_diff] using hJ.subset
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
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ e ∈ X → M.cl (X \ {e}) ∈ U
Tactic:
refine fun heX ↦ by_contra fun hcl ↦ ?_
State after:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
⊢ False

State before:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
⊢ False
Tactic:
have hind : U.ExtIndep e (insert e J) := by
  rw [extIndep_iff_of_mem (.inl rfl)]
  simpa [heJ, hJ.indep, hJ.cl_eq_cl]
State after:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
hind : U.ExtIndep e (insert e J)
⊢ False

State before:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
hind : U.ExtIndep e (insert e J)
⊢ False
Tactic:
specialize hcon (insert e J) (by simpa using hIJ)
State after:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
hind : U.ExtIndep e (insert e J)
hcon : insert e J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ False

State before:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
hind : U.ExtIndep e (insert e J)
hcon : insert e J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ False
Tactic:
rw [maximal_extIndep_iff  hXE hind (insert_subset heX hJX)] at hcon
State after:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
hind : U.ExtIndep e (insert e J)
hcon :
  ¬(M.cl (insert e J \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ insert e J ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (insert e J \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ insert e J ∧ M.cl (X \ {e}) ∈ U)
⊢ False

State before:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
hind : U.ExtIndep e (insert e J)
hcon :
  ¬(M.cl (insert e J \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ insert e J ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (insert e J \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ insert e J ∧ M.cl (X \ {e}) ∈ U)
⊢ False
Tactic:
simp [heJ, hJ.cl_eq_cl, hcl] at hcon
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
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
⊢ U.ExtIndep e (insert e J)
Tactic:
rw [extIndep_iff_of_mem (.inl rfl)]
State after:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
⊢ M.Indep (insert e J \ {e}) ∧ M.cl (insert e J \ {e}) ∉ U

State before:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
⊢ M.Indep (insert e J \ {e}) ∧ M.cl (insert e J \ {e}) ∉ U
Tactic:
simpa [heJ, hJ.indep, hJ.cl_eq_cl]
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
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
hind : U.ExtIndep e (insert e J)
⊢ I ⊆ insert e J
Tactic:
simpa using hIJ
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
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
⊢ e ∈ I
Tactic:
refine by_contra fun heI ↦ ?_
State after:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
heI : e ∉ I
⊢ False

State before:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
heI : e ∉ I
⊢ False
Tactic:
rw [diff_singleton_eq_self heI] at hIJ
State after:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
heI : e ∉ I
⊢ False

State before:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
heI : e ∉ I
⊢ False
Tactic:
have h' : M.cl (X \ {e}) ∉ U ∧ e ∈ X := by
  simpa [maximal_extIndep_iff hXE hJi hJX, heJ, hJ.cl_eq_cl] using hcon J hIJ
State after:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
heI : e ∉ I
h' : M.cl (X \ {e}) ∉ U ∧ e ∈ X
⊢ False

State before:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
heI : e ∉ I
h' : M.cl (X \ {e}) ∉ U ∧ e ∈ X
⊢ False
Tactic:
exact h'.1 <| hconJe h'.2
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
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
heI : e ∉ I
⊢ M.cl (X \ {e}) ∉ U ∧ e ∈ X
Tactic:
simpa [maximal_extIndep_iff hXE hJi hJX, heJ, hJ.cl_eq_cl] using hcon J hIJ
State after:
no goals

State before:
case intro.intro.intro.inl
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hJ : M.Basis (I \ {e}) (X \ {e})
hIJ : I \ {e} ⊆ I \ {e}
hJX : I \ {e} ⊆ X
heJ : e ∉ I \ {e}
hJi : U.ExtIndep e (I \ {e})
⊢ False
Tactic:
rw [hJ.cl_eq_cl] at hI
State after:
case intro.intro.intro.inl
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (X \ {e}) ∉ U
hIX : I ⊆ X
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hJ : M.Basis (I \ {e}) (X \ {e})
hIJ : I \ {e} ⊆ I \ {e}
hJX : I \ {e} ⊆ X
heJ : e ∉ I \ {e}
hJi : U.ExtIndep e (I \ {e})
⊢ False

State before:
case intro.intro.intro.inl
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (X \ {e}) ∉ U
hIX : I ⊆ X
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hJ : M.Basis (I \ {e}) (X \ {e})
hIJ : I \ {e} ⊆ I \ {e}
hJX : I \ {e} ⊆ X
heJ : e ∉ I \ {e}
hJi : U.ExtIndep e (I \ {e})
⊢ False
Tactic:
exact hI.2 hconJe
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
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
⊢ x ≠ e
Tactic:
rintro rfl
State after:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
f : α
U✝ U : M.ModularCut
I : Set α
hIX : I ⊆ X
J : Set α
hJX : J ⊆ X
x : α
hJu : M.cl (J \ {x}) ∉ U
hXE : X ⊆ insert x M.E
hI : M.Indep (I \ {x}) ∧ M.cl (I \ {x}) ∉ U
hJ : M.Basis J (X \ {x})
hIJ : I \ {x} ⊆ J
heJ : x ∉ J
hJi : U.ExtIndep x J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep x K ∧ K ⊆ X}
heI : x ∈ I
hconJe : M.cl (X \ {x}) ∈ U
hssu : I \ {x} ⊂ J
hx : x ∈ J \ (I \ {x})
⊢ False

State before:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
f : α
U✝ U : M.ModularCut
I : Set α
hIX : I ⊆ X
J : Set α
hJX : J ⊆ X
x : α
hJu : M.cl (J \ {x}) ∉ U
hXE : X ⊆ insert x M.E
hI : M.Indep (I \ {x}) ∧ M.cl (I \ {x}) ∉ U
hJ : M.Basis J (X \ {x})
hIJ : I \ {x} ⊆ J
heJ : x ∉ J
hJi : U.ExtIndep x J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep x K ∧ K ⊆ X}
heI : x ∈ I
hconJe : M.cl (X \ {x}) ∈ U
hssu : I \ {x} ⊂ J
hx : x ∈ J \ (I \ {x})
⊢ False
Tactic:
simp [heJ] 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✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
⊢ x ∈ J \ I
Tactic:
simpa [hxe] using hx
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
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
⊢ I ⊆ J'
Tactic:
simpa [hJ', insert_diff_singleton_comm hxe.symm, subset_diff, hxJI.2] using hIJ
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
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
hcon : ∀ (J : Set α), I ⊆ J → J ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
⊢ J' \ {e} = J \ {x}
Tactic:
simp [hJ', insert_diff_self_of_not_mem, heJ]
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
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon : J' ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ U.ExtIndep e J'
Tactic:
simp only [extIndep_iff_of_mem (show e ∈ J' from .inl rfl), hJ'e]
State after:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon : J' ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ M.Indep (J \ {x}) ∧ M.cl (J \ {x}) ∉ U

State before:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon : J' ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
⊢ M.Indep (J \ {x}) ∧ M.cl (J \ {x}) ∉ U
Tactic:
exact ⟨hJ.indep.diff _, hJu⟩
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
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon : J' ∉ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
hind : U.ExtIndep e J'
hJ'X : J' ⊆ X
⊢ (M.cl (J \ {x}) = M.cl J → e ∈ X) ∧ ¬(M.cl (J \ {x}) ⋖[M] M.cl J)
Tactic:
rw [maximal_extIndep_iff hXE hind hJ'X, iff_true_intro hconJe] at hcon
State after:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon :
  ¬(M.cl (J' \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ J' ↔ True) → e ∉ X) ∨
      (M.cl (J' \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ J' ∧ True)
hind : U.ExtIndep e J'
hJ'X : J' ⊆ X
⊢ (M.cl (J \ {x}) = M.cl J → e ∈ X) ∧ ¬(M.cl (J \ {x}) ⋖[M] M.cl J)

State before:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
J : Set α
hJ : M.Basis J (X \ {e})
hIJ : I \ {e} ⊆ J
hJX : J ⊆ X
heJ : e ∉ J
hJi : U.ExtIndep e J
heI : e ∈ I
hconJe : M.cl (X \ {e}) ∈ U
hssu : I \ {e} ⊂ J
x : α
hx : x ∈ J \ (I \ {e})
hJu : M.cl (J \ {x}) ∉ U
hxe : x ≠ e
hxJI : x ∈ J \ I
J' : Set α := insert e (J \ {x})
hJ' : J' = insert e (J \ {x})
hIeJx : I ⊆ J'
hJ'e : J' \ {e} = J \ {x}
hcon :
  ¬(M.cl (J' \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ J' ↔ True) → e ∉ X) ∨
      (M.cl (J' \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ J' ∧ True)
hind : U.ExtIndep e J'
hJ'X : J' ⊆ X
⊢ (M.cl (J \ {x}) = M.cl J → e ∈ X) ∧ ¬(M.cl (J \ {x}) ⋖[M] M.cl J)
Tactic:
simpa [hJ'e, ← hJ.cl_eq_cl, show e ∈ J' from .inl rfl] using hcon
State after:
no goals