internlm/Lean-Github huggingface dataset:
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})
heX : e ∈ X
⊢ ¬M.cl I ∉ U
Tactic:
rw [extIndep_iff_of_not_mem heI] at hI
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 : M.Indep 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
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 : M.Indep 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
Tactic:
simpa [heI, hI] using (h e heI heX).2
Proof state after:
no goals
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
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
Tactic:
rw [extIndep_iff_of_mem heI] at hI
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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
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.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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
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:
obtain (hcl | hcl) := em (M.cl (X \ {e}) ∈ U)
Proof state after:
case refine_1.inl.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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
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
hcl : M.cl (X \ {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

case refine_1.inl.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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
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
hcl : M.cl (X \ {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.inl.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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
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
hcl : M.cl (X \ {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:
simp only [heI, hcl, iff_false, not_true_eq_false, not_false_eq_true, implies_true, and_true,
  and_false, or_false]
Proof state after:
case refine_1.inl.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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
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
hcl : M.cl (X \ {e}) ∉ U
⊢ M.cl (I \ {e}) = M.cl (X \ {e})
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case refine_1.inl.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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
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
hcl : M.cl (X \ {e}) ∉ U
⊢ M.cl (I \ {e}) = M.cl (X \ {e})
Tactic:
refine (M.cl_subset_cl hss).antisymm (M.cl_subset_cl_of_subset_cl fun x hx ↦
  by_contra fun hxcl ↦ hcl ?_)
Proof state after:
case refine_1.inl.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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
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
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
⊢ M.cl (X \ {e}) ∈ U
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case refine_1.inl.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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
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
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
⊢ M.cl (X \ {e}) ∈ U
Tactic:
have hxI : x ∉ I := by simpa [hx.2] using not_mem_of_mem_diff_cl ⟨(hX' hx), hxcl⟩
Proof state after:
case refine_1.inl.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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
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
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
hxI : x ∉ I
⊢ M.cl (X \ {e}) ∈ U
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case refine_1.inl.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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
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
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
hxI : x ∉ I
⊢ M.cl (X \ {e}) ∈ U
Tactic:
replace h := show M.cl (insert x (I \ {e})) ∈ U by
  simpa [hxI, hx.1, heI, ← insert_diff_singleton_comm hx.2, hI.1.insert_indep_iff,
    hX' hx, hxcl] using h x
Proof state after:
case refine_1.inl.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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
hxI : x ∉ I
h : M.cl (insert x (I \ {e})) ∈ U
⊢ M.cl (X \ {e}) ∈ U
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case refine_1.inl.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 \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
hxI : x ∉ I
h : M.cl (insert x (I \ {e})) ∈ U
⊢ M.cl (X \ {e}) ∈ U
Tactic:
exact U.cl_superset_mem' h (insert_subset hx hss)
Proof state after:
no goals
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case refine_1.inl.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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
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
hcl : M.cl (X \ {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:
simp only [heI, hcl, not_true_eq_false, imp_false, and_self, and_true]
Proof state after:
case refine_1.inl.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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
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
hcl : M.cl (X \ {e}) ∈ U
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ e ∉ X ∨ (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e}))
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case refine_1.inl.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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
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
hcl : M.cl (X \ {e}) ∈ U
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ e ∉ X ∨ (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e}))
Tactic:
refine .inr <| U.covBy_of_maximal_cl (M.cl_subset_cl hss) hcl hI.2 fun x ⟨hx, hxcl⟩ ↦ ?_
Proof state after:
case refine_1.inl.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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
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
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
⊢ M.cl (insert x (I \ {e})) ∈ U
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case refine_1.inl.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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
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
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
⊢ M.cl (insert x (I \ {e})) ∈ U
Tactic:
specialize h x
Proof state after:
case refine_1.inl.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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {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 (insert x (I \ {e})) ∈ U
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case refine_1.inl.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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {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 (insert x (I \ {e})) ∈ U
Tactic:
have hxI : x ∉ I := by simpa [hx.2] using not_mem_of_mem_diff_cl ⟨hX' hx, hxcl⟩
Proof state after:
case refine_1.inl.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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {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)
hxI : x ∉ I
⊢ M.cl (insert x (I \ {e})) ∈ U
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case refine_1.inl.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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {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)
hxI : x ∉ I
⊢ M.cl (insert x (I \ {e})) ∈ U
Tactic:
rw [← insert_diff_singleton_comm hx.2, hI.1.insert_indep_iff] at h
Proof state after:
case refine_1.inl.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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
h :
  x ∉ I →
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (x ∈ M.E \ M.cl (I \ {e}) ∨ x ∈ I \ {e} → e ∈ insert x I → M.cl (insert x (I \ {e})) ∈ U)
hxI : x ∉ I
⊢ M.cl (insert x (I \ {e})) ∈ U
Theorem: Matroid.ModularCut.maximal_extIndep_iff
Proof state before:
case refine_1.inl.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 : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
h :
  x ∉ I →
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (x ∈ M.E \ M.cl (I \ {e}) ∨ x ∈ I \ {e} → e ∈ insert x I → M.cl (insert x (I \ {e})) ∈ U)
hxI : x ∉ I
⊢ M.cl (insert x (I \ {e})) ∈ U
Tactic:
exact (h hxI hx.1).2 (.inl ⟨hX' hx, hxcl⟩) (.inr heI)
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
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {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)
⊢ x ∉ I
Tactic:
simpa [hx.2] using not_mem_of_mem_diff_cl ⟨hX' hx, hxcl⟩
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 :
  ∀ 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
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
⊢ x ∉ I
Tactic:
simpa [hx.2] using not_mem_of_mem_diff_cl ⟨(hX' hx), hxcl⟩
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 :
  ∀ 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
hcl : M.cl (X \ {e}) ∉ U
x : α
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
hxI : x ∉ I
⊢ M.cl (insert x (I \ {e})) ∈ U
Tactic:
simpa [hxI, hx.1, heI, ← insert_diff_singleton_comm hx.2, hI.1.insert_indep_iff,
  hX' hx, hxcl] using h x
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
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 (X \ {e}) = M.cl (I \ {e})
Tactic:
refine (M.cl_subset_cl hss).antisymm' (M.cl_subset_cl_of_subset_cl fun x hx ↦ ?_)
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
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)
x : α
hx : x ∈ X \ {e}
⊢ x ∈ M.cl (I \ {e})
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
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)
x : α
hx : x ∈ X \ {e}
⊢ x ∈ M.cl (I \ {e})
Tactic:
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]
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
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)
x : α
hx : x ∈ X \ {e}
⊢ M.Indep (insert x I) → x ∈ I
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
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)
x : α
hx : x ∈ X \ {e}
⊢ M.Indep (insert x I) → x ∈ I
Tactic:
exact fun h' ↦ by_contra fun hxI ↦ by simp [(h x hxI hx.1).1 h'] at hx
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
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)
x : α
hx : x ∈ X \ {e}
h' : M.Indep (insert x I)
hxI : x ∉ I
⊢ False
Tactic:
simp [(h x hxI hx.1).1 h'] at hx
Proof state after:
no goals
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 : 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:
have hxe : x ≠ e := by rintro rfl; contradiction
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
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 : 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
hxe : x ≠ e
⊢ False
Tactic:
rw [extIndep_iff_of_mem heI] at hI
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 : U.ExtIndep e (insert x I)
heI : e ∈ I
hxe : x ≠ e
⊢ False