internlm/Lean-Github huggingface dataset:
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
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
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
⊢ M.cl I ⋖[M] M.cl J
Tactic:
obtain (he | ⟨e, he⟩) := h.eq_empty_or_singleton
Proof state after:
case intro.intro.intro.inl.inl
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
he : J \ I = ∅
⊢ M.cl I ⋖[M] M.cl J

case intro.intro.intro.inl.inr.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e✝ f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
e : α
he : J \ I = {e}
⊢ M.cl I ⋖[M] M.cl J
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.intro.inl.inr.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e✝ f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
e : α
he : J \ I = {e}
⊢ M.cl I ⋖[M] M.cl J
Tactic:
obtain rfl : J = insert e I := by rw [← union_diff_cancel hIJ, he, union_singleton]
Proof state after:
case intro.intro.intro.inl.inr.intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X✝ Y✝ : Set α
e✝ f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
e : α
hYU : M.cl (insert e I) ∈ U
hJ : M.Basis' (insert e I) (X ∪ Y)
hIJ : I ⊆ insert e I
hJ' : M.Basis (insert e I) (M.cl Y)
h : (insert e I \ I).Subsingleton
he : insert e I \ I = {e}
⊢ M.cl I ⋖[M] M.cl (insert e I)
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.intro.inl.inr.intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X✝ Y✝ : Set α
e✝ f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
e : α
hYU : M.cl (insert e I) ∈ U
hJ : M.Basis' (insert e I) (X ∪ Y)
hIJ : I ⊆ insert e I
hJ' : M.Basis (insert e I) (M.cl Y)
h : (insert e I \ I).Subsingleton
he : insert e I \ I = {e}
⊢ M.cl I ⋖[M] M.cl (insert e I)
Tactic:
simpa [show e ∉ I from (he.symm.subset rfl).2] using hJ.indep.cl_diff_covBy (.inl rfl)
Proof state after:
no goals
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.intro.inl.inl
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
he : J \ I = ∅
⊢ M.cl I ⋖[M] M.cl J
Tactic:
rw [(diff_eq_empty.1 he).antisymm hIJ] at hYU
Proof state after:
case intro.intro.intro.inl.inl
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl I ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
he : J \ I = ∅
⊢ M.cl I ⋖[M] M.cl J
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.intro.inl.inl
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl I ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
he : J \ I = ∅
⊢ M.cl I ⋖[M] M.cl J
Tactic:
contradiction
Proof state after:
no goals
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e✝ f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
h : (J \ I).Subsingleton
e : α
he : J \ I = {e}
⊢ J = insert e I
Tactic:
rw [← union_diff_cancel hIJ, he, union_singleton]
Proof state after:
no goals
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
hYU : M.cl I ∈ U
hJ : M.Basis' I (X ∪ Y)
hIJ : I ⊆ I
hJ' : M.Basis I (M.cl Y)
hnt : (I \ I).Nontrivial
⊢ M.cl I ⋖[M] M.cl I
Tactic:
simp at hnt
Proof state after:
no goals
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
⊢ y ∉ M.cl X
Tactic:
rw [← hI.cl_eq_cl, hI.indep.not_mem_cl_iff_of_not_mem hy.2 hyE]
Proof state after:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
⊢ M.Indep (insert y I)
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
⊢ M.Indep (insert y I)
Tactic:
exact hJ.indep.subset (insert_subset hy.1 hIJ)
Proof state after:
no goals
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ F ∈ U.delete {e} ↔ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)
Tactic:
rw [ModularCut.delete, ModularCut.restrict, ModularCut.mem_mk_iff, mem_setOf_eq,
  ← delete_eq_restrict, ← deleteElem, flat_deleteElem_iff]
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U ↔ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U ↔ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U → e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)

case mpr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F) → (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mp
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U → e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)

case mpr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F) → (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Tactic:
rintro ⟨⟨heF, (hF | hF)⟩, hFU⟩
Proof state after:
case mp.intro.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)

case mp.intro.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)

