internlm/Lean-Github huggingface dataset:
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
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
hxe : x ≠ e
⊢ False
Tactic:
rw [extIndep_iff_of_mem (.inr heI), ← insert_diff_singleton_comm hxe,
  hI.1.insert_indep_iff_of_not_mem (by simp [hxI, hxe])] at hind
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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
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 : x ∈ M.E \ M.cl (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
⊢ False
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
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 : x ∈ M.E \ M.cl (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
⊢ False
Tactic:
simp only [hIX heI, heI, true_iff, true_implies, true_and] at h
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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
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 (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
h : M.cl (I \ {e}) = M.cl (X \ {e}) ∧ M.cl (X \ {e}) ∉ U ∨ (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ M.cl (X \ {e}) ∈ U
⊢ False
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
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 (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
h : M.cl (I \ {e}) = M.cl (X \ {e}) ∧ M.cl (X \ {e}) ∉ U ∨ (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})) ∧ M.cl (X \ {e}) ∈ U
⊢ False
Tactic:
obtain (⟨h_eq, -⟩ | ⟨hcv, h⟩) := h
Proof state after:
case pos.inl.intro
α : 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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
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 (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
h_eq : M.cl (I \ {e}) = M.cl (X \ {e})
⊢ False

case pos.inr.intro
α : 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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
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 (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
hcv : M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})
h : M.cl (X \ {e}) ∈ U
⊢ False
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case pos.inr.intro
α : 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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
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 (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
hcv : M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})
h : M.cl (X \ {e}) ∈ U
⊢ False
Tactic:
rw [hcv.eq_cl_insert_of_mem_diff ⟨M.mem_cl_of_mem ⟨hi, hxe⟩, hind.1.2⟩,
  cl_insert_cl_eq_cl_insert] at h
Proof state after:
case pos.inr.intro
α : 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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
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 (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
hcv : M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})
h : M.cl (insert x (I \ {e})) ∈ U
⊢ False
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case pos.inr.intro
α : 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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
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 (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
hcv : M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})
h : M.cl (insert x (I \ {e})) ∈ U
⊢ False
Tactic:
exact hind.2 h
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}
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
⊢ x ≠ e
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
f : α
U : M.ModularCut
hIX : I ⊆ X
x : α
hxI : x ∉ I
hi : x ∈ X
hX : X ⊆ insert x M.E
hI : U.ExtIndep x I
hss : I \ {x} ⊆ X \ {x}
hX' : X \ {x} ⊆ M.E
h :
  M.cl (I \ {x}) = M.cl (X \ {x}) ∧ (x ∈ X → ¬(x ∈ I ↔ M.cl (X \ {x}) ∈ U)) ∨
    (M.cl (I \ {x}) ⋖[M] M.cl (X \ {x})) ∧ x ∈ I ∧ M.cl (X \ {x}) ∈ U
hind : U.ExtIndep x (insert x I)
heI : x ∈ I
⊢ False
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
f : α
U : M.ModularCut
hIX : I ⊆ X
x : α
hxI : x ∉ I
hi : x ∈ X
hX : X ⊆ insert x M.E
hI : U.ExtIndep x I
hss : I \ {x} ⊆ X \ {x}
hX' : X \ {x} ⊆ M.E
h :
  M.cl (I \ {x}) = M.cl (X \ {x}) ∧ (x ∈ X → ¬(x ∈ I ↔ M.cl (X \ {x}) ∈ U)) ∨
    (M.cl (I \ {x}) ⋖[M] M.cl (X \ {x})) ∧ x ∈ I ∧ M.cl (X \ {x}) ∈ U
