internlm/Lean-Github huggingface dataset:
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
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
Tactic:
refine' ⟨subset_inter_iff.2 ⟨sub_inter.1, sub_inter.2.trans (subset_insert _ _)⟩,
 fun J J_ind I_sub_J J_sub_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
sub_inter : I ⊆ X ∧ I ⊆ M.E
J : Set α
J_ind : (C.extension e).Indep J
I_sub_J : I ⊆ J
J_sub_X : 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
sub_inter : I ⊆ X ∧ I ⊆ M.E
J : Set α
J_ind : (C.extension e).Indep J
I_sub_J : I ⊆ J
J_sub_X : J ⊆ X ∩ insert e M.E
⊢ I = J
Tactic:
rw [←hI.cl_eq_cl] at hX
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
heX : e ∉ X
I : Set α
hX : M.cl I ∉ C
hI : M.Basis' I X
sub_inter : I ⊆ X ∧ I ⊆ M.E
J : Set α
J_ind : (C.extension e).Indep J
I_sub_J : I ⊆ J
J_sub_X : 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
heX : e ∉ X
I : Set α
hX : M.cl I ∉ C
hI : M.Basis' I X
sub_inter : I ⊆ X ∧ I ⊆ M.E
J : Set α
J_ind : (C.extension e).Indep J
I_sub_J : I ⊆ J
J_sub_X : J ⊆ X ∩ insert e M.E
⊢ I = J
Tactic:
rw [basis'_iff_basis_inter_ground, basis_iff] at hI
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
heX : e ∉ X
I : Set α
hX : M.cl I ∉ C
hI : M.Indep I ∧ I ⊆ X ∩ M.E ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X ∩ M.E → I = J
sub_inter : I ⊆ X ∧ I ⊆ M.E
J : Set α
J_ind : (C.extension e).Indep J
I_sub_J : I ⊆ J
J_sub_X : 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
heX : e ∉ X
I : Set α
hX : M.cl I ∉ C
hI : M.Indep I ∧ I ⊆ X ∩ M.E ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X ∩ M.E → I = J
sub_inter : I ⊆ X ∧ I ⊆ M.E
J : Set α
J_ind : (C.extension e).Indep J
I_sub_J : I ⊆ J
J_sub_X : J ⊆ X ∩ insert e M.E
⊢ I = J
Tactic:
obtain (M_ind | ⟨e_mem, _, _⟩) := (C.extension_indep e).1 J_ind
Proof state after:
case ex_basis.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
heX : e ∉ X
I : Set α
hX : M.cl I ∉ C
hI : M.Indep I ∧ I ⊆ X ∩ M.E ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X ∩ M.E → I = J
sub_inter : I ⊆ X ∧ I ⊆ M.E
J : Set α
J_ind : (C.extension e).Indep J
I_sub_J : I ⊆ J
J_sub_X : J ⊆ X ∩ insert e M.E
M_ind : M.Indep J
⊢ I = J

case ex_basis.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
heX : e ∉ X
I : Set α
hX : M.cl I ∉ C
hI : M.Indep I ∧ I ⊆ X ∩ M.E ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X ∩ M.E → I = J
sub_inter : I ⊆ X ∧ I ⊆ M.E
J : Set α
J_ind : (C.extension e).Indep J
I_sub_J : I ⊆ J
J_sub_X : J ⊆ X ∩ insert e M.E
e_mem : e ∈ J \ M.E
left✝ : M.Indep (J \ {e})
right✝ : M.cl (J \ {e}) ∉ C
⊢ I = J
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_mem
Proof state before:
case ex_basis.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
heX : e ∉ X
I : Set α
hX : M.cl I ∉ C
hI : M.Indep I ∧ I ⊆ X ∩ M.E ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X ∩ M.E → I = J
sub_inter : I ⊆ X ∧ I ⊆ M.E
J : Set α
J_ind : (C.extension e).Indep J
I_sub_J : I ⊆ J
J_sub_X : J ⊆ X ∩ insert e M.E
e_mem : e ∈ J \ M.E
left✝ : M.Indep (J \ {e})
right✝ : M.cl (J \ {e}) ∉ C
⊢ I = J
Tactic:
exact absurd (J_sub_X.trans inter_subset_left e_mem.1) heX
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_mem
Proof state before:
case ex_basis.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
heX : e ∉ X
I : Set α
hX : M.cl I ∉ C
hI : M.Indep I ∧ I ⊆ X ∩ M.E ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X ∩ M.E → I = J
sub_inter : I ⊆ X ∧ I ⊆ M.E
J : Set α
J_ind : (C.extension e).Indep J
I_sub_J : I ⊆ J
J_sub_X : J ⊆ X ∩ insert e M.E
M_ind : M.Indep J
⊢ I = J
Tactic:
apply hI.2.2 _ M_ind I_sub_J
Proof state after:
case ex_basis.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
heX : e ∉ X
I : Set α
hX : M.cl I ∉ C
hI : M.Indep I ∧ I ⊆ X ∩ M.E ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X ∩ M.E → I = J
sub_inter : I ⊆ X ∧ I ⊆ M.E
J : Set α
J_ind : (C.extension e).Indep J
I_sub_J : I ⊆ J
J_sub_X : J ⊆ X ∩ insert e M.E
M_ind : M.Indep J
⊢ J ⊆ X ∩ M.E
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_mem
Proof state before:
case ex_basis.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
heX : e ∉ X
I : Set α
hX : M.cl I ∉ C
hI : M.Indep I ∧ I ⊆ X ∩ M.E ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X ∩ M.E → I = J
sub_inter : I ⊆ X ∧ I ⊆ M.E
J : Set α
J_ind : (C.extension e).Indep J
I_sub_J : I ⊆ J
J_sub_X : J ⊆ X ∩ insert e M.E
M_ind : M.Indep J
⊢ J ⊆ X ∩ M.E
Tactic:
exact fun j j_mem ↦ ⟨(J_sub_X j_mem).1, M_ind.subset_ground j_mem⟩
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_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
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
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
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_dep : (C.extension e).Dep (insert x I)
⊢ x ∈ 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
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_mem : x ∈ I
⊢ x ∈ M.cl I
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_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
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_mem : x ∈ I
⊢ x ∈ M.cl I
Tactic:
exact (M.subset_cl _ hI.indep.subset_ground x_mem)
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_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
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_dep : (C.extension e).Dep (insert x I)
⊢ x ∈ 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
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_dep : (C.extension e).Dep (insert x I)
x_ground : insert x I ⊆ (C.extension e).E
⊢ x ∈ M.cl I
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_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
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_dep : (C.extension e).Dep (insert x I)
x_ground : insert x I ⊆ (C.extension e).E
⊢ x ∈ 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
heX : x ∉ X
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 ∈ 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
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_dep : (C.extension e).Dep (insert x I)
x_ground : insert x I ⊆ (C.extension e).E
ne : x ≠ e
⊢ x ∈ M.cl I
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_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
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_dep : (C.extension e).Dep (insert x I)
x_ground : insert x I ⊆ (C.extension e).E
ne : x ≠ e
⊢ x ∈ M.cl I
Tactic:
rw [hI.indep.mem_cl_iff, ←(@ModularCut.extension_delete _ M C e he), deleteElem,
delete_dep_iff, disjoint_singleton_right]
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
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_dep : (C.extension e).Dep (insert x I)
x_ground : insert x I ⊆ (C.extension e).E
ne : x ≠ e
⊢ (C.extension e).Dep (insert x I) ∧ e ∉ insert x I ∨ x ∈ I
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_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
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_dep : (C.extension e).Dep (insert x I)
x_ground : insert x I ⊆ (C.extension e).E
ne : x ≠ e
⊢ (C.extension e).Dep (insert x I) ∧ e ∉ insert x I ∨ x ∈ I
Tactic:
refine' Or.inl ⟨x_dep, fun e_mem ↦ heX (hI.subset (mem_of_mem_insert_of_ne e_mem ne.symm))⟩
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_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
heX : x ∉ X
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 ∈ M.cl I
Tactic:
rw [dep_iff, (C.extension_indep x), not_or] at x_dep
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
heX : x ∉ X
ex_basis : (C.extension x).Basis' I X
x_mem : x ∈ (C.extension x).cl I
x_dep :
  (¬M.Indep (insert x I) ∧ ¬(x ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {x}) ∧ M.cl (insert x I \ {x}) ∉ C)) ∧
    insert x I ⊆ (C.extension x).E