case mpr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F) → (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mpr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F) → (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Tactic:
rintro ⟨heF, (hFU | hFU)⟩
Proof state after:
case mpr.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : F ∈ U
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U

case mpr.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : insert e F ∈ U ∧ e ∈ M.cl F
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mpr.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : insert e F ∈ U ∧ e ∈ M.cl F
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Tactic:
have hfl := U.flat_of_mem hFU.1
Proof state after:
case mpr.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : insert e F ∈ U ∧ e ∈ M.cl F
hfl : M.Flat (insert e F)
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mpr.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : insert e F ∈ U ∧ e ∈ M.cl F
hfl : M.Flat (insert e F)
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Tactic:
rw [← hfl.cl, ← cl_insert_cl_eq_cl_insert, insert_eq_of_mem hFU.2, cl_cl] at hFU
Proof state after:
case mpr.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : M.cl F ∈ U ∧ e ∈ M.cl F
hfl : M.Flat (insert e F)
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mpr.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : M.cl F ∈ U ∧ e ∈ M.cl F
hfl : M.Flat (insert e F)
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Tactic:
exact ⟨⟨heF, .inr hfl⟩, hFU.1⟩
Proof state after:
no goals
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mp.intro.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)
Tactic:
rw [hF.cl] at hFU
Proof state after:
case mp.intro.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : F ∈ U
heF : e ∉ F
hF : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mp.intro.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : F ∈ U
heF : e ∉ F
hF : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)
Tactic:
exact ⟨heF, .inl hFU⟩
Proof state after:
no goals
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mp.intro.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)
Tactic:
rw [← hF.cl]
Proof state after:
case mp.intro.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mp.intro.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
obtain (heF' | heF') := em (e ∈ M.cl F)
Proof state after:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)

