internlm/Lean-Github huggingface dataset:
Theorem: Matroid.ModularCut.mem_of_ssubset_indep_of_forall_diff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
⊢ M.cl J ∈ U
Tactic:
have hmod : M.ModularFamily Is := hI.modularFamily_of_subsets (by simp [hIs])
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
⊢ M.cl J ∈ U
Theorem: Matroid.ModularCut.mem_of_ssubset_indep_of_forall_diff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
⊢ M.cl J ∈ U
Tactic:
have hne := nonempty_of_ssubset hJI
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
⊢ M.cl J ∈ U
Theorem: Matroid.ModularCut.mem_of_ssubset_indep_of_forall_diff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
⊢ M.cl J ∈ U
Tactic:
have h_inter : ⋂ e, Is e = J := by
  rw [hIs, ← biInter_eq_iInter (t := fun x _ ↦ I \ {x}), biInter_diff_singleton_eq_diff _ hne,
    diff_diff_right, diff_self, empty_union, inter_eq_self_of_subset_right hJI.subset]
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
⊢ M.cl J ∈ U
Theorem: Matroid.ModularCut.mem_of_ssubset_indep_of_forall_diff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
⊢ M.cl J ∈ U
Tactic:
have _ := hne.coe_sort
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
x✝ : Nonempty ↑(I \ J)
⊢ M.cl J ∈ U
Theorem: Matroid.ModularCut.mem_of_ssubset_indep_of_forall_diff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
x✝ : Nonempty ↑(I \ J)
⊢ M.cl J ∈ U
Tactic:
rw [← h_inter, ← hmod.iInter_cl_eq_cl_iInter]
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
x✝ : Nonempty ↑(I \ J)
⊢ ⋂ i, M.cl (Is i) ∈ U
Theorem: Matroid.ModularCut.mem_of_ssubset_indep_of_forall_diff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
x✝ : Nonempty ↑(I \ J)
⊢ ⋂ i, M.cl (Is i) ∈ U
Tactic:
exact U.iInter_mem _ (fun ⟨i, hi⟩ ↦ h _ (by simpa)) hmod.cls_modularFamily
Proof state after:
no goals
Theorem: Matroid.ModularCut.mem_of_ssubset_indep_of_forall_diff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
⊢ ⋃ i, Is i ⊆ I
Tactic:
simp [hIs]
Proof state after:
no goals
Theorem: Matroid.ModularCut.mem_of_ssubset_indep_of_forall_diff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
⊢ ⋂ e, Is e = J
Tactic:
rw [hIs, ← biInter_eq_iInter (t := fun x _ ↦ I \ {x}), biInter_diff_singleton_eq_diff _ hne,
  diff_diff_right, diff_self, empty_union, inter_eq_self_of_subset_right hJI.subset]
Proof state after:
no goals
Theorem: Matroid.ModularCut.mem_of_ssubset_indep_of_forall_diff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
x✝¹ : Nonempty ↑(I \ J)
x✝ : ↑(I \ J)
i : α
hi : i ∈ I \ J
⊢ ↑⟨i, hi⟩ ∈ I \ J
Tactic:
simpa
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
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
⊢ M.cl X ⋖[M] M.cl Y
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
Proof state after:
case 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
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
⊢ M.cl X ⋖[M] M.cl Y
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case 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
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
⊢ M.cl X ⋖[M] M.cl Y
Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_basis'_of_subset (hI.subset.trans subset_union_left)
Proof state after:
case intro.intro.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
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.59226)
hIJ : I ⊆ J
⊢ M.cl X ⋖[M] M.cl Y
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.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
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.59226)
hIJ : I ⊆ J
⊢ M.cl X ⋖[M] M.cl Y
Tactic:
have hJ' := hJ.basis_cl_right
Proof state after:
case intro.intro.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
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.59226)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl (X ∪ ?m.59226))
⊢ M.cl X ⋖[M] M.cl Y
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.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
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.59226)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl (X ∪ ?m.59226))
⊢ M.cl X ⋖[M] M.cl Y
Tactic:
rw [← cl_cl_union_cl_eq_cl_union, union_eq_self_of_subset_left hXY, cl_cl] at hJ'
Proof state after:
case intro.intro.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
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
⊢ M.cl X ⋖[M] M.cl Y
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.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
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
⊢ M.cl X ⋖[M] M.cl Y
Tactic:
rw [← hI.cl_eq_cl, ← M.cl_cl Y, ← hJ'.cl_eq_cl]
Proof state after:
case intro.intro.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
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
⊢ M.cl I ⋖[M] M.cl J
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.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
hYU : M.cl Y ∈ U
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
⊢ M.cl I ⋖[M] M.cl J
Tactic:
rw [← M.cl_cl Y, ← hJ'.cl_eq_cl] at hYU
Proof state after:
case intro.intro.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
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
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)
⊢ M.cl I ⋖[M] M.cl J
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.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
hXU : M.cl X ∉ U
hmax : ∀ x ∈ Y \ M.cl X, M.cl (insert x X) ∈ U
I : Set α
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)
⊢ M.cl I ⋖[M] M.cl J
Tactic:
rw [← hI.cl_eq_cl] at hXU
Proof state after:
case intro.intro.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)
⊢ M.cl I ⋖[M] M.cl J
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.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)
⊢ M.cl I ⋖[M] M.cl J
Tactic:
obtain (h | hnt) := (J \ I).subsingleton_or_nontrivial
Proof state after:
case intro.intro.intro.inl
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
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

