internlm/Lean-Github huggingface dataset:
Theorem: Matroid.flat_deleteElem_iff
Proof state before:
case mp.intro.intro
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
F : Set α
hF : M.Flat F
⊢ e ∉ F \ {e} ∧ (M.Flat (F \ {e}) ∨ M.Flat (insert e (F \ {e})))
Tactic:
obtain (heF | heF) := em (e ∈ F) <;> simp [heF, hF]
Proof state after:
no goals
Theorem: Matroid.flat_deleteElem_iff
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
heF : e ∉ F
hF : M.Flat (insert e F)
⊢ F = insert e F \ {e}
Tactic:
simp [heF]
Proof state after:
no goals
Theorem: Matroid.Hyperplane.cl_eq_ground_of_ssuperset
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : M.Hyperplane H
hX : H ⊂ X
hX' : autoParam (X ⊆ M.E) _auto✝
⊢ M.cl X = M.E
Tactic:
obtain ⟨e, heX, heH⟩ := exists_of_ssubset hX
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hX : H ⊂ X
hX' : autoParam (X ⊆ M.E) _auto✝
e : α
heX : e ∈ X
heH : e ∉ H
⊢ M.cl X = M.E
Theorem: Matroid.Hyperplane.cl_eq_ground_of_ssuperset
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hX : H ⊂ X
hX' : autoParam (X ⊆ M.E) _auto✝
e : α
heX : e ∈ X
heH : e ∉ H
⊢ M.cl X = M.E
Tactic:
exact (M.cl_subset_ground _).antisymm ((hH.cl_insert_eq heH (hX' heX)).symm.trans_subset
  (M.cl_subset_cl (insert_subset heX hX.subset)))
Proof state after:
no goals
Theorem: Matroid.Hyperplane.spanning_of_ssuperset
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : M.Hyperplane H
hX : H ⊂ X
hXE : autoParam (X ⊆ M.E) _auto✝
⊢ M.Spanning X
Tactic:
rw [spanning_iff_cl, hH.cl_eq_ground_of_ssuperset hX]
Proof state after:
no goals
Theorem: Matroid.Hyperplane.not_spanning
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : M.Hyperplane H
⊢ ¬M.Spanning H
Tactic:
rw [hH.flat.spanning_iff]
Proof state after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : M.Hyperplane H
⊢ ¬H = M.E
Theorem: Matroid.Hyperplane.not_spanning
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : M.Hyperplane H
⊢ ¬H = M.E
Tactic:
exact hH.ssubset_ground.ne
Proof state after:
no goals
Theorem: Matroid.Hyperplane.flat_superset_eq_ground
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : M.Hyperplane H
hF : M.Flat F
hHF : H ⊂ F
⊢ F = M.E
Tactic:
rw [← hF.cl, hH.cl_eq_ground_of_ssuperset hHF]
Proof state after:
no goals
Theorem: Matroid.hyperplane_iff_maximal_proper_flat
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ M.Hyperplane H ↔ M.Flat H ∧ H ⊂ M.E ∧ ∀ (F : Set α), H ⊂ F → M.Flat F → F = M.E
Tactic:
rw [hyperplane_iff_covBy, covBy_iff, and_iff_right M.ground_flat, and_congr_right_iff,
  and_congr_right_iff]
Proof state after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ M.Flat H →
    H ⊂ M.E →
      ((∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → F = H ∨ F = M.E) ↔ ∀ (F : Set α), H ⊂ F → M.Flat F → F = M.E)
Theorem: Matroid.hyperplane_iff_maximal_proper_flat
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ M.Flat H →
    H ⊂ M.E →
      ((∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → F = H ∨ F = M.E) ↔ ∀ (F : Set α), H ⊂ F → M.Flat F → F = M.E)
Tactic:
simp_rw [or_iff_not_imp_left, ssubset_iff_subset_ne, and_imp]
Proof state after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ M.Flat H →
    H ⊆ M.E →
      H ≠ M.E →
        ((∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → ¬F = H → F = M.E) ↔
          ∀ (F : Set α), H ⊆ F → H ≠ F → M.Flat F → F = M.E)
Theorem: Matroid.hyperplane_iff_maximal_proper_flat
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ M.Flat H →
    H ⊆ M.E →
      H ≠ M.E →
        ((∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → ¬F = H → F = M.E) ↔
          ∀ (F : Set α), H ⊆ F → H ≠ F → M.Flat F → F = M.E)
Tactic:
exact fun _ _ _  ↦
  ⟨fun h F hHF hne' hF ↦ h F hF hHF hF.subset_ground hne'.symm, fun h F hF hHF _ hne' ↦
    h F hHF (Ne.symm hne') hF⟩
Proof state after:
no goals
Theorem: Matroid.hyperplane_iff_maximal_nonspanning
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ M.Hyperplane H ↔ H ∈ maximals (fun x x_1 => x ⊆ x_1) {X | ¬M.Spanning X ∧ X ⊆ M.E}
Tactic:
simp_rw [and_comm (b := _ ⊆ _), mem_maximals_setOf_iff, and_imp]
Proof state after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ M.Hyperplane H ↔ (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
Theorem: Matroid.hyperplane_iff_maximal_nonspanning
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ M.Hyperplane H ↔ (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
Tactic:
refine' ⟨fun h ↦ ⟨⟨h.subset_ground, h.not_spanning⟩, fun X hX hX' hHX ↦ _⟩, fun h ↦ _⟩
Proof state after:
case refine'_1
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : M.Hyperplane H
X : Set α
hX : X ⊆ M.E
hX' : ¬M.Spanning X
hHX : H ⊆ X
⊢ H = X

case refine'_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
⊢ M.Hyperplane H
Theorem: Matroid.hyperplane_iff_maximal_nonspanning
Proof state before:
case refine'_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
⊢ M.Hyperplane H
Tactic:
rw [hyperplane_iff_covBy, covBy_iff, and_iff_right M.ground_flat,
  flat_iff_ssubset_cl_insert_forall h.1.1]
Proof state after:
case refine'_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
⊢ (∀ e ∈ M.E \ H, M.cl H ⊂ M.cl (insert e H)) ∧ H ⊂ M.E ∧ ∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → F = H ∨ F = M.E
Theorem: Matroid.hyperplane_iff_maximal_nonspanning
Proof state before:
case refine'_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
⊢ (∀ e ∈ M.E \ H, M.cl H ⊂ M.cl (insert e H)) ∧ H ⊂ M.E ∧ ∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → F = H ∨ F = M.E
Tactic:
refine'
  ⟨fun e he ↦ _, h.1.1.ssubset_of_ne (by rintro rfl; exact h.1.2 M.ground_spanning),
    fun F hF hHF hFE ↦ or_iff_not_imp_right.mpr fun hFE' ↦ _⟩
Proof state after:
case refine'_2.refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
⊢ M.cl H ⊂ M.cl (insert e H)

case refine'_2.refine'_2
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
F : Set α
hF : M.Flat F
hHF : H ⊆ F
hFE : F ⊆ M.E
hFE' : ¬F = M.E
⊢ F = H
Theorem: Matroid.hyperplane_iff_maximal_nonspanning
Proof state before:
case refine'_2.refine'_2
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
F : Set α
hF : M.Flat F
hHF : H ⊆ F
hFE : F ⊆ M.E
hFE' : ¬F = M.E
⊢ F = H
Tactic:
have h' := h.2 hFE
Proof state after:
case refine'_2.refine'_2
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
F : Set α
hF : M.Flat F
hHF : H ⊆ F
hFE : F ⊆ M.E
hFE' : ¬F = M.E
h' : ¬M.Spanning F → H ⊆ F → H = F
⊢ F = H
Theorem: Matroid.hyperplane_iff_maximal_nonspanning
Proof state before:
case refine'_2.refine'_2
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
F : Set α
hF : M.Flat F
hHF : H ⊆ F
hFE : F ⊆ M.E
hFE' : ¬F = M.E
h' : ¬M.Spanning F → H ⊆ F → H = F
⊢ F = H
Tactic:
rw [hF.spanning_iff] at h'
Proof state after:
case refine'_2.refine'_2
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
F : Set α
hF : M.Flat F
hHF : H ⊆ F
hFE : F ⊆ M.E
hFE' : ¬F = M.E
h' : ¬F = M.E → H ⊆ F → H = F
⊢ F = H
Theorem: Matroid.hyperplane_iff_maximal_nonspanning
Proof state before:
case refine'_2.refine'_2
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
F : Set α
hF : M.Flat F
hHF : H ⊆ F
hFE : F ⊆ M.E
hFE' : ¬F = M.E
h' : ¬F = M.E → H ⊆ F → H = F
⊢ F = H
Tactic:
rw [h' hFE' hHF]
Proof state after:
no goals
Theorem: Matroid.hyperplane_iff_maximal_nonspanning
Proof state before:
case refine'_1
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : M.Hyperplane H
X : Set α
hX : X ⊆ M.E
hX' : ¬M.Spanning X
hHX : H ⊆ X
⊢ H = X
Tactic:
exact by_contra fun hne ↦ hX' (h.spanning_of_ssuperset (hHX.ssubset_of_ne hne))
Proof state after:
no goals
Theorem: Matroid.hyperplane_iff_maximal_nonspanning
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
⊢ H ≠ M.E
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H₁ H₂ H' B C K : Set α
e f : α
h : (M.E ⊆ M.E ∧ ¬M.Spanning M.E) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → M.E ⊆ y → M.E = y
⊢ False
Theorem: Matroid.hyperplane_iff_maximal_nonspanning
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H₁ H₂ H' B C K : Set α
e f : α
h : (M.E ⊆ M.E ∧ ¬M.Spanning M.E) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → M.E ⊆ y → M.E = y
⊢ False
Tactic:
exact h.1.2 M.ground_spanning
Proof state after:
no goals
Theorem: Matroid.hyperplane_iff_maximal_nonspanning
Proof state before:
case refine'_2.refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
⊢ M.cl H ⊂ M.cl (insert e H)
Tactic:
have h' := h.2 (insert_subset he.1 h.1.1)
Proof state after:
case refine'_2.refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : ¬M.Spanning (insert e H) → H ⊆ insert e H → H = insert e H
⊢ M.cl H ⊂ M.cl (insert e H)
Theorem: Matroid.hyperplane_iff_maximal_nonspanning
Proof state before:
case refine'_2.refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : ¬M.Spanning (insert e H) → H ⊆ insert e H → H = insert e H
⊢ M.cl H ⊂ M.cl (insert e H)
Tactic:
simp only [subset_insert, forall_true_left, @eq_comm _ H, insert_eq_self, iff_false_intro he.2,
  imp_false, Classical.not_not, spanning_iff_cl]  at h'
Proof state after:
case refine'_2.refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : M.Spanning (insert e H)
⊢ M.cl H ⊂ M.cl (insert e H)
Theorem: Matroid.hyperplane_iff_maximal_nonspanning
Proof state before:
case refine'_2.refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : M.Spanning (insert e H)
⊢ M.cl H ⊂ M.cl (insert e H)
Tactic:
rw [spanning_iff_cl] at h'
Proof state after:
case refine'_2.refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : M.cl (insert e H) = M.E
⊢ M.cl H ⊂ M.cl (insert e H)
Theorem: Matroid.hyperplane_iff_maximal_nonspanning
Proof state before:
case refine'_2.refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : M.cl (insert e H) = M.E
⊢ M.cl H ⊂ M.cl (insert e H)
Tactic:
rw [h', ← not_spanning_iff_cl h.1.1]
Proof state after:
case refine'_2.refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : M.cl (insert e H) = M.E
⊢ ¬M.Spanning H
Theorem: Matroid.hyperplane_iff_maximal_nonspanning
Proof state before:
case refine'_2.refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : M.cl (insert e H) = M.E
⊢ ¬M.Spanning H
Tactic:
exact h.1.2
Proof state after:
no goals
Theorem: Matroid.compl_cocircuit_iff_hyperplane
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
⊢ M.Cocircuit (M.E \ H) ↔ M.Hyperplane H
Tactic:
simp_rw [cocircuit_iff_mem_minimals_compl_nonspanning, hyperplane_iff_maximal_nonspanning,
  (and_comm (b := _ ⊆ _)), mem_minimals_setOf_iff, mem_maximals_setOf_iff,
  diff_diff_cancel_left hH, and_iff_right hH, subset_diff, and_imp, and_congr_right_iff]
Proof state after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
⊢ ¬M.Spanning H →
    ((∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y) ↔
      ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y)
Theorem: Matroid.compl_cocircuit_iff_hyperplane
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
⊢ ¬M.Spanning H →
    ((∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y) ↔
      ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y)
Tactic:
refine' fun _ ↦ ⟨fun h X hXE hX hHX ↦ _, fun h X hX hXE hXH ↦ _⟩
Proof state after:
case refine'_1
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ H = X

case refine'_2
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXE : X ⊆ M.E
hXH : Disjoint X H
⊢ M.E \ H = X
Theorem: Matroid.compl_cocircuit_iff_hyperplane
Proof state before:
case refine'_2
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXE : X ⊆ M.E
hXH : Disjoint X H
⊢ M.E \ H = X
Tactic:
rw [h diff_subset hX, diff_diff_cancel_left hXE]
Proof state after:
case refine'_2
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXE : X ⊆ M.E
hXH : Disjoint X H
⊢ H ⊆ M.E \ X
Theorem: Matroid.compl_cocircuit_iff_hyperplane
Proof state before:
case refine'_2
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXE : X ⊆ M.E
hXH : Disjoint X H
⊢ H ⊆ M.E \ X
Tactic:
rw [subset_diff]
Proof state after:
case refine'_2
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXE : X ⊆ M.E
hXH : Disjoint X H
⊢ H ⊆ M.E ∧ Disjoint H X
Theorem: Matroid.compl_cocircuit_iff_hyperplane
Proof state before:
case refine'_2
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXE : X ⊆ M.E
hXH : Disjoint X H
⊢ H ⊆ M.E ∧ Disjoint H X
Tactic:
exact ⟨hH, hXH.symm⟩
Proof state after:
no goals
Theorem: Matroid.compl_cocircuit_iff_hyperplane
Proof state before:
case refine'_1
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ H = X
Tactic:
rw [← diff_diff_cancel_left hH, ← diff_diff_cancel_left hXE,
  h (y := M.E \ X) (by rwa [diff_diff_cancel_left hXE]) diff_subset]
Proof state after:
case refine'_1
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ Disjoint (M.E \ X) H
Theorem: Matroid.compl_cocircuit_iff_hyperplane
Proof state before:
case refine'_1
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ Disjoint (M.E \ X) H
Tactic:
rw [← subset_compl_iff_disjoint_left, diff_eq, compl_inter, compl_compl]
Proof state after:
case refine'_1
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ H ⊆ M.Eᶜ ∪ X
Theorem: Matroid.compl_cocircuit_iff_hyperplane
Proof state before:
case refine'_1
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ H ⊆ M.Eᶜ ∪ X
Tactic:
exact hHX.trans subset_union_right
Proof state after:
no goals
Theorem: Matroid.compl_cocircuit_iff_hyperplane
Proof state before:
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ ¬M.Spanning (M.E \ (M.E \ X))
Tactic:
rwa [diff_diff_cancel_left hXE]
Proof state after:
no goals
Theorem: Matroid.compl_hyperplane_iff_cocircuit
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h : autoParam (K ⊆ M.E) _auto✝
⊢ M.Hyperplane (M.E \ K) ↔ M.Cocircuit K
Tactic:
rw [← compl_cocircuit_iff_hyperplane, diff_diff_right, diff_self, empty_union, inter_comm,
  inter_eq_left.mpr h]
Proof state after:
no goals
Theorem: Matroid.Hyperplane.inter_ssubset_left_of_ne
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h₁ : M.Hyperplane H₁
h₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
⊢ H₁ ∩ H₂ ⊂ H₁
Tactic:
refine inter_subset_left.ssubset_of_ne fun h_eq ↦ hne <| h₁.eq_of_subset h₂ ?_
Proof state after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h₁ : M.Hyperplane H₁
h₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
h_eq : H₁ ∩ H₂ = H₁
⊢ H₁ ⊆ H₂
Theorem: Matroid.Hyperplane.inter_ssubset_left_of_ne
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h₁ : M.Hyperplane H₁
h₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
h_eq : H₁ ∩ H₂ = H₁
⊢ H₁ ⊆ H₂
Tactic:
rw [← h_eq]
Proof state after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h₁ : M.Hyperplane H₁
h₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
h_eq : H₁ ∩ H₂ = H₁
⊢ H₁ ∩ H₂ ⊆ H₂
Theorem: Matroid.Hyperplane.inter_ssubset_left_of_ne
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h₁ : M.Hyperplane H₁
h₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
h_eq : H₁ ∩ H₂ = H₁
⊢ H₁ ∩ H₂ ⊆ H₂
Tactic:
exact inter_subset_right
Proof state after:
no goals
Theorem: Matroid.Hyperplane.inter_ssubset_right_of_ne
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h₁ : M.Hyperplane H₁
h₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
⊢ H₁ ∩ H₂ ⊂ H₂
Tactic:
rw [inter_comm]
Proof state after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h₁ : M.Hyperplane H₁
h₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
⊢ H₂ ∩ H₁ ⊂ H₂
Theorem: Matroid.Hyperplane.inter_ssubset_right_of_ne
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h₁ : M.Hyperplane H₁
h₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
⊢ H₂ ∩ H₁ ⊂ H₂
Tactic:
exact h₂.inter_ssubset_left_of_ne h₁ hne.symm
Proof state after:
no goals
Theorem: Matroid.Base.hyperplane_of_cl_diff_singleton
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hB : M.Base B
heB : e ∈ B
⊢ M.Hyperplane (M.cl (B \ {e}))
Tactic:
rw [hyperplane_iff_covBy, Flat.covBy_iff_eq_cl_insert (M.cl_flat _)]
Proof state after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hB : M.Base B
heB : e ∈ B
⊢ ∃ e_1 ∈ M.E \ M.cl (B \ {e}), M.E = M.cl (insert e_1 (M.cl (B \ {e})))
Theorem: Matroid.Base.hyperplane_of_cl_diff_singleton
Proof state before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hB : M.Base B
heB : e ∈ B
⊢ ∃ e_1 ∈ M.E \ M.cl (B \ {e}), M.E = M.cl (insert e_1 (M.cl (B \ {e})))
Tactic:
refine' ⟨e, ⟨hB.subset_ground heB, _⟩, _⟩
Proof state after:
case refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hB : M.Base B
heB : e ∈ B
⊢ e ∉ M.cl (B \ {e})

case refine'_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hB : M.Base B
heB : e ∈ B
⊢ M.E = M.cl (insert e (M.cl (B \ {e})))
Theorem: Matroid.Base.hyperplane_of_cl_diff_singleton
Proof state before:
case refine'_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hB : M.Base B
heB : e ∈ B
⊢ M.E = M.cl (insert e (M.cl (B \ {e})))
Tactic:
simpa [insert_eq_of_mem heB] using hB.cl_eq.symm
Proof state after:
no goals
Theorem: Matroid.Base.hyperplane_of_cl_diff_singleton
Proof state before:
case refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hB : M.Base B
heB : e ∈ B
⊢ e ∉ M.cl (B \ {e})
Tactic:
rw [(hB.indep.diff {e}).not_mem_cl_iff (hB.subset_ground heB)]
Proof state after:
case refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hB : M.Base B
heB : e ∈ B
⊢ M.Indep (insert e (B \ {e})) ∧ e ∉ B \ {e}