case mp.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mp.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
have hF' : M.Flat F := by
  have hFE := ((subset_insert _ _).trans hF.subset_ground)
  rw [flat_iff_subset_cl_self]
  refine (subset_diff_singleton (M.cl_subset_cl (subset_insert e F)) heF').trans ?_
  simp [hF.cl]
Proof state after:
case mp.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hF' : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mp.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hF' : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
rw [hF'.cl] at hFU
Proof state after:
case mp.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hF' : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mp.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hF' : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
exact ⟨heF, .inl hFU⟩
Proof state after:
no goals
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
rw [← insert_eq_of_mem heF'] at hFU
Proof state after:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : insert e (M.cl F) ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : insert e (M.cl F) ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
replace hFU := U.cl_mem_of_mem hFU
Proof state after:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
hFU : M.cl (insert e (M.cl F)) ∈ U
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
hFU : M.cl (insert e (M.cl F)) ∈ U
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
rw [cl_insert_cl_eq_cl_insert] at hFU
Proof state after:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
hFU : M.cl (insert e F) ∈ U
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
hFU : M.cl (insert e F) ∈ U
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
exact ⟨heF, .inr ⟨hFU, heF'⟩⟩
Proof state after:
no goals
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
⊢ M.Flat F
Tactic:
have hFE := ((subset_insert _ _).trans hF.subset_ground)
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hFE : F ⊆ M.E
⊢ M.Flat F
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hFE : F ⊆ M.E
⊢ M.Flat F
Tactic:
rw [flat_iff_subset_cl_self]
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hFE : F ⊆ M.E
⊢ M.cl F ⊆ F
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hFE : F ⊆ M.E
⊢ M.cl F ⊆ F
Tactic:
refine (subset_diff_singleton (M.cl_subset_cl (subset_insert e F)) heF').trans ?_
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hFE : F ⊆ M.E
⊢ M.cl (insert e F) \ {e} ⊆ F
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hFE : F ⊆ M.E
⊢ M.cl (insert e F) \ {e} ⊆ F
Tactic:
simp [hF.cl]
Proof state after:
no goals
Theorem: Matroid.ModularCut.mem_delete_elem_iff
Proof state before:
case mpr.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : F ∈ U
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Tactic:
simpa [(U.flat_of_mem hFU), heF, (U.flat_of_mem hFU).cl]
Proof state after:
no goals
Theorem: Matroid.mem_ofDeleteElem_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ F ∈ ModularCut.ofDeleteElem M e ↔ e ∉ F ∧ M.cl F = insert e F
Tactic:
change _ ∧ _ ↔ _
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ (M ＼ e).Flat F ∧ e ∈ M.cl F ↔ e ∉ F ∧ M.cl F = insert e F
Theorem: Matroid.mem_ofDeleteElem_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ (M ＼ e).Flat F ∧ e ∈ M.cl F ↔ e ∉ F ∧ M.cl F = insert e F
Tactic:
rw [flat_deleteElem_iff, and_assoc, and_congr_right_iff]
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ e ∉ F → ((M.Flat F ∨ M.Flat (insert e F)) ∧ e ∈ M.cl F ↔ M.cl F = insert e F)
Theorem: Matroid.mem_ofDeleteElem_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ e ∉ F → ((M.Flat F ∨ M.Flat (insert e F)) ∧ e ∈ M.cl F ↔ M.cl F = insert e F)
Tactic:
refine fun he ↦ ⟨?_, fun h ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
⊢ (M.Flat F ∨ M.Flat (insert e F)) ∧ e ∈ M.cl F → M.cl F = insert e F

case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
h : M.cl F = insert e F
⊢ (M.Flat F ∨ M.Flat (insert e F)) ∧ e ∈ M.cl F
Theorem: Matroid.mem_ofDeleteElem_iff
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
h : M.cl F = insert e F
⊢ (M.Flat F ∨ M.Flat (insert e F)) ∧ e ∈ M.cl F
Tactic:
rw [h, and_iff_left (.inl rfl), ← h]
Proof state after:
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
h : M.cl F = insert e F
⊢ M.Flat F ∨ M.Flat (M.cl F)
Theorem: Matroid.mem_ofDeleteElem_iff
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
h : M.cl F = insert e F
⊢ M.Flat F ∨ M.Flat (M.cl F)
Tactic:
exact .inr (M.cl_flat F)
Proof state after:
no goals
Theorem: Matroid.mem_ofDeleteElem_iff
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
⊢ (M.Flat F ∨ M.Flat (insert e F)) ∧ e ∈ M.cl F → M.cl F = insert e F
Tactic:
rintro ⟨(hF | hF), heF⟩
Proof state after:
case refine_1.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
heF : e ∈ M.cl F
hF : M.Flat F
⊢ M.cl F = insert e F

case refine_1.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
heF : e ∈ M.cl F
hF : M.Flat (insert e F)
⊢ M.cl F = insert e F
Theorem: Matroid.mem_ofDeleteElem_iff
Proof state before:
case refine_1.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
heF : e ∈ M.cl F
hF : M.Flat (insert e F)
⊢ M.cl F = insert e F
Tactic:
rw [← hF.cl, ← cl_insert_cl_eq_cl_insert, insert_eq_of_mem heF, cl_cl]
Proof state after:
no goals
Theorem: Matroid.mem_ofDeleteElem_iff
Proof state before:
case refine_1.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
heF : e ∈ M.cl F
hF : M.Flat F
⊢ M.cl F = insert e F
Tactic:
rw [hF.cl] at heF
Proof state after:
case refine_1.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
heF : e ∈ F
hF : M.Flat F
⊢ M.cl F = insert e F
Theorem: Matroid.mem_ofDeleteElem_iff
Proof state before:
case refine_1.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
heF : e ∈ F
hF : M.Flat F
⊢ M.cl F = insert e F
Tactic:
contradiction
Proof state after:
no goals
Theorem: Matroid.mem_ofDeleteElem_iff'
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ F ∈ ModularCut.ofDeleteElem M e ↔ e ∈ M.cl F \ F ∧ M.Flat (insert e F)
Tactic:
simp only [deleteElem, mem_ofDeleteElem_iff, mem_diff]
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ e ∉ F ∧ M.cl F = insert e F ↔ (e ∈ M.cl F ∧ e ∉ F) ∧ M.Flat (insert e F)