internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Flat.exists_unique_flat_of_not_mem
Proof state before:
case h.refine'_1.right
α : 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₀
he : e ∈ M.E \ F₀
⊢ ∃ e_1 ∈ M.E \ F₀, M.cl (insert e F₀) = M.cl (insert e_1 F₀)
Tactic:
use e, he
Proof state after:
no goals
Theorem: Matroid.Flat.exists_unique_flat_of_not_mem
Proof state before:
case h.refine'_1.left
α : 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₀
he : e ∈ M.E \ F₀
⊢ e ∈ M.cl (insert e F₀)
Tactic:
exact (M.inter_ground_subset_cl (insert e F₀)) ⟨mem_insert _ _, he.1⟩
Proof state after:
no goals
Theorem: Matroid.CovBy.eq_cl_union_of_covBy_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₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
⊢ F = M.cl (F₀ ∪ F₁)
Tactic:
refine subset_antisymm ?_ (h₁.flat_right.cl_subset_of_subset (union_subset h₀.subset h₁.subset))
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₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
⊢ F ⊆ M.cl (F₀ ∪ F₁)
Theorem: Matroid.CovBy.eq_cl_union_of_covBy_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₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
⊢ F ⊆ M.cl (F₀ ∪ F₁)
Tactic:
have hnss : ¬ (F₀ ⊆ F₁) :=
  fun hss ↦ hne.symm <| h₀.eq_of_subset_of_ssubset h₁.flat_left hss h₁.ssubset
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₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
hnss : ¬F₀ ⊆ F₁
⊢ F ⊆ M.cl (F₀ ∪ F₁)
Theorem: Matroid.CovBy.eq_cl_union_of_covBy_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₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
hnss : ¬F₀ ⊆ F₁
⊢ F ⊆ M.cl (F₀ ∪ F₁)
Tactic:
obtain ⟨e, he₀, he₁⟩ := not_subset.1 hnss
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 : α
h₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
hnss : ¬F₀ ⊆ F₁
e : α
he₀ : e ∈ F₀
he₁ : e ∉ F₁
⊢ F ⊆ M.cl (F₀ ∪ F₁)
Theorem: Matroid.CovBy.eq_cl_union_of_covBy_of_ne
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 : α
h₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
hnss : ¬F₀ ⊆ F₁
e : α
he₀ : e ∈ F₀
he₁ : e ∉ F₁
⊢ F ⊆ M.cl (F₀ ∪ F₁)
Tactic:
obtain rfl := h₁.cl_insert_eq ⟨h₀.subset he₀, he₁⟩
Proof state after:
case 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 : α
hne : F₀ ≠ F₁
hnss : ¬F₀ ⊆ F₁
e : α
he₀ : e ∈ F₀
he₁ : e ∉ F₁
h₀ : F₀ ⋖[M] M.cl (insert e F₁)
h₁ : F₁ ⋖[M] M.cl (insert e F₁)
⊢ M.cl (insert e F₁) ⊆ M.cl (F₀ ∪ F₁)
Theorem: Matroid.CovBy.eq_cl_union_of_covBy_of_ne
Proof state before:
case 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 : α
hne : F₀ ≠ F₁
hnss : ¬F₀ ⊆ F₁
e : α
he₀ : e ∈ F₀
he₁ : e ∉ F₁
h₀ : F₀ ⋖[M] M.cl (insert e F₁)
h₁ : F₁ ⋖[M] M.cl (insert e F₁)
⊢ M.cl (insert e F₁) ⊆ M.cl (F₀ ∪ F₁)
Tactic:
exact M.cl_subset_cl (insert_subset (Or.inl he₀) subset_union_right)
Proof state after:
no goals
Theorem: Matroid.Flat.exists_left_covBy_of_ssubset
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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
⊢ ∃ F, (F₀ ⋖[M] F) ∧ F ⊆ F₁
Tactic:
obtain ⟨e, he⟩ := exists_of_ssubset hss
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
e : α
he : e ∈ F₁ ∧ e ∉ F₀
⊢ ∃ F, (F₀ ⋖[M] F) ∧ F ⊆ F₁
Theorem: Matroid.Flat.exists_left_covBy_of_ssubset
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
e : α
he : e ∈ F₁ ∧ e ∉ F₀
⊢ ∃ F, (F₀ ⋖[M] F) ∧ F ⊆ F₁
Tactic:
exact ⟨_, hF₀.covBy_cl_insert he.2 (hF₁.subset_ground he.1),
  hF₁.cl_subset_of_subset <| insert_subset he.1 hss.subset⟩
