internlm/Lean-Github huggingface dataset:
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_1
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
⊢ x ∈ insert e (M.cl I)
Tactic:
obtain (x_dep | x_mem) := ex_basis.indep.mem_cl_iff.1 x_mem
Proof state after:
case intro.refine'_1.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : (C.extension e).Dep (insert x I)
⊢ x ∈ insert e (M.cl I)

case intro.refine'_1.inr
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem✝ : x ∈ (C.extension e).cl I
x_mem : x ∈ I
⊢ x ∈ insert e (M.cl I)
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_1.inr
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem✝ : x ∈ (C.extension e).cl I
x_mem : x ∈ I
⊢ x ∈ insert e (M.cl I)
Tactic:
exact Or.inr ((M.subset_cl _ hI.indep.subset_ground) x_mem)
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_1.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : (C.extension e).Dep (insert x I)
⊢ x ∈ insert e (M.cl I)
Tactic:
have x_ground:= x_dep.subset_ground
Proof state after:
case intro.refine'_1.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : (C.extension e).Dep (insert x I)
x_ground : insert x I ⊆ (C.extension e).E
⊢ x ∈ insert e (M.cl I)
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_1.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : (C.extension e).Dep (insert x I)
x_ground : insert x I ⊆ (C.extension e).E
⊢ x ∈ insert e (M.cl I)
Tactic:
obtain (rfl | ne) := eq_or_ne x e
Proof state after:
case intro.refine'_1.inl.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
X : Set α
C : M.ModularCut
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
x : α
he : x ∉ M.E
ex_basis : (C.extension x).Basis' I X
x_mem : x ∈ (C.extension x).cl I
x_dep : (C.extension x).Dep (insert x I)
x_ground : insert x I ⊆ (C.extension x).E
⊢ x ∈ insert x (M.cl I)

case intro.refine'_1.inl.inr
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : (C.extension e).Dep (insert x I)
x_ground : insert x I ⊆ (C.extension e).E
ne : x ≠ e
⊢ x ∈ insert e (M.cl I)
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_1.inl.inr
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : (C.extension e).Dep (insert x I)
x_ground : insert x I ⊆ (C.extension e).E
ne : x ≠ e
⊢ x ∈ insert e (M.cl I)
Tactic:
rw [←not_indep_iff, (C.extension_indep e), not_or, not_indep_iff _] at x_dep
Proof state after:
case intro.refine'_1.inl.inr
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : M.Dep (insert x I) ∧ ¬(e ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {e}) ∧ M.cl (insert x I \ {e}) ∉ C)
x_ground : insert x I ⊆ (C.extension e).E
ne : x ≠ e
⊢ x ∈ insert e (M.cl I)

α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : ¬M.Indep (insert x I) ∧ ¬(e ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {e}) ∧ M.cl (insert x I \ {e}) ∉ C)
x_ground : insert x I ⊆ (C.extension e).E
ne : x ≠ e
⊢ insert x I ⊆ M.E
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : ¬M.Indep (insert x I) ∧ ¬(e ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {e}) ∧ M.cl (insert x I \ {e}) ∉ C)
x_ground : insert x I ⊆ (C.extension e).E
ne : x ≠ e
⊢ insert x I ⊆ M.E
Tactic:
rw [C.extension_ground e, ←diff_singleton_subset_iff, diff_singleton_eq_self _] at x_ground
Proof state after:
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : ¬M.Indep (insert x I) ∧ ¬(e ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {e}) ∧ M.cl (insert x I \ {e}) ∉ C)
x_ground : insert x I ⊆ M.E
ne : x ≠ e
⊢ insert x I ⊆ M.E

