internlm/Lean-Github huggingface dataset:
Theorem: Matroid.ModularCut.remove
Proof state before:
case Js_inter_eq.h.e'_3.h.refine'_2.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ Y
b : α
hb : b ∈ B \ Y
⊢ x ∈ B \ {b}
Tactic:
exact ⟨hB₂ x_mem, ne_of_mem_of_not_mem x_mem hb.2⟩
Proof state after:
no goals
Theorem: Matroid.ModularCut.remove
Proof state before:
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ ⋂₀ Js₁
⊢ x ∈ Y
Tactic:
by_contra x_notin_Y
Proof state after:
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ ⋂₀ Js₁
x_notin_Y : x ∉ Y
⊢ False
Theorem: Matroid.ModularCut.remove
Proof state before:
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ ⋂₀ Js₁
x_notin_Y : x ∉ Y
⊢ False
Tactic:
have xBY : x ∈ B \ Y := ⟨Js₁_sInter_sub_B x_mem, x_notin_Y⟩
Proof state after:
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ ⋂₀ Js₁
x_notin_Y : x ∉ Y
xBY : x ∈ B \ Y
⊢ False
Theorem: Matroid.ModularCut.remove
Proof state before:
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ ⋂₀ Js₁
x_notin_Y : x ∉ Y
xBY : x ∈ B \ Y
⊢ False
Tactic:
rw [mem_sInter] at x_mem
Proof state after:
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : ∀ t ∈ Js₁, x ∈ t
x_notin_Y : x ∉ Y
xBY : x ∈ B \ Y
⊢ False
Theorem: Matroid.ModularCut.remove
Proof state before:
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : ∀ t ∈ Js₁, x ∈ t
x_notin_Y : x ∉ Y
xBY : x ∈ B \ Y
⊢ False
Tactic:
exact absurd rfl (x_mem (B \ {x}) ⟨x, xBY, rfl⟩).2
Proof state after:
no goals
Theorem: Matroid.ModularCut.remove
Proof state before:
case inr.a
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
⊢ Js ⊆ C.Fs
Tactic:
rintro J ⟨b, hb, rfl⟩
Proof state after:
case inr.a.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
b : α
hb : b ∈ B \ Y
⊢ M.cl (B \ {b}) ∈ C.Fs
Theorem: Matroid.ModularCut.remove
Proof state before:
case inr.a.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
b : α
hb : b ∈ B \ Y
⊢ M.cl (B \ {b}) ∈ C.Fs
Tactic:
exact h_remove b hb
Proof state after:
no goals
Theorem: Matroid.ModularCut.remove
Proof state before:
case inr.a
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
⊢ Js.Nonempty
Tactic:
obtain ⟨A, a, ha⟩ := Js₁_none
Proof state after:
case inr.a.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
A : Set α
a : α
ha : a ∈ B \ Y ∧ B \ {a} = A
⊢ Js.Nonempty
Theorem: Matroid.ModularCut.remove
Proof state before:
case inr.a.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
A : Set α
a : α
ha : a ∈ B \ Y ∧ B \ {a} = A
⊢ Js.Nonempty
Tactic:
refine' ⟨M.cl (B \ {a}), _⟩
Proof state after:
case inr.a.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
A : Set α
a : α
ha : a ∈ B \ Y ∧ B \ {a} = A
⊢ M.cl (B \ {a}) ∈ Js
Theorem: Matroid.ModularCut.remove
Proof state before:
case inr.a.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
A : Set α
a : α
ha : a ∈ B \ Y ∧ B \ {a} = A
⊢ M.cl (B \ {a}) ∈ Js
Tactic:
refine' ⟨a, ha.1, rfl⟩
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_indep
Proof state before:
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
C : M.ModularCut
e : α
I : Set α
⊢ (C.extension e).Indep I ↔ M.Indep I ∨ e ∈ I \ M.E ∧ M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ C
Tactic:
simp [extension]
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_eq_self
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
e : α
C : M.ModularCut
he : e ∈ M.E
⊢ (C.extension e).E = M.E
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_eq_self
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
e : α
C : M.ModularCut
he : e ∈ M.E
x✝¹ : Set α
x✝ : x✝¹ ⊆ (C.extension e).E
⊢ (C.extension e).Indep x✝¹ ↔ M.Indep x✝¹
Tactic:
simp [he]
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_delete
Proof state before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
C : M.ModularCut
e : α
he : e ∉ M.E
⊢ (C.extension e ＼ e).E = M.E
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_delete
Proof state before:
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
C : M.ModularCut
e : α
he : e ∉ M.E
I : Set α
hI : I ⊆ (C.extension e ＼ e).E
⊢ (C.extension e ＼ e).Indep I ↔ M.Indep I
Tactic:
simp [show e ∉ I from fun heI ↦ by simpa using hI heI]
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_delete
Proof state before:
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
C : M.ModularCut
e : α
he : e ∉ M.E
I : Set α
hI : I ⊆ (C.extension e ＼ e).E
heI : e ∈ I
⊢ False
Tactic:
simpa using hI heI
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
⊢ (C.extension e).cl X = insert e (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
I : Set α
hI : M.Basis' I X
⊢ (C.extension e).cl X = insert e (M.cl X)
Theorem: Matroid.ModularCut.extension_cl_eq_of_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
I : Set α
hI : M.Basis' I X
⊢ (C.extension e).cl X = insert e (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
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
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
⊢ (C.extension e).cl X = insert e (M.cl X)
Theorem: Matroid.ModularCut.extension_cl_eq_of_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
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
⊢ (C.extension e).cl X = insert e (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
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
⊢ ∀ (x : α), x ∈ (C.extension e).cl I ↔ x ∈ insert e (M.cl I)
Theorem: Matroid.ModularCut.extension_cl_eq_of_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
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
⊢ ∀ (x : α), x ∈ (C.extension e).cl I ↔ x ∈ insert e (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
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)

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
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ insert e (M.cl I)
⊢ x ∈ (C.extension e).cl I
Theorem: Matroid.ModularCut.extension_cl_eq_of_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
I : Set α
hI : M.Basis' I X
ex_basis : (C.extension e).Basis' I X
x : α
x_mem : x ∈ insert e (M.cl I)
⊢ x ∈ (C.extension e).cl I
Tactic:
obtain (rfl | x_mem) := x_mem
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
⊢ x ∈ (C.extension x).cl 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
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_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
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.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 ∈ M.cl I
⊢ (C.extension e).Dep (insert x I) ∨ x ∈ I
Theorem: Matroid.ModularCut.extension_cl_eq_of_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
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.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

case intro.refine'_2.inr.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 ∈ M.cl I
x_mem : x ∈ I
⊢ (C.extension e).Dep (insert x I) ∨ x ∈ I
Theorem: Matroid.ModularCut.extension_cl_eq_of_mem
Proof state before:
case intro.refine'_2.inr.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 ∈ 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_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
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
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_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
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
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
Theorem: Matroid.ModularCut.extension_cl_eq_of_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
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
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_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
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
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_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
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
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_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
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, _, cl_not_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
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
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})
cl_not_mem : M.cl (J \ {e}) ∉ C
⊢ I = J
Theorem: Matroid.ModularCut.extension_cl_eq_of_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
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})
cl_not_mem : M.cl (J \ {e}) ∉ C
⊢ I = J
Tactic:
exact absurd hX (fun I_cl_mem ↦ cl_not_mem (C.superset I_cl_mem (M.cl_subset_cl
 (subset_diff_singleton I_sub_J (not_mem_subset hI.1.subset_ground e_mem.2))) (M.cl_flat _)))
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_cl_eq_of_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
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
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_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
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