Proof state after:
no goals
Theorem: Matroid.Flat.exists_covBy_right_of_ssubset
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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
⊢ ∃ F, F₀ ⊆ F ∧ (F ⋖[M] F₁)
Tactic:
obtain ⟨I, J, hI, hJ, hIJ⟩ := M.exists_basis_subset_basis hss.subset
Proof state after:
case 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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
I J : Set α
hI : M.Basis I F₀
hJ : M.Basis J F₁
hIJ : I ⊆ J
⊢ ∃ F, F₀ ⊆ F ∧ (F ⋖[M] F₁)
Theorem: Matroid.Flat.exists_covBy_right_of_ssubset
Proof state before:
case 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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
I J : Set α
hI : M.Basis I F₀
hJ : M.Basis J F₁
hIJ : I ⊆ J
⊢ ∃ F, F₀ ⊆ F ∧ (F ⋖[M] F₁)
Tactic:
have hssu : I ⊂ J := hIJ.ssubset_of_ne <| by
  rintro rfl
  rw [hF₀.eq_cl_of_basis hI, hF₁.eq_cl_of_basis hJ] at hss
  exact hss.ne rfl
Proof state after:
case 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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
I J : Set α
hI : M.Basis I F₀
hJ : M.Basis J F₁
hIJ : I ⊆ J
hssu : I ⊂ J
⊢ ∃ F, F₀ ⊆ F ∧ (F ⋖[M] F₁)
Theorem: Matroid.Flat.exists_covBy_right_of_ssubset
Proof state before:
case 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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
I J : Set α
hI : M.Basis I F₀
hJ : M.Basis J F₁
hIJ : I ⊆ J
hssu : I ⊂ J
⊢ ∃ F, F₀ ⊆ F ∧ (F ⋖[M] F₁)
Tactic:
obtain ⟨e, heJ, heI⟩ := exists_of_ssubset hssu
Proof state after:
case intro.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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
I J : Set α
hI : M.Basis I F₀
hJ : M.Basis J F₁
hIJ : I ⊆ J
hssu : I ⊂ J
e : α
heJ : e ∈ J
heI : e ∉ I
⊢ ∃ F, F₀ ⊆ F ∧ (F ⋖[M] F₁)
Theorem: Matroid.Flat.exists_covBy_right_of_ssubset
Proof state before:
case intro.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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
I J : Set α
hI : M.Basis I F₀
hJ : M.Basis J F₁
hIJ : I ⊆ J
hssu : I ⊂ J
e : α
heJ : e ∈ J
heI : e ∉ I
⊢ ∃ F, F₀ ⊆ F ∧ (F ⋖[M] F₁)
Tactic:
refine ⟨M.cl (J \ {e}), hI.subset_cl.trans (M.cl_subset_cl (subset_diff_singleton hIJ heI)), ?_⟩
Proof state after:
case intro.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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
I J : Set α
hI : M.Basis I F₀
hJ : M.Basis J F₁
hIJ : I ⊆ J
hssu : I ⊂ J
e : α
heJ : e ∈ J
heI : e ∉ I
⊢ M.cl (J \ {e}) ⋖[M] F₁
Theorem: Matroid.Flat.exists_covBy_right_of_ssubset
Proof state before:
case intro.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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
I J : Set α
hI : M.Basis I F₀
hJ : M.Basis J F₁
hIJ : I ⊆ J
hssu : I ⊂ J
e : α
heJ : e ∈ J
heI : e ∉ I
⊢ M.cl (J \ {e}) ⋖[M] F₁
Tactic:
convert (M.cl_flat (J \ {e})).covBy_cl_insert ?_ (hJ.indep.subset_ground heJ)
Proof state after:
case h.e'_4
α : 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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
I J : Set α
hI : M.Basis I F₀
hJ : M.Basis J F₁
hIJ : I ⊆ J
hssu : I ⊂ J
e : α
heJ : e ∈ J
heI : e ∉ I
⊢ F₁ = M.cl (insert e (M.cl (J \ {e})))

