internlm/Lean-Github huggingface dataset:
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
⊢ M.Indep (insert e (B \ {e})) ∧ e ∉ B \ {e}
Tactic:
simpa [insert_eq_of_mem heB] using hB.indep
Proof state after:
no goals
Theorem: Matroid.Hyperplane.cl_insert_eq_univ
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
he : e ∈ M.E \ H
⊢ M.cl (insert e H) = M.E
Tactic:
refine' hH.ssuperset_eq_univ_of_flat (M.cl_flat _)
  ((ssubset_insert he.2).trans_subset (M.subset_cl _ _))
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
he : e ∈ M.E \ H
⊢ insert e H ⊆ M.E
Theorem: Matroid.Hyperplane.cl_insert_eq_univ
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
he : e ∈ M.E \ H
⊢ insert e H ⊆ M.E
Tactic:
rw [insert_eq, union_subset_iff, singleton_subset_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
he : e ∈ M.E \ H
⊢ e ∈ M.E ∧ H ⊆ M.E
Theorem: Matroid.Hyperplane.cl_insert_eq_univ
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
he : e ∈ M.E \ H
⊢ e ∈ M.E ∧ H ⊆ M.E
Tactic:
exact ⟨he.1, hH.subset_ground⟩
Proof state after:
no goals
Theorem: Matroid.exists_hyperplane_sep_of_not_mem_cl
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 : e ∈ M.E \ M.cl X
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis X
Proof state after:
case 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 : α
h : e ∈ M.E \ M.cl X
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H
Theorem: Matroid.exists_hyperplane_sep_of_not_mem_cl
Proof state before:
case 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 : α
h : e ∈ M.E \ M.cl X
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H
Tactic:
rw [← hI.cl_eq_cl, mem_diff, hI.indep.not_mem_cl_iff] at h
Proof state after:
case 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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H
Theorem: Matroid.exists_hyperplane_sep_of_not_mem_cl
Proof state before:
case 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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H
Tactic:
obtain ⟨B, hB, heIB⟩ := h.2.1.exists_base_superset
Proof state after:
case intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : insert e I ⊆ B
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H
Theorem: Matroid.exists_hyperplane_sep_of_not_mem_cl
Proof state before:
case intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : insert e I ⊆ B
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H
Tactic:
rw [insert_subset_iff] at heIB
Proof state after:
case intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : e ∈ B ∧ I ⊆ B
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H
Theorem: Matroid.exists_hyperplane_sep_of_not_mem_cl
Proof state before:
case intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : e ∈ B ∧ I ⊆ B
⊢ ∃ H, M.Hyperplane H ∧ X ⊆ H ∧ e ∉ H
Tactic:
refine ⟨_, hB.hyperplane_of_cl_diff_singleton heIB.1, ?_, ?_⟩
Proof state after:
case intro.intro.intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : e ∈ B ∧ I ⊆ B
⊢ X ⊆ M.cl (B \ {e})

case intro.intro.intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : e ∈ B ∧ I ⊆ B
⊢ e ∉ M.cl (B \ {e})
Theorem: Matroid.exists_hyperplane_sep_of_not_mem_cl
Proof state before:
case intro.intro.intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : e ∈ B ∧ I ⊆ B
⊢ e ∉ M.cl (B \ {e})
Tactic:
exact hB.indep.not_mem_cl_diff_of_mem heIB.1
Proof state after:
no goals
Theorem: Matroid.exists_hyperplane_sep_of_not_mem_cl
Proof state before:
case intro.intro.intro.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
I : Set α
h : e ∈ M.E ∧ M.Indep (insert e I) ∧ e ∉ I
hI : M.Basis I X
B : Set α
hB : M.Base B
heIB : e ∈ B ∧ I ⊆ B
⊢ X ⊆ M.cl (B \ {e})
Tactic:
exact hI.subset_cl.trans (M.cl_subset_cl (subset_diff_singleton heIB.2 h.2.2))
Proof state after:
no goals
Theorem: Matroid.cl_eq_sInter_hyperplanes
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 : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.cl X = ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H} ∩ M.E
Tactic:
refine' subset_antisymm (subset_inter _ (M.cl_subset_ground _)) _
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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.cl X ⊆ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}

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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H} ∩ M.E ⊆ M.cl X
Theorem: Matroid.cl_eq_sInter_hyperplanes
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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H} ∩ M.E ⊆ M.cl X
Tactic:
rintro e ⟨heH, heE⟩
Proof state after:
case refine'_2.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
e : α
heH : e ∈ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}
heE : e ∈ M.E
⊢ e ∈ M.cl X
Theorem: Matroid.cl_eq_sInter_hyperplanes
Proof state before:
case refine'_2.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
e : α
heH : e ∈ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}
heE : e ∈ M.E
⊢ e ∈ M.cl X
Tactic:
refine' by_contra fun hx ↦ _
Proof state after:
case refine'_2.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
e : α
heH : e ∈ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}
heE : e ∈ M.E
hx : e ∉ M.cl X
⊢ False
Theorem: Matroid.cl_eq_sInter_hyperplanes
Proof state before:
case refine'_2.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
e : α
heH : e ∈ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}
heE : e ∈ M.E
hx : e ∉ M.cl X
⊢ False
Tactic:
obtain ⟨H, hH, hXH, heH'⟩ := exists_hyperplane_sep_of_not_mem_cl ⟨heE, hx⟩
Proof state after:
case refine'_2.intro.intro.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
e : α
heH : e ∈ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}
heE : e ∈ M.E
hx : e ∉ M.cl X
H : Set α
hH : M.Hyperplane H
hXH : X ⊆ H
heH' : e ∉ H
⊢ False
Theorem: Matroid.cl_eq_sInter_hyperplanes
Proof state before:
case refine'_2.intro.intro.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
e : α
heH : e ∈ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}
heE : e ∈ M.E
hx : e ∉ M.cl X
H : Set α
hH : M.Hyperplane H
hXH : X ⊆ H
heH' : e ∉ H
⊢ False
Tactic:
exact heH' (heH H ⟨hH, hXH⟩)
Proof state after:
no goals
Theorem: Matroid.cl_eq_sInter_hyperplanes
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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.cl X ⊆ ⋂₀ {H | M.Hyperplane H ∧ X ⊆ H}
Tactic:
rw [subset_sInter_iff]
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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ∀ t' ∈ {H | M.Hyperplane H ∧ X ⊆ H}, M.cl X ⊆ t'
Theorem: Matroid.cl_eq_sInter_hyperplanes
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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ∀ t' ∈ {H | M.Hyperplane H ∧ X ⊆ H}, M.cl X ⊆ t'
Tactic:
rintro H ⟨hH, hXH⟩
Proof state after:
case refine'_1.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hXH : X ⊆ H
⊢ M.cl X ⊆ H
Theorem: Matroid.cl_eq_sInter_hyperplanes
Proof state before:
case refine'_1.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 : α
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hXH : X ⊆ H
⊢ M.cl X ⊆ H
Tactic:
exact hH.flat.cl_subset_of_subset hXH
Proof state after:
no goals
Theorem: Matroid.mem_cl_iff_forall_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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M.cl X ↔ ∀ (H : Set α), M.Hyperplane H → X ⊆ H → e ∈ H
Tactic:
simp_rw [← M.cl_inter_ground X,
  M.cl_eq_sInter_hyperplanes _ (inter_subset_left.trans hX), mem_inter_iff, and_iff_left he,
  mem_sInter, mem_setOf_eq, 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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ (∀ (t : Set α), M.Hyperplane t → X ∩ M.E ⊆ t → e ∈ t) ↔ ∀ (H : Set α), M.Hyperplane H → X ⊆ H → e ∈ H
Theorem: Matroid.mem_cl_iff_forall_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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ (∀ (t : Set α), M.Hyperplane t → X ∩ M.E ⊆ t → e ∈ t) ↔ ∀ (H : Set α), M.Hyperplane H → X ⊆ H → e ∈ H
Tactic:
exact ⟨fun h H hH hXH ↦ h _ hH (inter_subset_left.trans hXH),
  fun h H hH hXH ↦ h H hH (by rwa [inter_eq_self_of_subset_left hX] at hXH )⟩
Proof state after:
no goals
Theorem: Matroid.mem_cl_iff_forall_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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (H : Set α), M.Hyperplane H → X ⊆ H → e ∈ H
H : Set α
hH : M.Hyperplane H
hXH : X ∩ M.E ⊆ H
⊢ X ⊆ H
Tactic:
rwa [inter_eq_self_of_subset_left hX] at hXH
Proof state after:
no goals
Theorem: Matroid.mem_dual_cl_iff_forall_circuit
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M✶.cl X ↔ ∀ (C : Set α), M.Circuit C → e ∈ C → (X ∩ C).Nonempty
Tactic:
rw [← dual_dual M]
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M✶✶✶.cl X ↔ ∀ (C : Set α), M✶✶.Circuit C → e ∈ C → (X ∩ C).Nonempty
Theorem: Matroid.mem_dual_cl_iff_forall_circuit
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M✶✶✶.cl X ↔ ∀ (C : Set α), M✶✶.Circuit C → e ∈ C → (X ∩ C).Nonempty
Tactic:
simp_rw [← cocircuit_def, dual_dual M, mem_cl_iff_forall_hyperplane (M := M✶) hX he]
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ (∀ (H : Set α), M✶.Hyperplane H → X ⊆ H → e ∈ H) ↔ ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty
Theorem: Matroid.mem_dual_cl_iff_forall_circuit
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ (∀ (H : Set α), M✶.Hyperplane H → X ⊆ H → e ∈ H) ↔ ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty
Tactic:
refine' ⟨fun h C hC heC ↦ by_contra fun hne ↦ _, fun h H hH hXE ↦ by_contra fun he' ↦ _⟩
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (H : Set α), M✶.Hyperplane H → X ⊆ H → e ∈ H
C : Set α
hC : M✶.Cocircuit C
heC : e ∈ C
hne : ¬(X ∩ C).Nonempty
⊢ False

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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty
H : Set α
hH : M✶.Hyperplane H
hXE : X ⊆ H
he' : e ∉ H
⊢ False
Theorem: Matroid.mem_dual_cl_iff_forall_circuit
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty
H : Set α
hH : M✶.Hyperplane H
hXE : X ⊆ H
he' : e ∉ H
⊢ False
Tactic:
obtain ⟨f, hf⟩ := h _ hH.compl_cocircuit ⟨he, he'⟩
Proof state after:
case refine'_2.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✝ : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty
H : Set α
hH : M✶.Hyperplane H
hXE : X ⊆ H
he' : e ∉ H
f : α
hf : f ∈ X ∩ (M✶.E \ H)
⊢ False
Theorem: Matroid.mem_dual_cl_iff_forall_circuit
Proof state before:
case refine'_2.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✝ : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty
H : Set α
hH : M✶.Hyperplane H
hXE : X ⊆ H
he' : e ∉ H
f : α
hf : f ∈ X ∩ (M✶.E \ H)
⊢ False
Tactic:
exact hf.2.2 (hXE hf.1)
Proof state after:
no goals
Theorem: Matroid.mem_dual_cl_iff_forall_circuit
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (H : Set α), M✶.Hyperplane H → X ⊆ H → e ∈ H
C : Set α
hC : M✶.Cocircuit C
heC : e ∈ C
hne : ¬(X ∩ C).Nonempty
⊢ False
Tactic:
rw [nonempty_iff_ne_empty, not_not, ← disjoint_iff_inter_eq_empty] at hne
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (H : Set α), M✶.Hyperplane H → X ⊆ H → e ∈ H
C : Set α
hC : M✶.Cocircuit C
heC : e ∈ C
hne : Disjoint X C
⊢ False
Theorem: Matroid.mem_dual_cl_iff_forall_circuit
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (H : Set α), M✶.Hyperplane H → X ⊆ H → e ∈ H
C : Set α
hC : M✶.Cocircuit C
heC : e ∈ C
hne : Disjoint X C
⊢ False
Tactic:
exact (h _ hC.compl_hyperplane (subset_diff.mpr ⟨hX, hne⟩)).2 heC
Proof state after:
no goals
Theorem: Matroid.Flat.subset_hyperplane_of_ne_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 : α
hF : M.Flat F
h : F ≠ M.E
⊢ ∃ H, M.Hyperplane H ∧ F ⊆ H
Tactic:
obtain ⟨e, heE, heF⟩ := exists_of_ssubset (hF.subset_ground.ssubset_of_ne h)
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 : α
hF : M.Flat F
h : F ≠ M.E
e : α
heE : e ∈ M.E
heF : e ∉ F
⊢ ∃ H, M.Hyperplane H ∧ F ⊆ H
Theorem: Matroid.Flat.subset_hyperplane_of_ne_ground
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 : α
hF : M.Flat F
h : F ≠ M.E
e : α
heE : e ∈ M.E
heF : e ∉ F
⊢ ∃ H, M.Hyperplane H ∧ F ⊆ H
Tactic:
rw [← hF.cl] at heF
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 : α
hF : M.Flat F
h : F ≠ M.E
e : α
heE : e ∈ M.E
heF : e ∉ M.cl F
⊢ ∃ H, M.Hyperplane H ∧ F ⊆ H
Theorem: Matroid.Flat.subset_hyperplane_of_ne_ground
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 : α
hF : M.Flat F
h : F ≠ M.E
e : α
heE : e ∈ M.E
heF : e ∉ M.cl F
⊢ ∃ H, M.Hyperplane H ∧ F ⊆ H
Tactic:
obtain ⟨H, hH, hFH, -⟩ := exists_hyperplane_sep_of_not_mem_cl ⟨heE, heF⟩
Proof state after:
case intro.intro.intro.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 : α
hF : M.Flat F
h : F ≠ M.E
e : α
heE : e ∈ M.E
heF : e ∉ M.cl F
H : Set α
hH : M.Hyperplane H
hFH : F ⊆ H
⊢ ∃ H, M.Hyperplane H ∧ F ⊆ H
Theorem: Matroid.Flat.subset_hyperplane_of_ne_ground
Proof state before:
case intro.intro.intro.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 : α
hF : M.Flat F
h : F ≠ M.E
e : α
heE : e ∈ M.E
heF : e ∉ M.cl F
H : Set α
hH : M.Hyperplane H
hFH : F ⊆ H
⊢ ∃ H, M.Hyperplane H ∧ F ⊆ H
Tactic:
exact ⟨H, hH, hFH⟩
Proof state after:
no goals
Theorem: Matroid.subset_hyperplane_iff_cl_ne_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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ M.cl Y ≠ M.E ↔ ∃ H, M.Hyperplane H ∧ Y ⊆ H
Tactic:
refine' ⟨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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
h : M.cl Y ≠ M.E
⊢ ∃ H, M.Hyperplane H ∧ Y ⊆ H

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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ H, M.Hyperplane H ∧ Y ⊆ H) → M.cl Y ≠ M.E
Theorem: Matroid.subset_hyperplane_iff_cl_ne_ground
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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ H, M.Hyperplane H ∧ Y ⊆ H) → M.cl Y ≠ M.E
Tactic:
rintro ⟨H, hH, hYH⟩ hY
Proof state after:
case refine'_2.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 : α
hY✝ : autoParam (Y ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hYH : Y ⊆ H
hY : M.cl Y = M.E
⊢ False
Theorem: Matroid.subset_hyperplane_iff_cl_ne_ground
Proof state before:
case refine'_2.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 : α
hY✝ : autoParam (Y ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hYH : Y ⊆ H
hY : M.cl Y = M.E
⊢ False
Tactic:
refine' hH.ssubset_ground.not_subset _
Proof state after:
case refine'_2.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 : α
hY✝ : autoParam (Y ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hYH : Y ⊆ H
hY : M.cl Y = M.E
⊢ M.E ⊆ H
Theorem: Matroid.subset_hyperplane_iff_cl_ne_ground
Proof state before:
case refine'_2.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 : α
hY✝ : autoParam (Y ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hYH : Y ⊆ H
hY : M.cl Y = M.E
⊢ M.E ⊆ H
Tactic:
rw [← hH.flat.cl]
Proof state after:
case refine'_2.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 : α
hY✝ : autoParam (Y ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hYH : Y ⊆ H
hY : M.cl Y = M.E
⊢ M.E ⊆ M.cl H
Theorem: Matroid.subset_hyperplane_iff_cl_ne_ground
Proof state before:
case refine'_2.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 : α
hY✝ : autoParam (Y ⊆ M.E) _auto✝
H : Set α
hH : M.Hyperplane H
hYH : Y ⊆ H
hY : M.cl Y = M.E
⊢ M.E ⊆ M.cl H
Tactic:
exact hY.symm.trans_subset (M.cl_mono hYH)
Proof state after:
no goals
Theorem: Matroid.subset_hyperplane_iff_cl_ne_ground
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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
h : M.cl Y ≠ M.E
⊢ ∃ H, M.Hyperplane H ∧ Y ⊆ H
Tactic:
obtain ⟨H, hH, hYH⟩ := (M.cl_flat Y).subset_hyperplane_of_ne_ground h
Proof state after:
case refine'_1.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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
h : M.cl Y ≠ M.E
H : Set α
hH : M.Hyperplane H
hYH : M.cl Y ⊆ H
⊢ ∃ H, M.Hyperplane H ∧ Y ⊆ H
Theorem: Matroid.subset_hyperplane_iff_cl_ne_ground
Proof state before:
case refine'_1.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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
h : M.cl Y ≠ M.E
H : Set α
hH : M.Hyperplane H
hYH : M.cl Y ⊆ H
⊢ ∃ H, M.Hyperplane H ∧ Y ⊆ H
Tactic:
exact ⟨H, hH, (M.subset_cl Y).trans hYH⟩
Proof state after:
no goals
Theorem: Matroid.Hyperplane.inter_covBy_comm
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₁
hH₂ : M.Hyperplane H₂
⊢ H₁ ∩ H₂ ⋖[M] H₁ ↔ H₁ ∩ H₂ ⋖[M] H₂
Tactic:
obtain (rfl | hne) := eq_or_ne H₁ H₂
Proof state after:
case inl
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H' B C K : Set α
e f : α
hH₁ hH₂ : M.Hyperplane H₁
⊢ H₁ ∩ H₁ ⋖[M] H₁ ↔ H₁ ∩ H₁ ⋖[M] H₁

case inr
α : 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₁
hH₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
⊢ H₁ ∩ H₂ ⋖[M] H₁ ↔ H₁ ∩ H₂ ⋖[M] H₂
Theorem: Matroid.Hyperplane.inter_covBy_comm
Proof state before:
case inl
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H' B C K : Set α
e f : α
hH₁ hH₂ : M.Hyperplane H₁
⊢ H₁ ∩ H₁ ⋖[M] H₁ ↔ H₁ ∩ H₁ ⋖[M] H₁

case inr
α : 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₁
hH₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
⊢ H₁ ∩ H₂ ⋖[M] H₁ ↔ H₁ ∩ H₂ ⋖[M] H₂
Tactic:
simp
Proof state after:
case inr
α : 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₁
hH₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
⊢ H₁ ∩ H₂ ⋖[M] H₁ ↔ H₁ ∩ H₂ ⋖[M] H₂
Theorem: Matroid.Hyperplane.inter_covBy_comm
Proof state before:
case inr
α : 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₁
hH₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
⊢ H₁ ∩ H₂ ⋖[M] H₁ ↔ H₁ ∩ H₂ ⋖[M] H₂
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
Proof state after:
case inr.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₁ : M.Hyperplane H₁
hH₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
h : H₁ ∩ H₂ ⋖[M] H₁
⊢ H₁ ∩ H₂ ⋖[M] H₂

case inr.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₁ : M.Hyperplane H₁
hH₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
h : H₁ ∩ H₂ ⋖[M] H₂
⊢ H₁ ∩ H₂ ⋖[M] H₁