internlm/Lean-Github huggingface dataset:
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
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
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 :
  ¬(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
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
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
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}
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
⊢ U.ExtIndep e (insert e J)
Tactic:
rw [extIndep_iff_of_mem (.inl rfl)]
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
⊢ M.Indep (insert e J \ {e}) ∧ M.cl (insert e J \ {e}) ∉ U
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
⊢ M.Indep (insert e J \ {e}) ∧ M.cl (insert e J \ {e}) ∉ U
Tactic:
simpa [heJ, hJ.indep, hJ.cl_eq_cl]
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}
heX : e ∈ X
hcl : M.cl (X \ {e}) ∉ U
hind : U.ExtIndep e (insert e J)
⊢ I ⊆ insert e J
Tactic:
simpa using hIJ
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}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
⊢ e ∈ I
Tactic:
refine by_contra fun heI ↦ ?_
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}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
heI : e ∉ I
⊢ 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}
hconJe : e ∈ X → M.cl (X \ {e}) ∈ U
heI : e ∉ I
⊢ False
Tactic:
rw [diff_singleton_eq_self heI] at 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 ⊆ 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:
α : 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
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 ⊆ 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
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 ⊆ 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
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 ⊆ 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
Proof state after:
no goals
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
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 (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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
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 : 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
Proof 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
Theorem: Matroid.ModularCut.existsMaximalSubsetProperty
Proof 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
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 : 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
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 : 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
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 : 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]
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 : 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]
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 : 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
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 : 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⟩
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 : 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
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 : 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)
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 : 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
Proof state after:
no goals
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
⊢ (M ＼ e).extendBy e (ofDeleteElem M e) = M
Tactic:
refine Eq.symm <| eq_of_indep_iff_indep_forall (by simp [he]) fun I hI ↦ ?_
Proof state after:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I
Tactic:
obtain (heI | heI) := em' (e ∈ I)
Proof state after:
case inl
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∉ I
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I

case inr
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∈ I
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
case inl
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∉ I
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I

case inr
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∈ I
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I
Tactic:
simp [extIndep_iff_of_not_mem heI, heI]
Proof state after:
case inr
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∈ I
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
case inr
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∈ I
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I
Tactic:
obtain ⟨I, rfl, heI'⟩ : ∃ J, I = insert e J ∧ e ∉ J := ⟨I \ {e}, by simp [heI], by simp⟩
Proof state after:
case inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
⊢ M.Indep (insert e I) ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep (insert e I)
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
case inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
⊢ M.Indep (insert e I) ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep (insert e I)
Tactic:
suffices
  M.Indep (insert e I) ↔ M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))) by
  simpa [extIndep_iff_of_mem heI, heI']
Proof state after:
case inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
case inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
Tactic:
refine ⟨fun h ↦ ⟨h.subset (subset_insert _ _), fun he _ ↦ ?_⟩, fun ⟨hIi, h⟩ ↦ ?_⟩
Proof state after:
case inr.intro.intro.refine_1
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he✝ : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
h : M.Indep (insert e I)
he : e ∈ M.cl (M.cl I \ {e})
x✝ : M.Flat (insert e (M.cl I))
⊢ False

case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
h : e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))
⊢ M.Indep (insert e I)
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
h : e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))
⊢ M.Indep (insert e I)
Tactic:
rw [hIi.insert_indep_iff_of_not_mem heI', mem_diff, and_iff_right (hI (.inl rfl))]
Proof state after:
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
h : e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))
⊢ e ∉ M.cl I
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
h : e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))
⊢ e ∉ M.cl I
Tactic:
refine fun heCl ↦ ?_
Proof state after:
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
h : e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))
heCl : e ∈ M.cl I
⊢ False