internlm/Lean-Github huggingface dataset:
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.cl F = insert e F ↔ (e ∈ M.cl F ∧ e ∉ F) ∧ M.Flat (insert e F)
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨h.1.2, ?_⟩⟩
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
h : e ∉ F ∧ M.cl F = insert e F
⊢ (e ∈ M.cl F ∧ e ∉ F) ∧ M.Flat (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
h : (e ∈ M.cl F ∧ e ∉ F) ∧ M.Flat (insert e F)
⊢ M.cl F = insert e 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
h : (e ∈ M.cl F ∧ e ∉ F) ∧ M.Flat (insert e F)
⊢ M.cl F = insert e F
Tactic:
rw [← h.2.cl, ← cl_insert_cl_eq_cl_insert, insert_eq_of_mem h.1.1, cl_cl]
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
h : e ∉ F ∧ M.cl F = insert e F
⊢ (e ∈ M.cl F ∧ e ∉ F) ∧ M.Flat (insert e F)
Tactic:
rw [← h.2, and_iff_left <| M.cl_flat F, and_iff_left h.1, h.2]
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
h : e ∉ F ∧ M.cl F = insert e F
⊢ e ∈ insert e F
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
h : e ∉ F ∧ M.cl F = insert e F
⊢ e ∈ insert e F
Tactic:
exact mem_insert _ _
Proof state after:
no goals
Theorem: Matroid.ModularCut.extIndep_iff_of_not_mem
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heI : e ∉ I
⊢ U.ExtIndep e I ↔ M.Indep I
Tactic:
simp [ExtIndep, heI]
Proof state after:
no goals
Theorem: Matroid.ModularCut.extIndep_iff_of_mem
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heI : e ∈ I
⊢ U.ExtIndep e I ↔ M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
Tactic:
simp [ExtIndep, heI]
Proof state after:
no goals
Theorem: Matroid.ModularCut.ExtIndep.diff_singleton_indep
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : U.ExtIndep e I
⊢ M.Indep (I \ {e})
Tactic:
obtain (h | h) := h
Proof state after:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : M.Indep I ∧ e ∉ I
⊢ M.Indep (I \ {e})

case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U ∧ e ∈ I
⊢ M.Indep (I \ {e})
Theorem: Matroid.ModularCut.ExtIndep.diff_singleton_indep
Proof state before:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : M.Indep I ∧ e ∉ I
⊢ M.Indep (I \ {e})

case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U ∧ e ∈ I
⊢ M.Indep (I \ {e})
Tactic:
exact h.1.diff _
Proof state after:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U ∧ e ∈ I
⊢ M.Indep (I \ {e})
Theorem: Matroid.ModularCut.ExtIndep.diff_singleton_indep
Proof state before:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U ∧ e ∈ I
⊢ M.Indep (I \ {e})
Tactic:
exact h.1
Proof state after:
no goals
Theorem: Matroid.ModularCut.ExtIndep.subset
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : U.ExtIndep e I
hJI : J ⊆ I
⊢ U.ExtIndep e J
Tactic:
obtain (heJ | heJ) := em (e ∈ J)
Proof state after:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : U.ExtIndep e I
hJI : J ⊆ I
heJ : e ∈ J
⊢ U.ExtIndep e J

case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : U.ExtIndep e I
hJI : J ⊆ I
heJ : e ∉ J
⊢ U.ExtIndep e J
Theorem: Matroid.ModularCut.ExtIndep.subset
Proof state before:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : U.ExtIndep e I
hJI : J ⊆ I
heJ : e ∉ J
⊢ U.ExtIndep e J
Tactic:
rw [extIndep_iff_of_not_mem heJ]
Proof state after:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : U.ExtIndep e I
hJI : J ⊆ I
heJ : e ∉ J
⊢ M.Indep J
Theorem: Matroid.ModularCut.ExtIndep.subset
Proof state before:
case inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : U.ExtIndep e I
hJI : J ⊆ I
heJ : e ∉ J
⊢ M.Indep J
Tactic:
exact h.diff_singleton_indep.subset (subset_diff_singleton hJI heJ)
Proof state after:
no goals
Theorem: Matroid.ModularCut.ExtIndep.subset
Proof state before:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : U.ExtIndep e I
hJI : J ⊆ I
heJ : e ∈ J
⊢ U.ExtIndep e J
Tactic:
rw [extIndep_iff_of_mem (hJI heJ)] at h
Proof state after:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hJI : J ⊆ I
heJ : e ∈ J
⊢ U.ExtIndep e J
Theorem: Matroid.ModularCut.ExtIndep.subset
Proof state before:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hJI : J ⊆ I
heJ : e ∈ J
⊢ U.ExtIndep e J
Tactic:
rw [extIndep_iff_of_mem heJ, and_iff_right (h.1.subset (diff_subset_diff_left hJI))]
Proof state after:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hJI : J ⊆ I
heJ : e ∈ J
⊢ M.cl (J \ {e}) ∉ U
Theorem: Matroid.ModularCut.ExtIndep.subset
Proof state before:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hJI : J ⊆ I
heJ : e ∈ J
⊢ M.cl (J \ {e}) ∉ U
Tactic:
exact fun hJU ↦ h.2 <| U.cl_superset_mem' hJU <| diff_subset_diff_left hJI
Proof state after:
no goals
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ X} ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ I ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
have hss : I \ {e} ⊆ X \ {e} := diff_subset_diff_left hIX
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ X} ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ I ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ X} ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ I ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
have hX' : X \ {e} ⊆ M.E := by simpa
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ X} ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ I ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ X} ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ I ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
rw [mem_maximals_iff_forall_insert (fun _ _ ht hst ↦ ⟨ht.1.subset hst, hst.trans ht.2⟩)]
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
⊢ ((U.ExtIndep e I ∧ I ⊆ X) ∧ ∀ x ∉ I, ¬(U.ExtIndep e (insert x I) ∧ insert x I ⊆ X)) ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ I ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
⊢ ((U.ExtIndep e I ∧ I ⊆ X) ∧ ∀ x ∉ I, ¬(U.ExtIndep e (insert x I) ∧ insert x I ⊆ X)) ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ ((e ∈ I ↔ M.cl (X \ {e}) ∈ U) → e ∉ X) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
simp only [hI, hIX, and_self, insert_subset_iff, and_true, not_and, true_and, imp_not_comm]
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
⊢ (∀ x ∉ I, x ∈ X → ¬U.ExtIndep e (insert x I)) ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
⊢ (∀ x ∉ I, x ∈ X → ¬U.ExtIndep e (insert x I)) ↔
    M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