hind : U.ExtIndep x (insert x I)
heI : x ∈ I
⊢ False
Tactic:
contradiction
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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
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 : M.Indep (insert x (I \ {e})) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
⊢ x ∉ I \ {e}
Tactic:
simp [hxI, hxe]
Proof state after:
no goals
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case pos.inl.intro
α : 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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
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 (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
h_eq : M.cl (I \ {e}) = M.cl (X \ {e})
⊢ False
Tactic:
exact not_mem_of_mem_diff_cl (h_eq ▸ hind.1) <| by simp [hi, hxe]
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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
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 (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
h_eq : M.cl (I \ {e}) = M.cl (X \ {e})
⊢ x ∈ X \ {e}
Tactic:
simp [hi, hxe]
Proof state after:
no goals
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
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
Tactic:
rw [extIndep_iff_of_mem (.inl rfl)] at hind
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 : M.Indep (insert e I \ {e}) ∧ M.cl (insert e I \ {e}) ∉ U
⊢ False
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
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 : M.Indep (insert e I \ {e}) ∧ M.cl (insert e I \ {e}) ∉ U
⊢ False
Tactic:
simp only [mem_singleton_iff, insert_diff_of_mem, hxI, not_false_eq_true,
  diff_singleton_eq_self, h.1] at hind
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 : M.Indep I ∧ M.cl (X \ {e}) ∉ U
⊢ False
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
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 : M.Indep I ∧ M.cl (X \ {e}) ∉ U
⊢ False
Tactic:
exact hind.2 <| h.2 hi
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 : 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
⊢ e ∉ insert x I
Tactic:
simp [heI, hne]
Proof state after:
no goals
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : ¬M.Coloop e
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)
Tactic:
rw [coloop_iff_diff_cl, not_not] at he
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
⊢ ∃ x ∈ B \ I, U.ExtIndep e (insert x I)
Tactic:
by_contra! hcon
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
⊢ False
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
⊢ False
Tactic:
have hB : U.ExtIndep e B := hBmax.1
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
⊢ False
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
⊢ False
Tactic:
have hIeE := hI.diff_singleton_indep.subset_ground
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
⊢ False
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
⊢ False
Tactic:
have hBeE := hB.diff_singleton_indep.subset_ground
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
⊢ False
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
⊢ False
Tactic:
have hss : B \ {e} ⊆ (I ∪ B) \ {e} := diff_subset_diff_left subset_union_right
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
⊢ False
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
⊢ False
Tactic:
have hIBe : I ∪ B ⊆ insert e M.E :=
  union_subset hI.subset_insert_ground hB.subset_insert_ground
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
⊢ False
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
⊢ False
Tactic:
have hIBe' : (I ∪ B) \ {e} ⊆ M.E := by rwa [diff_singleton_subset_iff]
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
⊢ False
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
⊢ False
Tactic:
have hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E} := by
  simp only [ext_iff, mem_setOf_eq, iff_self_and]
  exact  fun _ ↦ ExtIndep.subset_insert_ground
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
⊢ False
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
⊢ False
Tactic:
rw [hrw, U.maximal_extIndep_iff Subset.rfl hI hI.subset_insert_ground] at hInmax
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax :
  ¬(M.cl (I \ {e}) = M.cl (insert e M.E \ {e}) ∧ ((e ∈ I ↔ M.cl (insert e M.E \ {e}) ∈ U) → e ∉ insert e M.E) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (insert e M.E \ {e})) ∧ e ∈ I ∧ M.cl (insert e M.E \ {e}) ∈ U)
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
⊢ False
Theorem: Matroid.ModularCut.extIndep_aug_of_not_coloop
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax :
  ¬(M.cl (I \ {e}) = M.cl (insert e M.E \ {e}) ∧ ((e ∈ I ↔ M.cl (insert e M.E \ {e}) ∈ U) → e ∉ insert e M.E) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (insert e M.E \ {e})) ∧ e ∈ I ∧ M.cl (insert e M.E \ {e}) ∈ U)
hBmax : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | U.ExtIndep e I}
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
⊢ False
Tactic:
rw [hrw, U.maximal_extIndep_iff Subset.rfl hB hB.subset_insert_ground] at hBmax
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : M.cl (M.E \ {e}) = M.E
hI : U.ExtIndep e I
hInmax :
  ¬(M.cl (I \ {e}) = M.cl (insert e M.E \ {e}) ∧ ((e ∈ I ↔ M.cl (insert e M.E \ {e}) ∈ U) → e ∉ insert e M.E) ∨
      (M.cl (I \ {e}) ⋖[M] M.cl (insert e M.E \ {e})) ∧ e ∈ I ∧ M.cl (insert e M.E \ {e}) ∈ U)
hBmax :
  M.cl (B \ {e}) = M.cl (insert e M.E \ {e}) ∧ ((e ∈ B ↔ M.cl (insert e M.E \ {e}) ∈ U) → e ∉ insert e M.E) ∨
    (M.cl (B \ {e}) ⋖[M] M.cl (insert e M.E \ {e})) ∧ e ∈ B ∧ M.cl (insert e M.E \ {e}) ∈ U
hcon : ∀ x ∈ B \ I, ¬U.ExtIndep e (insert x I)
hB : U.ExtIndep e B
hIeE : I \ {e} ⊆ M.E
hBeE : B \ {e} ⊆ M.E
hss : B \ {e} ⊆ (I ∪ B) \ {e}
hIBe : I ∪ B ⊆ insert e M.E
hIBe' : (I ∪ B) \ {e} ⊆ M.E
hImax : I ∈ maximals (fun x x_1 => x ⊆ x_1) {J | U.ExtIndep e J ∧ J ⊆ I ∪ B}
hrw : {J | U.ExtIndep e J} = {J | U.ExtIndep e J ∧ J ⊆ insert e M.E}
⊢ False