α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : ¬M.Indep (insert x I) ∧ ¬(e ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {e}) ∧ M.cl (insert x I \ {e}) ∉ C)
x_ground : insert x I \ {e} ⊆ M.E
ne : x ≠ e
⊢ e ∉ insert x I
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : ¬M.Indep (insert x I) ∧ ¬(e ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {e}) ∧ M.cl (insert x I \ {e}) ∉ C)
x_ground : insert x I \ {e} ⊆ M.E
ne : x ≠ e
⊢ e ∉ insert x I
Tactic:
rintro (rfl | e_I)
Proof state after:
case inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x_mem : e ∈ (C.extension e).cl I
x_dep : ¬M.Indep (insert e I) ∧ ¬(e ∈ insert e I \ M.E ∧ M.Indep (insert e I \ {e}) ∧ M.cl (insert e I \ {e}) ∉ C)
x_ground : insert e I \ {e} ⊆ M.E
ne : e ≠ e
⊢ False

case inr
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : ¬M.Indep (insert x I) ∧ ¬(e ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {e}) ∧ M.cl (insert x I \ {e}) ∉ C)
x_ground : insert x I \ {e} ⊆ M.E
ne : x ≠ e
e_I : e ∈ I
⊢ False
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case inr
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : ¬M.Indep (insert x I) ∧ ¬(e ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {e}) ∧ M.cl (insert x I \ {e}) ∉ C)
x_ground : insert x I \ {e} ⊆ M.E
ne : x ≠ e
e_I : e ∈ I
⊢ False
Tactic:
exact he (hI.indep.subset_ground e_I)
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_1.inl.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
X : Set α
C : M.ModularCut
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
x : α
he : x ∉ M.E
ex_basis : (C.extension x).Basis' I X
x_mem : x ∈ (C.extension x).cl I
x_dep : (C.extension x).Dep (insert x I)
x_ground : insert x I ⊆ (C.extension x).E
⊢ x ∈ insert x (M.cl I)
Tactic:
exact mem_insert _ _
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_1.inl.inr
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : M.Dep (insert x I) ∧ ¬(e ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {e}) ∧ M.cl (insert x I \ {e}) ∉ C)
x_ground : insert x I ⊆ (C.extension e).E
ne : x ≠ e
⊢ x ∈ insert e (M.cl I)
Tactic:
apply Or.inr (hI.indep.mem_cl_iff.2 (Or.inl x_dep.1))
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
x_dep : ¬M.Indep (insert x I) ∧ ¬(e ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {e}) ∧ M.cl (insert x I \ {e}) ∉ C)
x_ground : insert x I ⊆ M.E
ne : x ≠ e
⊢ insert x I ⊆ M.E
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x_mem : e ∈ (C.extension e).cl I
x_dep : ¬M.Indep (insert e I) ∧ ¬(e ∈ insert e I \ M.E ∧ M.Indep (insert e I \ {e}) ∧ M.cl (insert e I \ {e}) ∉ C)
x_ground : insert e I \ {e} ⊆ M.E
ne : e ≠ e
⊢ False
Tactic:
exact ne rfl
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_2.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
X : Set α
C : M.ModularCut
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
x : α
he : x ∉ M.E
ex_basis : (C.extension x).Basis' I X
⊢ x ∈ (C.extension x).cl I
Tactic:
have xnI := (not_mem_subset hI.indep.subset_ground he)
Proof state after:
case intro.refine'_2.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
X : Set α
C : M.ModularCut
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
x : α
he : x ∉ M.E
ex_basis : (C.extension x).Basis' I X
xnI : x ∉ I
⊢ x ∈ (C.extension x).cl I
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_2.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
X : Set α
C : M.ModularCut
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
x : α
he : x ∉ M.E
ex_basis : (C.extension x).Basis' I X
xnI : x ∉ I
⊢ x ∈ (C.extension x).cl I
Tactic:
rw [ex_basis.indep.mem_cl_iff, or_iff_left xnI, dep_iff,
 C.extension_ground, insert_subset_insert_iff xnI, (C.extension_indep x), not_or,
 and_iff_left (hI.indep.subset_ground)]