refine ⟨fun h ↦ ?_, fun h x hxI hi hind ↦ ?_⟩
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
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h : ∀ x ∉ I, x ∈ X → ¬U.ExtIndep e (insert x I)
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U

case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
⊢ False
Theorem: Matroid.ModularCut.maximal_extIndep_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
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
⊢ False
Tactic:
by_cases heI : e ∈ I
Proof state after:
case pos
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∈ I
⊢ False

case neg
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
⊢ False
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case neg
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
⊢ False
Tactic:
simp only [heI, not_false_eq_true, diff_singleton_eq_self, false_iff, not_not, false_and,
  and_false, or_false] at h
Proof state after:
case neg
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
⊢ False
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case neg
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
⊢ False
Tactic:
obtain (rfl | hne) := eq_or_ne e x
Proof state after:
case neg.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hxI : e ∉ I
hi : e ∈ X
hind : U.ExtIndep e (insert e I)
⊢ False

case neg.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ False
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case neg.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ False
Tactic:
rw [extIndep_iff_of_not_mem heI] at hI
Proof state after:
case neg.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ False
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case neg.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : U.ExtIndep e (insert x I)
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ False
Tactic:
rw [extIndep_iff_of_not_mem (by simp [heI, hne]), hI.insert_indep_iff_of_not_mem hxI, h.1] at hind
Proof state after:
case neg.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (X \ {e})
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ False
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case neg.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (X \ {e})
heI : e ∉ I
h : M.cl I = M.cl (X \ {e}) ∧ (e ∈ X → M.cl (X \ {e}) ∈ U)
hne : e ≠ x
⊢ False
Tactic:
refine not_mem_of_mem_diff_cl hind ⟨hi, hne.symm⟩
Proof state after:
no goals
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
⊢ X \ {e} ⊆ M.E
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.ModularCut.maximal_extIndep_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
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h : ∀ x ∉ I, x ∈ X → ¬U.ExtIndep e (insert x I)
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
simp only [ExtIndep, insert_subset_iff, hIX, and_true, imp_not_comm, not_or, not_and,
  not_not] at 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
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Theorem: Matroid.ModularCut.maximal_extIndep_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
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
obtain (heI | heI) := em (e ∈ I)
Proof state after:
case refine_1.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U

case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∉ I
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∉ I
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
simp only [mem_insert_iff, heI, or_false] at h
Proof state after:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
have hXI : M.cl (X \ {e}) = M.cl (I \ {e}) := by
  refine (M.cl_subset_cl hss).antisymm' (M.cl_subset_cl_of_subset_cl fun x hx ↦ ?_)
  rw [hI.diff_singleton_indep.mem_cl_iff', and_iff_right (hX' hx), mem_diff, and_iff_left hx.2,
    diff_singleton_eq_self heI]
  exact fun h' ↦ by_contra fun hxI ↦ by simp [(h x hxI hx.1).1 h'] at hx
Proof state after:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
hXI : M.cl (X \ {e}) = M.cl (I \ {e})
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
hXI : M.cl (X \ {e}) = M.cl (I \ {e})
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ (e ∈ X → ¬(e ∈ I ↔ M.cl (X \ {e}) ∈ U)) ∨
    (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ e ∈ I ∧ M.cl (X \ {e}) ∈ U
Tactic:
simp only [heI, not_false_eq_true, diff_singleton_eq_self, hXI, false_iff, not_imp_not,
  true_and, false_and, and_false, or_false]
Proof state after:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
hXI : M.cl (X \ {e}) = M.cl (I \ {e})
⊢ e ∈ X → ¬M.cl I ∉ U
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
hXI : M.cl (X \ {e}) = M.cl (I \ {e})
⊢ e ∈ X → ¬M.cl I ∉ U
Tactic:
intro heX
Proof state after:
case refine_1.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : U.ExtIndep e I
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∉ I
h : ∀ x ∉ I, x ∈ X → (M.Indep (insert x I) → e = x) ∧ (M.Indep (insert x I \ {e}) → e = x → M.cl (insert x I \ {e}) ∈ U)
hXI : M.cl (X \ {e}) = M.cl (I \ {e})
heX : e ∈ X
⊢ ¬M.cl I ∉ U