case intro.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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
I J : Set α
hI : M.Basis I F₀
hJ : M.Basis J F₁
hIJ : I ⊆ J
hssu : I ⊂ J
e : α
heJ : e ∈ J
heI : e ∉ I
⊢ e ∉ M.cl (J \ {e})
Theorem: Matroid.Flat.exists_covBy_right_of_ssubset
Proof state before:
case intro.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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
I J : Set α
hI : M.Basis I F₀
hJ : M.Basis J F₁
hIJ : I ⊆ J
hssu : I ⊂ J
e : α
heJ : e ∈ J
heI : e ∉ I
⊢ e ∉ M.cl (J \ {e})
Tactic:
exact hJ.indep.not_mem_cl_diff_of_mem heJ
Proof state after:
no goals
Theorem: Matroid.Flat.exists_covBy_right_of_ssubset
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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
I J : Set α
hI : M.Basis I F₀
hJ : M.Basis J F₁
hIJ : I ⊆ J
⊢ I ≠ J
Tactic:
rintro rfl
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
I : Set α
hI : M.Basis I F₀
hJ : M.Basis I F₁
hIJ : I ⊆ I
⊢ False
Theorem: Matroid.Flat.exists_covBy_right_of_ssubset
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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
I : Set α
hI : M.Basis I F₀
hJ : M.Basis I F₁
hIJ : I ⊆ I
⊢ False
Tactic:
rw [hF₀.eq_cl_of_basis hI, hF₁.eq_cl_of_basis hJ] at hss
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
I : Set α
hss : M.cl I ⊂ M.cl I
hI : M.Basis I F₀
hJ : M.Basis I F₁
hIJ : I ⊆ I
⊢ False
Theorem: Matroid.Flat.exists_covBy_right_of_ssubset
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₀
hF₁ : M.Flat F₁
I : Set α
hss : M.cl I ⊂ M.cl I
hI : M.Basis I F₀
hJ : M.Basis I F₁
hIJ : I ⊆ I
⊢ False
Tactic:
exact hss.ne rfl
Proof state after:
no goals
Theorem: Matroid.Flat.exists_covBy_right_of_ssubset
Proof state before:
case h.e'_4
α : 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₀
hF₁ : M.Flat F₁
hss : F₀ ⊂ F₁
I J : Set α
hI : M.Basis I F₀
hJ : M.Basis J F₁
hIJ : I ⊆ J
hssu : I ⊂ J
e : α
heJ : e ∈ J
heI : e ∉ I
⊢ F₁ = M.cl (insert e (M.cl (J \ {e})))
Tactic:
rw [cl_insert_cl_eq_cl_insert, insert_diff_singleton, insert_eq_of_mem heJ,
  hF₁.eq_cl_of_basis hJ]