x_ground : insert x I ⊆ (C.extension x).E
⊢ x ∈ M.cl I
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_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
heX : x ∉ X
ex_basis : (C.extension x).Basis' I X
x_mem : x ∈ (C.extension x).cl I
x_dep :
  (¬M.Indep (insert x I) ∧ ¬(x ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {x}) ∧ M.cl (insert x I \ {x}) ∉ C)) ∧
    insert x I ⊆ (C.extension x).E
x_ground : insert x I ⊆ (C.extension x).E
⊢ x ∈ M.cl I
Tactic:
apply absurd _ x_dep.1.2
Proof state after:
α : 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
heX : x ∉ X
ex_basis : (C.extension x).Basis' I X
x_mem : x ∈ (C.extension x).cl I
x_dep :
  (¬M.Indep (insert x I) ∧ ¬(x ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {x}) ∧ M.cl (insert x I \ {x}) ∉ C)) ∧
    insert x I ⊆ (C.extension x).E
x_ground : insert x I ⊆ (C.extension x).E
⊢ 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_not_mem
Proof state before:
α : 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
heX : x ∉ X
ex_basis : (C.extension x).Basis' I X
x_mem : x ∈ (C.extension x).cl I
x_dep :
  (¬M.Indep (insert x I) ∧ ¬(x ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {x}) ∧ M.cl (insert x I \ {x}) ∉ C)) ∧
    insert x I ⊆ (C.extension x).E
