internlm/Lean-Github huggingface dataset:
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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 ↦ ?_)
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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'
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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]
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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⟩
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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)
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof state after:
no goals
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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, ?_⟩
Proof 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}
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof 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}
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof 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}
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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]
Proof 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✝
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof state after:
no goals
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof state after:
no goals
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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 ↦ ?_
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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]
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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)
Proof 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