Proof state after:
no goals
Theorem: Matroid.CovBy.covBy_cl_union_of_inter_covBy
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₀ : F₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
⊢ F₀ ⋖[M] M.cl (F₀ ∪ F₁)
Tactic:
obtain ⟨e₀, -, h₀'⟩ := h₀.exists_eq_cl_insert
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 : α
h₀ : F₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
⊢ F₀ ⋖[M] M.cl (F₀ ∪ F₁)
Theorem: Matroid.CovBy.covBy_cl_union_of_inter_covBy
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 : α
h₀ : F₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
⊢ F₀ ⋖[M] M.cl (F₀ ∪ F₁)
Tactic:
obtain ⟨e₁, he₁, h₁'⟩ := h₁.exists_eq_cl_insert
Proof state after:
case 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 : α
h₀ : F₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
e₁ : α
he₁ : e₁ ∈ F₁ \ (F₀ ∩ F₁)
h₁' : M.cl (insert e₁ (F₀ ∩ F₁)) = F₁
⊢ F₀ ⋖[M] M.cl (F₀ ∪ F₁)
Theorem: Matroid.CovBy.covBy_cl_union_of_inter_covBy
Proof state before:
case 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 : α
h₀ : F₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
e₁ : α
he₁ : e₁ ∈ F₁ \ (F₀ ∩ F₁)
h₁' : M.cl (insert e₁ (F₀ ∩ F₁)) = F₁
⊢ F₀ ⋖[M] M.cl (F₀ ∪ F₁)
Tactic:
nth_rw 2 [← h₀', ← h₁']
Proof state after:
case 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 : α
h₀ : F₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
e₁ : α
he₁ : e₁ ∈ F₁ \ (F₀ ∩ F₁)
h₁' : M.cl (insert e₁ (F₀ ∩ F₁)) = F₁
⊢ F₀ ⋖[M] M.cl (M.cl (insert e₀ (F₀ ∩ F₁)) ∪ M.cl (insert e₁ (F₀ ∩ F₁)))
Theorem: Matroid.CovBy.covBy_cl_union_of_inter_covBy
Proof state before:
case 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 : α
h₀ : F₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
e₁ : α
he₁ : e₁ ∈ F₁ \ (F₀ ∩ F₁)
h₁' : M.cl (insert e₁ (F₀ ∩ F₁)) = F₁
⊢ F₀ ⋖[M] M.cl (M.cl (insert e₀ (F₀ ∩ F₁)) ∪ M.cl (insert e₁ (F₀ ∩ F₁)))
Tactic:
rw [cl_cl_union_cl_eq_cl_union, ← singleton_union, ← singleton_union,
  ← union_union_distrib_right, union_comm {e₀}, union_assoc, singleton_union, singleton_union,
  ← M.cl_insert_cl_eq_cl_insert, h₀']
Proof state after:
case 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 : α
h₀ : F₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
e₁ : α
he₁ : e₁ ∈ F₁ \ (F₀ ∩ F₁)
h₁' : M.cl (insert e₁ (F₀ ∩ F₁)) = F₁
⊢ F₀ ⋖[M] M.cl (insert e₁ F₀)
Theorem: Matroid.CovBy.covBy_cl_union_of_inter_covBy
Proof state before:
case 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 : α
h₀ : F₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
e₁ : α
he₁ : e₁ ∈ F₁ \ (F₀ ∩ F₁)
h₁' : M.cl (insert e₁ (F₀ ∩ F₁)) = F₁
⊢ F₀ ⋖[M] M.cl (insert e₁ F₀)
Tactic:
exact h₀.flat_right.covBy_cl_insert (fun h ↦ he₁.2 ⟨h, he₁.1⟩) (h₁.flat_right.subset_ground he₁.1)
Proof state after:
no goals
Theorem: Matroid.Flat.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two
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₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
have h0le := hF₀.one_le_relRank_of_ssubset 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Theorem: Matroid.Flat.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two
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₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
have h1le := hF.one_le_relRank_of_ssubset 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Theorem: Matroid.Flat.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two
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₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
rw [← M.relRank_add_of_subset_of_subset h₀.subset h₁.subset] at 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Theorem: Matroid.Flat.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two
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₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
have h0top : M.relRank F₀ F ≠ ⊤ := by
  intro h'; rw [h'] at h; norm_cast at 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Theorem: Matroid.Flat.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two
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₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
have h1top : M.relRank F F₁ ≠ ⊤ := by
  intro h'; rw [h', add_top] at h; norm_cast at 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Theorem: Matroid.Flat.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two
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₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
have hle1 := WithTop.le_of_add_le_add_left h0top <| h.le.trans (add_le_add_right h0le 1)
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
hle1 : M.relRank F F₁ ≤ 1
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Theorem: Matroid.Flat.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two
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₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
hle1 : M.relRank F F₁ ≤ 1
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
have hle0 := WithTop.le_of_add_le_add_right h1top <| h.le.trans (add_le_add_left h1le 1)
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
hle1 : M.relRank F F₁ ≤ 1
hle0 : M.relRank F₀ F ≤ 1
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Theorem: Matroid.Flat.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two
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₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
hle1 : M.relRank F F₁ ≤ 1
hle0 : M.relRank F₀ F ≤ 1
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
rw [hF₀.covBy_iff_relRank_eq_one hF, hF.covBy_iff_relRank_eq_one hF₁,
  and_iff_right h₀.subset, and_iff_right h₁.subset]
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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
hle1 : M.relRank F F₁ ≤ 1
hle0 : M.relRank F₀ F ≤ 1
⊢ M.relRank F₀ F = 1 ∧ M.relRank F F₁ = 1
Theorem: Matroid.Flat.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two
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₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h1top : M.relRank F F₁ ≠ ⊤
hle1 : M.relRank F F₁ ≤ 1
hle0 : M.relRank F₀ F ≤ 1
⊢ M.relRank F₀ F = 1 ∧ M.relRank F F₁ = 1
Tactic:
exact ⟨hle0.antisymm h0le, hle1.antisymm h1le⟩
Proof state after:
no goals
Theorem: Matroid.Flat.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two
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₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
⊢ M.relRank F₀ F ≠ ⊤
Tactic:
intro 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h' : M.relRank F₀ F = ⊤
⊢ False
Theorem: Matroid.Flat.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two
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₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h' : M.relRank F₀ F = ⊤
⊢ False
Tactic:
rw [h'] at 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : ⊤ + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h' : M.relRank F₀ F = ⊤
⊢ False
Theorem: Matroid.Flat.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two
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₀
hF₁ : M.Flat F₁
h : ⊤ + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h' : M.relRank F₀ F = ⊤
⊢ False
Tactic:
norm_cast at h
Proof state after:
no goals
Theorem: Matroid.Flat.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two
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₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
⊢ M.relRank F F₁ ≠ ⊤
Tactic:
intro 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h' : M.relRank F F₁ = ⊤
⊢ False
Theorem: Matroid.Flat.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two
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₀
hF₁ : M.Flat F₁
h : M.relRank F₀ F + M.relRank F F₁ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h' : M.relRank F F₁ = ⊤
⊢ False
Tactic:
rw [h', add_top] at 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 : α
hF₀ : M.Flat F₀
hF₁ : M.Flat F₁
h : ⊤ = 2
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
h0le : 1 ≤ M.relRank F₀ F
h1le : 1 ≤ M.relRank F F₁
h0top : M.relRank F₀ F ≠ ⊤
h' : M.relRank F F₁ = ⊤
⊢ False