internlm/Lean-Github huggingface dataset:
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
case inr.inr.inl.intro
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax :
  M.cl (I \ {e}) = M.cl ((I ∪ B) \ {e}) ∧ ((e ∈ I ↔ M.cl ((I ∪ B) \ {e}) ∈ U) → e ∉ I ∪ B) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl ((I ∪ B) \ {e})) ∧ e ∈ I ∧ M.cl ((I ∪ B) \ {e}) ∈ U
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBsp : M.Spanning (B \ {e})
⊢ False
Tactic:
exact hsp <| hBsp.superset hss hIBe'
Proof state after:
no goals
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax :
  M.cl (I \ {e}) = M.cl ((I ∪ B) \ {e}) ∧ ((e ∈ I ↔ M.cl ((I ∪ B) \ {e}) ∈ U) → e ∉ I ∪ B) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl ((I ∪ B) \ {e})) ∧ e ∈ I ∧ M.cl ((I ∪ B) \ {e}) ∈ U
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
⊢ M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
Tactic:
refine by_contra fun hne ↦ hsp <| ?_
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax :
  M.cl (I \ {e}) = M.cl ((I ∪ B) \ {e}) ∧ ((e ∈ I ↔ M.cl ((I ∪ B) \ {e}) ∈ U) → e ∉ I ∪ B) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl ((I ∪ B) \ {e})) ∧ e ∈ I ∧ M.cl ((I ∪ B) \ {e}) ∈ U
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hne : ¬M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
⊢ M.Spanning ((I ∪ B) \ {e})
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax :
  M.cl (I \ {e}) = M.cl ((I ∪ B) \ {e}) ∧ ((e ∈ I ↔ M.cl ((I ∪ B) \ {e}) ∈ U) → e ∉ I ∪ B) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl ((I ∪ B) \ {e})) ∧ e ∈ I ∧ M.cl ((I ∪ B) \ {e}) ∈ U
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hne : ¬M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
⊢ M.Spanning ((I ∪ B) \ {e})
Tactic:
rw [← cl_spanning_iff hIBe']
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax :
  M.cl (I \ {e}) = M.cl ((I ∪ B) \ {e}) ∧ ((e ∈ I ↔ M.cl ((I ∪ B) \ {e}) ∈ U) → e ∉ I ∪ B) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl ((I ∪ B) \ {e})) ∧ e ∈ I ∧ M.cl ((I ∪ B) \ {e}) ∈ U
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hne : ¬M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
⊢ M.Spanning (M.cl ((I ∪ B) \ {e}))
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax :
  M.cl (I \ {e}) = M.cl ((I ∪ B) \ {e}) ∧ ((e ∈ I ↔ M.cl ((I ∪ B) \ {e}) ∈ U) → e ∉ I ∪ B) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl ((I ∪ B) \ {e})) ∧ e ∈ I ∧ M.cl ((I ∪ B) \ {e}) ∈ U
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hne : ¬M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
⊢ M.Spanning (M.cl ((I ∪ B) \ {e}))
Tactic:
have hssu := (M.cl_subset_cl hss).ssubset_of_ne hne
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax :
  M.cl (I \ {e}) = M.cl ((I ∪ B) \ {e}) ∧ ((e ∈ I ↔ M.cl ((I ∪ B) \ {e}) ∈ U) → e ∉ I ∪ B) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl ((I ∪ B) \ {e})) ∧ e ∈ I ∧ M.cl ((I ∪ B) \ {e}) ∈ U
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hne : ¬M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
hssu : M.cl (B \ {e}) ⊂ M.cl ((I ∪ B) \ {e})
⊢ M.Spanning (M.cl ((I ∪ B) \ {e}))
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax :
  M.cl (I \ {e}) = M.cl ((I ∪ B) \ {e}) ∧ ((e ∈ I ↔ M.cl ((I ∪ B) \ {e}) ∈ U) → e ∉ I ∪ B) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl ((I ∪ B) \ {e})) ∧ e ∈ I ∧ M.cl ((I ∪ B) \ {e}) ∈ U
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hne : ¬M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
hssu : M.cl (B \ {e}) ⊂ M.cl ((I ∪ B) \ {e})
⊢ M.Spanning (M.cl ((I ∪ B) \ {e}))
Tactic:
exact hBhp.spanning_of_ssuperset hssu
Proof state after:
no goals
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : M.Indep (B \ {e}) ∧ M.cl (B \ {e}) ∉ U
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax :
  M.cl (I \ {e}) = M.cl ((I ∪ B) \ {e}) ∧ ((e ∈ I ↔ M.cl ((I ∪ B) \ {e}) ∈ U) → e ∉ I ∪ B) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl ((I ∪ B) \ {e})) ∧ e ∈ I ∧ M.cl ((I ∪ B) \ {e}) ∈ U
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hclcl : M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
⊢ M.cl (I \ {e}) = M.cl (B \ {e}) ∧ e ∈ I
Tactic:
simpa [heB, ← hclcl, hB.2] using hImax
Proof state after:
no goals
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : M.Indep (B \ {e}) ∧ M.cl (B \ {e}) ∉ U
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
hU : M.E ∈ U
hInmax : (M.Spanning (I \ {e}) → ¬(e ∈ I → False ∧ e ∉ M.E)) ∧ (M.Hyperplane (M.cl (I \ {e})) → e ∉ I)
hsp : ¬M.Spanning ((I ∪ B) \ {e})
hBhp : M.Hyperplane (M.cl (B \ {e}))
heB : e ∈ B
hclcl : M.cl (B \ {e}) = M.cl ((I ∪ B) \ {e})
hImax : M.cl (I \ {e}) = M.cl (B \ {e}) ∧ e ∈ I
⊢ ¬M.Hyperplane (M.cl (I \ {e}))
Tactic:
simpa [hImax.2] using hInmax
Proof state after:
no goals
Theorem: Matroid.ModularCut.extIndep_aug
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)
Tactic:
obtain (he | he) := em' (M.Coloop e)
Proof state after:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : ¬M.Coloop e
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)