Proof state after:
case intro.refine'_2.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
X : Set α
C : M.ModularCut
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
x : α
he : x ∉ M.E
ex_basis : (C.extension x).Basis' I X
xnI : x ∉ I
⊢ ¬M.Indep (insert x I) ∧ ¬(x ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {x}) ∧ M.cl (insert x I \ {x}) ∉ C)
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_2.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
X : Set α
C : M.ModularCut
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
x : α
he : x ∉ M.E
ex_basis : (C.extension x).Basis' I X
xnI : x ∉ I
⊢ ¬M.Indep (insert x I) ∧ ¬(x ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {x}) ∧ M.cl (insert x I \ {x}) ∉ C)
Tactic:
refine' ⟨fun hf ↦ he (hf.subset_ground (mem_insert _ _)), fun hf ↦ hf.2.2 _⟩
Proof state after:
case intro.refine'_2.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
X : Set α
C : M.ModularCut
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
x : α
he : x ∉ M.E
ex_basis : (C.extension x).Basis' I X
xnI : x ∉ I
hf : x ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {x}) ∧ M.cl (insert x I \ {x}) ∉ C
⊢ M.cl (insert x I \ {x}) ∈ C
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_2.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
X : Set α
C : M.ModularCut
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
x : α
he : x ∉ M.E
ex_basis : (C.extension x).Basis' I X
xnI : x ∉ I
hf : x ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {x}) ∧ M.cl (insert x I \ {x}) ∉ C
⊢ M.cl (insert x I \ {x}) ∈ C
Tactic:
rwa [insert_diff_self_of_not_mem xnI, hI.cl_eq_cl]
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_2.inr.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
x_dep : M.Dep (insert x I)
⊢ (C.extension e).Dep (insert x I) ∨ x ∈ I
Tactic:
refine' Or.inl (dep_iff.2 ⟨fun ind ↦ _, _⟩)
Proof state after:
case intro.refine'_2.inr.inl.refine'_1
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
x_dep : M.Dep (insert x I)
ind : (C.extension e).Indep (insert x I)
⊢ False

case intro.refine'_2.inr.inl.refine'_2
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
x_dep : M.Dep (insert x I)
⊢ insert x I ⊆ (C.extension e).E
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_2.inr.inl.refine'_2
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
x_dep : M.Dep (insert x I)
⊢ insert x I ⊆ (C.extension e).E
Tactic:
rw [C.extension_ground]
Proof state after:
case intro.refine'_2.inr.inl.refine'_2
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
x_dep : M.Dep (insert x I)
⊢ insert x I ⊆ insert e M.E
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_2.inr.inl.refine'_2
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
x_dep : M.Dep (insert x I)
⊢ insert x I ⊆ insert e M.E
Tactic:
exact (x_dep.subset_ground).trans (subset_insert _ _)
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_2.inr.inl.refine'_1
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
x_dep : M.Dep (insert x I)
ind : (C.extension e).Indep (insert x I)
⊢ False
Tactic:
obtain (M_ind | ⟨e_mem, _⟩) := (C.extension_indep e).1 ind
Proof state after:
case intro.refine'_2.inr.inl.refine'_1.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
x_dep : M.Dep (insert x I)
ind : (C.extension e).Indep (insert x I)
M_ind : M.Indep (insert x I)
⊢ False

case intro.refine'_2.inr.inl.refine'_1.inr.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
x_dep : M.Dep (insert x I)
ind : (C.extension e).Indep (insert x I)
e_mem : e ∈ insert x I \ M.E
right✝ : M.Indep (insert x I \ {e}) ∧ M.cl (insert x I \ {e}) ∉ C
⊢ False
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_2.inr.inl.refine'_1.inr.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
x_dep : M.Dep (insert x I)
ind : (C.extension e).Indep (insert x I)
e_mem : e ∈ insert x I \ M.E
right✝ : M.Indep (insert x I \ {e}) ∧ M.cl (insert x I \ {e}) ∉ C
⊢ False
Tactic:
exact he (x_dep.subset_ground e_mem.1)
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_2.inr.inl.refine'_1.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∈ C
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
x_dep : M.Dep (insert x I)
ind : (C.extension e).Indep (insert x I)
M_ind : M.Indep (insert x I)
⊢ False
Tactic:
exact x_dep.not_indep M_ind
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_mem
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
⊢ (C.extension e).cl X = M.cl X
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
Proof state after:
case intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
⊢ (C.extension e).cl X = M.cl X
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_mem
Proof state before:
case intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
⊢ (C.extension e).cl X = M.cl X
Tactic:
have ex_basis : (extension C e).Basis' I X
Proof state after:
case ex_basis
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
⊢ (C.extension e).Basis' I X

case intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
⊢ (C.extension e).cl X = M.cl X
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_mem
Proof state before:
case intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
⊢ (C.extension e).cl X = M.cl X
Tactic:
rw [←hI.cl_eq_cl, ←ex_basis.cl_eq_cl, ext_iff]
Proof state after:
case intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
⊢ ∀ (x : α), x ∈ (C.extension e).cl I ↔ x ∈ M.cl I
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_mem
Proof state before:
case intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
⊢ ∀ (x : α), x ∈ (C.extension e).cl I ↔ x ∈ M.cl I
Tactic:
refine' fun x ↦ ⟨fun x_mem ↦ _, fun (x_mem) ↦ _⟩
Proof state after:
case intro.refine'_1
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ (C.extension e).cl I
⊢ x ∈ M.cl I

case intro.refine'_2
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
⊢ x ∈ (C.extension e).cl I
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_mem
Proof state before:
case intro.refine'_2
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
⊢ x ∈ (C.extension e).cl I
Tactic:
rw [ex_basis.indep.mem_cl_iff]
Proof state after:
case intro.refine'_2
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
⊢ (C.extension e).Dep (insert x I) ∨ x ∈ I
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_mem
Proof state before:
case intro.refine'_2
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
⊢ (C.extension e).Dep (insert x I) ∨ x ∈ I
Tactic:
obtain (x_dep | x_mem) := hI.indep.mem_cl_iff.1 x_mem
Proof state after:
case intro.refine'_2.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ M.cl I
x_dep : M.Dep (insert x I)
⊢ (C.extension e).Dep (insert x I) ∨ x ∈ I

case intro.refine'_2.inr
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem✝ : x ∈ M.cl I
x_mem : x ∈ I
⊢ (C.extension e).Dep (insert x I) ∨ x ∈ I
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_mem
Proof state before:
case intro.refine'_2.inr
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem✝ : x ∈ M.cl I
x_mem : x ∈ I
⊢ (C.extension e).Dep (insert x I) ∨ x ∈ I
Tactic:
exact Or.inr x_mem
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_mem
Proof state before:
case ex_basis
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
⊢ (C.extension e).Basis' I X
Tactic:
rw [basis'_iff_basis_inter_ground, C.extension_ground, basis_iff, C.extension_indep,
and_iff_right (Or.inl hI.indep)]
Proof state after:
case ex_basis
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
⊢ I ⊆ X ∩ insert e M.E ∧ ∀ (J : Set α), (C.extension e).Indep J → I ⊆ J → J ⊆ X ∩ insert e M.E → I = J
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_mem
Proof state before:
case ex_basis
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
⊢ I ⊆ X ∩ insert e M.E ∧ ∀ (J : Set α), (C.extension e).Indep J → I ⊆ J → J ⊆ X ∩ insert e M.E → I = J
Tactic:
have sub_inter:= subset_inter_iff.1 hI.basis_inter_ground.subset
Proof state after:
case ex_basis
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
hX : M.cl X ∉ C
heX : e ∉ X
I : Set α
hI : M.Basis' I X
sub_inter : I ⊆ X ∧ I ⊆ M.E
⊢ I ⊆ X ∩ insert e M.E ∧ ∀ (J : Set α), (C.extension e).Indep J → I ⊆ J → J ⊆ X ∩ insert e M.E → I = J