case intro.intro.intro.inr
α : 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
⊢ M.cl I ⋖[M] M.cl J
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.intro.inr
α : 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
⊢ M.cl I ⋖[M] M.cl J
Tactic:
obtain (rfl | hssu) := hIJ.eq_or_ssubset
Proof state after:
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

case intro.intro.intro.inr.inr
α : 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
⊢ M.cl I ⋖[M] M.cl J
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.intro.inr.inr
α : 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
⊢ M.cl I ⋖[M] M.cl J
Tactic:
refine by_contra fun _ ↦ hXU <| U.mem_of_ssubset_indep_of_forall_diff hJ.indep hssu fun x hx ↦ ?_
Proof state after:
case intro.intro.intro.inr.inr
α : 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
⊢ M.cl (J \ {x}) ∈ U
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.intro.inr.inr
α : 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
⊢ M.cl (J \ {x}) ∈ U
Tactic:
obtain ⟨y, hy, hyx⟩ := hnt.exists_ne x
Proof state after:
case intro.intro.intro.inr.inr.intro.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)
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
⊢ M.cl (J \ {x}) ∈ U
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.intro.inr.inr.intro.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)
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
⊢ M.cl (J \ {x}) ∈ U
Tactic:
have hyE : y ∈ M.E := hJ.indep.subset_ground hy.1
Proof state after:
case intro.intro.intro.inr.inr.intro.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)
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.cl (J \ {x}) ∈ U
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.intro.inr.inr.intro.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)
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.cl (J \ {x}) ∈ U
Tactic:
have hyX : y ∉ M.cl X := by
  rw [← hI.cl_eq_cl, hI.indep.not_mem_cl_iff_of_not_mem hy.2 hyE]
  exact hJ.indep.subset (insert_subset hy.1 hIJ)
Proof state after:
case intro.intro.intro.inr.inr.intro.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)
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
hyX : y ∉ M.cl X
⊢ M.cl (J \ {x}) ∈ U
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.intro.inr.inr.intro.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)
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
hyX : y ∉ M.cl X
⊢ M.cl (J \ {x}) ∈ U
Tactic:
have hyY : y ∈ Y := Or.elim (hJ.subset hy.1) (False.elim ∘ (not_mem_of_mem_diff_cl ⟨hyE, hyX⟩)) id
Proof state after:
case intro.intro.intro.inr.inr.intro.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)
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
hyX : y ∉ M.cl X
hyY : y ∈ Y
⊢ M.cl (J \ {x}) ∈ U
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.intro.inr.inr.intro.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)
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
hyX : y ∉ M.cl X
hyY : y ∈ Y
⊢ M.cl (J \ {x}) ∈ U
Tactic:
specialize hmax y ⟨hyY, hyX⟩
Proof state after:
case intro.intro.intro.inr.inr.intro.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
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
hyX : y ∉ M.cl X
hyY : y ∈ Y
hmax : M.cl (insert y X) ∈ U
⊢ M.cl (J \ {x}) ∈ U
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.intro.inr.inr.intro.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
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
hyX : y ∉ M.cl X
hyY : y ∈ Y
hmax : M.cl (insert y X) ∈ U
⊢ M.cl (J \ {x}) ∈ U
Tactic:
rw [← cl_insert_cl_eq_cl_insert, ← hI.cl_eq_cl, cl_insert_cl_eq_cl_insert] at hmax
Proof state after:
case intro.intro.intro.inr.inr.intro.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
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
hyX : y ∉ M.cl X
hyY : y ∈ Y
hmax : M.cl (insert y I) ∈ U
⊢ M.cl (J \ {x}) ∈ U
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.intro.inr.inr.intro.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
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
hyX : y ∉ M.cl X
hyY : y ∈ Y
hmax : M.cl (insert y I) ∈ U
⊢ M.cl (J \ {x}) ∈ U
Tactic:
refine U.cl_superset_mem' hmax ?_
Proof state after:
case intro.intro.intro.inr.inr.intro.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
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
hyX : y ∉ M.cl X
hyY : y ∈ Y
hmax : M.cl (insert y I) ∈ U
⊢ insert y I ⊆ J \ {x}
Theorem: Matroid.ModularCut.covBy_of_maximal_cl
Proof state before:
case intro.intro.intro.inr.inr.intro.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
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
hyX : y ∉ M.cl X
hyY : y ∈ Y
hmax : M.cl (insert y I) ∈ U
⊢ insert y I ⊆ J \ {x}
Tactic:
simp [insert_subset_iff, subset_diff, hIJ, hy.1, hyx.symm, hx.2]
Proof state after:
no goals