x_ground : insert x I ⊆ (C.extension x).E
⊢ x ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {x}) ∧ M.cl (insert x I \ {x}) ∉ C
Tactic:
rw [insert_diff_self_of_not_mem (not_mem_subset hI.indep.subset_ground he), hI.cl_eq_cl]
Proof state after:
α : 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
heX : x ∉ X
ex_basis : (C.extension x).Basis' I X
x_mem : x ∈ (C.extension x).cl I
x_dep :
  (¬M.Indep (insert x I) ∧ ¬(x ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {x}) ∧ M.cl (insert x I \ {x}) ∉ C)) ∧
    insert x I ⊆ (C.extension x).E
x_ground : insert x I ⊆ (C.extension x).E
⊢ x ∈ insert x I \ M.E ∧ M.Indep I ∧ M.cl X ∉ C
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_mem
Proof state before:
α : 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
heX : x ∉ X
ex_basis : (C.extension x).Basis' I X
x_mem : x ∈ (C.extension x).cl I
x_dep :
  (¬M.Indep (insert x I) ∧ ¬(x ∈ insert x I \ M.E ∧ M.Indep (insert x I \ {x}) ∧ M.cl (insert x I \ {x}) ∉ C)) ∧
    insert x I ⊆ (C.extension x).E
x_ground : insert x I ⊆ (C.extension x).E
⊢ x ∈ insert x I \ M.E ∧ M.Indep I ∧ M.cl X ∉ C
Tactic:
refine' ⟨⟨mem_insert _ _, he⟩, hI.indep, hX⟩
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_mem
Proof state before:
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
Tactic:
have del_dep : ((C.extension e) ＼ e).Dep (insert x I)
Proof state after:
case del_dep
α : 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 ＼ e).Dep (insert x I)

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)
del_dep : (C.extension e ＼ e).Dep (insert 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.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)
del_dep : (C.extension e ＼ e).Dep (insert x I)
⊢ (C.extension e).Dep (insert x I) ∨ x ∈ I
Tactic:
exact Or.inl (delete_dep_iff.1 del_dep).1
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_not_mem
Proof state before:
case del_dep
α : 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 ＼ e).Dep (insert x I)
Tactic:
rwa [C.extension_delete he]
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
⊢ (C.extension e).Flat F ↔ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Tactic:
rw [flat_iff_cl_self]
Proof state after:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
⊢ (C.extension e).cl F = F ↔ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
⊢ (C.extension e).cl F = F ↔ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Tactic:
refine' ⟨fun cl_eq_self ↦ _, fun cl_eq_self ↦ _⟩
Proof state after:
case refine'_1
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C

case refine'_2
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
⊢ (C.extension e).cl F = F
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_2
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
⊢ (C.extension e).cl F = F
Tactic:
sorry
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_1
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Tactic:
obtain (e_mem | e_not_mem) := em (e ∈ F ∧ F \ {e} ∈ C)
Proof state after:
case refine'_1.inl
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_mem : e ∈ F ∧ F \ {e} ∈ C
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C

case refine'_1.inr
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_1.inr
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Tactic:
have M_eq : (C.extension e) ↾ M.E = M
Proof state after:
case M_eq
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
⊢ C.extension e ↾ M.E = M

case refine'_1.inr
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_1.inr
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Tactic:
obtain (e_not_mem | f_not_mem) := not_and_or.1 e_not_mem
Proof state after:
case refine'_1.inr.inl
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C

case refine'_1.inr.inr
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
f_not_mem : F \ {e} ∉ C
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_1.inr.inr
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
f_not_mem : F \ {e} ∉ C
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Tactic:
have e_nF : e ∉ F
Proof state after:
case e_nF
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
f_not_mem : F \ {e} ∉ C
⊢ e ∉ F

case refine'_1.inr.inr
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
f_not_mem : F \ {e} ∉ C
e_nF : e ∉ F
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_1.inl
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_mem : e ∈ F ∧ F \ {e} ∈ C
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Tactic:
exact Or.inr e_mem
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case M_eq
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
⊢ C.extension e ↾ M.E = M
Tactic:
have ground_eq : M.E = (C.extension e).E \ {e}
Proof state after:
case ground_eq
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
⊢ M.E = (C.extension e).E \ {e}

case M_eq
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
ground_eq : M.E = (C.extension e).E \ {e}
⊢ C.extension e ↾ M.E = M
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case M_eq
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
ground_eq : M.E = (C.extension e).E \ {e}
⊢ C.extension e ↾ M.E = M
Tactic:
rw [ground_eq, ←delete]
Proof state after:
case M_eq
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
ground_eq : M.E = (C.extension e).E \ {e}
⊢ (C.extension e).delete {e} = M