Theorem: Matroid.ModularCut.covBy_of_maximal_cl (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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
⊢ M.cl X ⋖[M] M.cl Y
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
State after:
case intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
⊢ M.cl X ⋖[M] M.cl Y

State before:
case intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
⊢ M.cl X ⋖[M] M.cl Y
Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_basis'_of_subset (hI.subset.trans subset_union_left)
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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.59226)
hIJ : I ⊆ J
⊢ M.cl X ⋖[M] M.cl Y

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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.59226)
hIJ : I ⊆ J
⊢ M.cl X ⋖[M] M.cl Y
Tactic:
have hJ' := hJ.basis_cl_right
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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.59226)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl (X ∪ ?m.59226))
⊢ M.cl X ⋖[M] M.cl Y

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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.59226)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl (X ∪ ?m.59226))
⊢ M.cl X ⋖[M] M.cl Y
Tactic:
rw [← cl_cl_union_cl_eq_cl_union, union_eq_self_of_subset_left hXY, cl_cl] at hJ'
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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
⊢ M.cl X ⋖[M] M.cl Y

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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
⊢ M.cl X ⋖[M] M.cl Y
Tactic:
rw [← hI.cl_eq_cl, ← M.cl_cl Y, ← hJ'.cl_eq_cl]
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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
⊢ M.cl I ⋖[M] M.cl J

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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
⊢ M.cl I ⋖[M] M.cl J
Tactic:
rw [← M.cl_cl Y, ← hJ'.cl_eq_cl] at hYU
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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
⊢ M.cl I ⋖[M] M.cl J

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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
⊢ M.cl I ⋖[M] M.cl J
Tactic:
rw [← hI.cl_eq_cl] at hXU
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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
⊢ M.cl I ⋖[M] M.cl J

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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
⊢ M.cl I ⋖[M] M.cl J
Tactic:
obtain (h | hnt) := (J \ I).subsingleton_or_nontrivial
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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
⊢ M.cl I ⋖[M] M.cl J

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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
⊢ M.cl I ⋖[M] M.cl J

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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
⊢ M.cl I ⋖[M] M.cl J
Tactic:
obtain (rfl | hssu) := hIJ.eq_or_ssubset
State after:
case intro.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
hYU : M.cl I ∈ U
hJ : M.Basis' I (X ∪ Y)
hIJ : I ⊆ I
hJ' : M.Basis I (M.cl Y)
hnt : (I \ I).Nontrivial
⊢ M.cl I ⋖[M] M.cl I

case intro.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
⊢ M.cl I ⋖[M] M.cl J

State before:
case intro.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
⊢ M.cl I ⋖[M] M.cl J
Tactic:
refine by_contra fun _ ↦ hXU <| U.mem_of_ssubset_indep_of_forall_diff hJ.indep hssu fun x hx ↦ ?_
State after:
case intro.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
⊢ M.cl (J \ {x}) ∈ U

State before:
case intro.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
⊢ M.cl (J \ {x}) ∈ U
Tactic:
obtain ⟨y, hy, hyx⟩ := hnt.exists_ne x
State after:
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
⊢ M.cl (J \ {x}) ∈ U

State before:
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
⊢ M.cl (J \ {x}) ∈ U
Tactic:
have hyE : y ∈ M.E := hJ.indep.subset_ground hy.1
State after:
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
⊢ M.cl (J \ {x}) ∈ U

State before:
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
⊢ M.cl (J \ {x}) ∈ U
Tactic:
have hyX : y ∉ M.cl X := by
  rw [← hI.cl_eq_cl, hI.indep.not_mem_cl_iff_of_not_mem hy.2 hyE]
  exact hJ.indep.subset (insert_subset hy.1 hIJ)
State after:
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
hyX : y ∉ M.cl X
⊢ M.cl (J \ {x}) ∈ U

State before:
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
hyX : y ∉ M.cl X
⊢ M.cl (J \ {x}) ∈ U
Tactic:
have hyY : y ∈ Y := Or.elim (hJ.subset hy.1) (False.elim ∘ (not_mem_of_mem_diff_cl ⟨hyE, hyX⟩)) id
State after:
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
hyX : y ∉ M.cl X
hyY : y ∈ Y
⊢ M.cl (J \ {x}) ∈ U

State before:
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
hyX : y ∉ M.cl X
hyY : y ∈ Y
⊢ M.cl (J \ {x}) ∈ U
Tactic:
specialize hmax y ⟨hyY, hyX⟩
State after:
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
hyX : y ∉ M.cl X
hyY : y ∈ Y
hmax : M.cl (insert y X) ∈ U
⊢ M.cl (J \ {x}) ∈ U

State before:
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
hyX : y ∉ M.cl X
hyY : y ∈ Y
hmax : M.cl (insert y X) ∈ U
⊢ M.cl (J \ {x}) ∈ U
Tactic:
rw [← cl_insert_cl_eq_cl_insert, ← hI.cl_eq_cl, cl_insert_cl_eq_cl_insert] at hmax
State after:
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
hyX : y ∉ M.cl X
hyY : y ∈ Y
hmax : M.cl (insert y I) ∈ U
⊢ M.cl (J \ {x}) ∈ U

State before:
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
hyX : y ∉ M.cl X
hyY : y ∈ Y
hmax : M.cl (insert y I) ∈ U
⊢ M.cl (J \ {x}) ∈ U
Tactic:
refine U.cl_superset_mem' hmax ?_
State after:
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
hyX : y ∉ M.cl X
hyY : y ∈ Y
hmax : M.cl (insert y I) ∈ U
⊢ insert y I ⊆ J \ {x}

State before:
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
hyX : y ∉ M.cl X
hyY : y ∈ Y
hmax : M.cl (insert y I) ∈ U
⊢ insert y I ⊆ J \ {x}
Tactic:
simp [insert_subset_iff, subset_diff, hIJ, hy.1, hyx.symm, hx.2]
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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
⊢ M.cl I ⋖[M] M.cl J
Tactic:
obtain (he | ⟨e, he⟩) := h.eq_empty_or_singleton
State after:
case intro.intro.intro.inl.inl
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
he : J \ I = ∅
⊢ M.cl I ⋖[M] M.cl J

case intro.intro.intro.inl.inr.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e✝ f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
e : α
he : J \ I = {e}
⊢ M.cl I ⋖[M] M.cl J

State before:
case intro.intro.intro.inl.inr.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e✝ f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
e : α
he : J \ I = {e}
⊢ M.cl I ⋖[M] M.cl J
Tactic:
obtain rfl : J = insert e I := by rw [← union_diff_cancel hIJ, he, union_singleton]
State after:
case intro.intro.intro.inl.inr.intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X✝ Y✝ : Set α
e✝ f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
e : α
hYU : M.cl (insert e I) ∈ U
hJ : M.Basis' (insert e I) (X ∪ Y)
hIJ : I ⊆ insert e I
hJ' : M.Basis (insert e I) (M.cl Y)
h : (insert e I \ I).Subsingleton
he : insert e I \ I = {e}
⊢ M.cl I ⋖[M] M.cl (insert e I)

State before:
case intro.intro.intro.inl.inr.intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X✝ Y✝ : Set α
e✝ f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
e : α
hYU : M.cl (insert e I) ∈ U
hJ : M.Basis' (insert e I) (X ∪ Y)
hIJ : I ⊆ insert e I
hJ' : M.Basis (insert e I) (M.cl Y)
h : (insert e I \ I).Subsingleton
he : insert e I \ I = {e}
⊢ M.cl I ⋖[M] M.cl (insert e I)
Tactic:
simpa [show e ∉ I from (he.symm.subset rfl).2] using hJ.indep.cl_diff_covBy (.inl rfl)
State after:
no goals

State before:
case intro.intro.intro.inl.inl
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
he : J \ I = ∅
⊢ M.cl I ⋖[M] M.cl J
Tactic:
rw [(diff_eq_empty.1 he).antisymm hIJ] at hYU
State after:
case intro.intro.intro.inl.inl
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl I ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
he : J \ I = ∅
⊢ M.cl I ⋖[M] M.cl J

State before:
case intro.intro.intro.inl.inl
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl I ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
he : J \ I = ∅
⊢ M.cl I ⋖[M] M.cl J
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✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
e : α
he : J \ I = {e}
⊢ J = insert e I
Tactic:
rw [← union_diff_cancel hIJ, he, union_singleton]
State after:
no goals

State before:
case intro.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
hYU : M.cl I ∈ U
hJ : M.Basis' I (X ∪ Y)
hIJ : I ⊆ I
hJ' : M.Basis I (M.cl Y)
hnt : (I \ I).Nontrivial
⊢ M.cl I ⋖[M] M.cl I
Tactic:
simp at hnt
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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
⊢ y ∉ M.cl X
Tactic:
rw [← hI.cl_eq_cl, hI.indep.not_mem_cl_iff_of_not_mem hy.2 hyE]
State after:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
⊢ M.Indep (insert y I)

State before:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
⊢ M.Indep (insert y I)
Tactic:
exact hJ.indep.subset (insert_subset hy.1 hIJ)
State after:
no goals