case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : M.Coloop e
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)
Theorem: Matroid.ModularCut.extIndep_aug
Proof state before:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : M.Coloop e
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)
Tactic:
have hrw : (U.delete {e}).ExtIndep e = U.ExtIndep e := by
  ext; simp [ExtIndep, he.mem_cl_iff_mem, ModularCut.mem_delete_elem_iff]
Proof state after:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : M.Coloop e
hrw : (U.delete {e}).ExtIndep e = U.ExtIndep e
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)
Theorem: Matroid.ModularCut.extIndep_aug
Proof state before:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : M.Coloop e
hrw : (U.delete {e}).ExtIndep e = U.ExtIndep e
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)
Tactic:
simp_rw [← hrw] at hInmax hBmax hI ⊢
Proof state after:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.Coloop e
hrw : (U.delete {e}).ExtIndep e = U.ExtIndep e
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (U.delete {e}).ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (U.delete {e}).ExtIndep e I}
hI : (U.delete {e}).ExtIndep e I
⊢ ∃ x ∈ B \ I, (U.delete {e}).ExtIndep e (insert x I)
Theorem: Matroid.ModularCut.extIndep_aug
Proof state before:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.Coloop e
hrw : (U.delete {e}).ExtIndep e = U.ExtIndep e
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (U.delete {e}).ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (U.delete {e}).ExtIndep e I}
hI : (U.delete {e}).ExtIndep e I
⊢ ∃ x ∈ B \ I, (U.delete {e}).ExtIndep e (insert x I)
Tactic:
exact (U.delete {e}).extIndep_aug_of_not_coloop (fun h ↦ h.mem_ground.2 rfl) hI hInmax hBmax
Proof state after:
no goals
Theorem: Matroid.ModularCut.extIndep_aug
Proof state before:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : ¬M.Coloop e
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)
Tactic:
exact U.extIndep_aug_of_not_coloop he hI hInmax hBmax
Proof state after:
no goals
Theorem: Matroid.ModularCut.extIndep_aug
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : M.Coloop e
⊢ (U.delete {e}).ExtIndep e = U.ExtIndep e
Tactic:
ext
Proof state after:
case h.a
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : M.Coloop e
x✝ : Set α
⊢ (U.delete {e}).ExtIndep e x✝ ↔ U.ExtIndep e x✝
Theorem: Matroid.ModularCut.extIndep_aug
Proof state before:
case h.a
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
he : M.Coloop e
x✝ : Set α
⊢ (U.delete {e}).ExtIndep e x✝ ↔ U.ExtIndep e x✝
Tactic:
simp [ExtIndep, he.mem_cl_iff_mem, ModularCut.mem_delete_elem_iff]
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
⊢ ExistsMaximalSubsetProperty (U.ExtIndep e) X
Tactic:
intro I hI hIX
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
⊢ (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:
α : 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)
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 α
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}
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 α
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
Proof 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}
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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⟩
Proof 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}
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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)
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
Proof 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