internlm/Lean-Github huggingface dataset:
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 : ⊤ = 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:
norm_cast at h
Proof state after:
no goals
Theorem: Matroid.CovBy.covBy_and_covBy_of_covBy_of_ssubset_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₀F' : F₀ ⋖[M] F'
hF'F₁ : F' ⋖[M] F₁
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
⊢ (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)
Tactic:
apply hF₀F'.flat_left.covBy_and_covBy_of_ssubset_of_ssubset_of_relRank_eq_two hF'F₁.flat_right
  ?_ hF h₀ 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₀F' : F₀ ⋖[M] F'
hF'F₁ : F' ⋖[M] F₁
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
⊢ M.relRank F₀ F₁ = 2
Theorem: Matroid.CovBy.covBy_and_covBy_of_covBy_of_ssubset_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₀F' : F₀ ⋖[M] F'
hF'F₁ : F' ⋖[M] F₁
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
⊢ M.relRank F₀ F₁ = 2
Tactic:
rw [← M.relRank_add_of_subset_of_subset hF₀F'.subset hF'F₁.subset, hF'F₁.relRank_eq_one,
  hF₀F'.relRank_eq_one]
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₀F' : F₀ ⋖[M] F'
hF'F₁ : F' ⋖[M] F₁
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
⊢ 1 + 1 = 2
Theorem: Matroid.CovBy.covBy_and_covBy_of_covBy_of_ssubset_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₀F' : F₀ ⋖[M] F'
hF'F₁ : F' ⋖[M] F₁
hF : M.Flat F
h₀ : F₀ ⊂ F
h₁ : F ⊂ F₁
⊢ 1 + 1 = 2
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.Flat.mem_covByPartition_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 : α
X : Set α
hF : M.Flat F
⊢ X ∈ hF.covByPartition ↔ ∃ F', (F ⋖[M] F') ∧ F' \ F = X
Tactic:
simp [Flat.covByPartition]
Proof state after:
no goals
Theorem: Matroid.Flat.partOf_covByPartition_eq
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
e : α
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Tactic:
by_cases he : e ∈ M.E \ F
Proof state after:
case pos
α : 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
e : α
he : e ∈ M.E \ F
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F

case neg
α : 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
e : α
he : e ∉ M.E \ F
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Theorem: Matroid.Flat.partOf_covByPartition_eq
Proof state before:
case neg
α : 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
e : α
he : e ∉ M.E \ F
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Tactic:
have hrw : insert e F ∩ M.E = F := by
  refine subset_antisymm ?_ (subset_inter (subset_insert _ _) hF.subset_ground)
  rw [← singleton_union, union_inter_distrib_right, union_subset_iff,
     (and_iff_left inter_subset_left)]
  rintro f ⟨rfl, hf⟩
  exact by_contra fun hfF ↦ he ⟨hf, hfF⟩
Proof state after:
case neg
α : 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
e : α
he : e ∉ M.E \ F
hrw : insert e F ∩ M.E = F
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Theorem: Matroid.Flat.partOf_covByPartition_eq
Proof state before:
case neg
α : 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
e : α
he : e ∉ M.E \ F
hrw : insert e F ∩ M.E = F
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Tactic:
rw [← cl_inter_ground, hrw, hF.cl, diff_self, hF.covByPartition.partOf_eq_empty he]
Proof state after:
no goals
Theorem: Matroid.Flat.partOf_covByPartition_eq
Proof state before:
case pos
α : 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
e : α
he : e ∈ M.E \ F
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Tactic:
obtain ⟨F', hFF', hF'⟩ := hF.mem_covByPartition_iff.1 (hF.covByPartition.partOf_mem he)
Proof state after:
case pos.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
e : α
he : e ∈ M.E \ F
F' : Set α
hFF' : F ⋖[M] F'
hF' : F' \ F = hF.covByPartition.partOf e
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Theorem: Matroid.Flat.partOf_covByPartition_eq
Proof state before:
case pos.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
e : α
he : e ∈ M.E \ F
F' : Set α
hFF' : F ⋖[M] F'
hF' : F' \ F = hF.covByPartition.partOf e
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Tactic:
obtain rfl := hFF'.cl_insert_eq (hF'.symm.subset <| hF.covByPartition.mem_partOf he)
Proof state after:
case pos.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
e : α
he : e ∈ M.E \ F
hFF' : F ⋖[M] M.cl (insert e F)
hF' : M.cl (insert e F) \ F = hF.covByPartition.partOf e
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Theorem: Matroid.Flat.partOf_covByPartition_eq
Proof state before:
case pos.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
e : α
he : e ∈ M.E \ F
hFF' : F ⋖[M] M.cl (insert e F)
hF' : M.cl (insert e F) \ F = hF.covByPartition.partOf e
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Tactic:
exact hF'.symm
Proof state after:
no goals
Theorem: Matroid.Flat.partOf_covByPartition_eq
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
e : α
he : e ∉ M.E \ F
⊢ insert e F ∩ M.E = F
Tactic:
refine subset_antisymm ?_ (subset_inter (subset_insert _ _) hF.subset_ground)
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
e : α
he : e ∉ M.E \ F
⊢ insert e F ∩ M.E ⊆ F
Theorem: Matroid.Flat.partOf_covByPartition_eq
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
e : α
he : e ∉ M.E \ F
⊢ insert e F ∩ M.E ⊆ F
Tactic:
rw [← singleton_union, union_inter_distrib_right, union_subset_iff,
   (and_iff_left inter_subset_left)]
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
e : α
he : e ∉ M.E \ F
⊢ {e} ∩ M.E ⊆ F
Theorem: Matroid.Flat.partOf_covByPartition_eq
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
e : α
he : e ∉ M.E \ F
⊢ {e} ∩ M.E ⊆ F
Tactic:
rintro f ⟨rfl, hf⟩
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
f : α
hf : f ∈ M.E
he : f ∉ M.E \ F
⊢ f ∈ F
Theorem: Matroid.Flat.partOf_covByPartition_eq
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
f : α
hf : f ∈ M.E
he : f ∉ M.E \ F
⊢ f ∈ F
Tactic:
exact by_contra fun hfF ↦ he ⟨hf, hfF⟩
Proof state after:
no goals
Theorem: Matroid.Flat.rel_covByPartition_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✝ : α
hF : M.Flat F
e f : α
⊢ hF.covByPartition.Rel e f ↔ e ∈ M.E \ F ∧ f ∈ M.E \ F ∧ M.cl (insert e F) = M.cl (insert f F)
Tactic:
simp only [hF.covByPartition.rel_iff_partOf_eq_partOf', partOf_covByPartition_eq, mem_diff,
  exists_prop, exists_and_left, 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✝ : α
hF : M.Flat F
e f : α
⊢ e ∈ M.E ∧ e ∉ F →
    f ∈ M.E ∧ f ∉ F → (M.cl (insert e F) \ F = M.cl (insert f F) \ F ↔ M.cl (insert e F) = M.cl (insert f F))
Theorem: Matroid.Flat.rel_covByPartition_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✝ : α
hF : M.Flat F
e f : α
⊢ e ∈ M.E ∧ e ∉ F →
    f ∈ M.E ∧ f ∉ F → (M.cl (insert e F) \ F = M.cl (insert f F) \ F ↔ M.cl (insert e F) = M.cl (insert f F))
Tactic:
refine fun _ _  ↦ ⟨fun h ↦ ?_, fun h ↦ by rw [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
e f : α
x✝¹ : e ∈ M.E ∧ e ∉ F
x✝ : f ∈ M.E ∧ f ∉ F
h : M.cl (insert e F) \ F = M.cl (insert f F) \ F
⊢ M.cl (insert e F) = M.cl (insert f F)
Theorem: Matroid.Flat.rel_covByPartition_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✝ : α
hF : M.Flat F
e f : α
x✝¹ : e ∈ M.E ∧ e ∉ F
x✝ : f ∈ M.E ∧ f ∉ F
h : M.cl (insert e F) \ F = M.cl (insert f F) \ F
⊢ M.cl (insert e F) = M.cl (insert f F)
Tactic:
rw [← union_eq_self_of_subset_right (M.cl_subset_cl (subset_insert e F)),
  ← union_eq_self_of_subset_right (M.cl_subset_cl (subset_insert f F)), hF.cl,
  ← diff_union_self, h, diff_union_self]
Proof state after:
no goals
Theorem: Matroid.Flat.rel_covByPartition_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✝ : α
hF : M.Flat F
e f : α
x✝¹ : e ∈ M.E ∧ e ∉ F
x✝ : f ∈ M.E ∧ f ∉ F
h : M.cl (insert e F) = M.cl (insert f F)
⊢ M.cl (insert e F) \ F = M.cl (insert f F) \ F
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Matroid.Flat.rel_covByPartition_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 : α
hF : M.Flat F
he : e ∈ M.E \ F
⊢ hF.covByPartition.Rel e f ↔ M.cl (insert e F) = M.cl (insert f F)
Tactic:
rw [hF.rel_covByPartition_iff, and_iff_right he, and_iff_right_iff_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 : α
hF : M.Flat F
he : e ∈ M.E \ F
⊢ M.cl (insert e F) = M.cl (insert f F) → f ∈ M.E \ F
Theorem: Matroid.Flat.rel_covByPartition_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 : α
hF : M.Flat F
he : e ∈ M.E \ F
⊢ M.cl (insert e F) = M.cl (insert f F) → f ∈ M.E \ F
Tactic:
refine fun hcl ↦ ⟨by_contra fun hf ↦ ?_, fun hfF ↦ ?_⟩
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 : α
hF : M.Flat F
he : e ∈ M.E \ F
hcl : M.cl (insert e F) = M.cl (insert f F)
hf : f ∉ M.E
⊢ 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 : α
hF : M.Flat F
he : e ∈ M.E \ F
hcl : M.cl (insert e F) = M.cl (insert f F)
hfF : f ∈ F
⊢ False
Theorem: Matroid.Flat.rel_covByPartition_iff'
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 : α
hF : M.Flat F
he : e ∈ M.E \ F
hcl : M.cl (insert e F) = M.cl (insert f F)
hfF : f ∈ F
⊢ False
Tactic:
rw [insert_eq_of_mem hfF, hF.cl] at hcl
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 : α
hF : M.Flat F
he : e ∈ M.E \ F
hcl : M.cl (insert e F) = F
hfF : f ∈ F
⊢ False
Theorem: Matroid.Flat.rel_covByPartition_iff'
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 : α
hF : M.Flat F
he : e ∈ M.E \ F
hcl : M.cl (insert e F) = F
hfF : f ∈ F
⊢ False
Tactic:
exact he.2 <| hcl.subset (M.mem_cl_of_mem (mem_insert e F))
Proof state after:
no goals
Theorem: Matroid.Flat.rel_covByPartition_iff'
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 : α
hF : M.Flat F
he : e ∈ M.E \ F
hcl : M.cl (insert e F) = M.cl (insert f F)
hf : f ∉ M.E
⊢ False
Tactic:
rw [← M.cl_inter_ground (insert f F), insert_inter_of_not_mem hf,
  inter_eq_self_of_subset_left hF.subset_ground, hF.cl] at hcl
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 : α
hF : M.Flat F
he : e ∈ M.E \ F
hcl : M.cl (insert e F) = F
hf : f ∉ M.E
⊢ False
Theorem: Matroid.Flat.rel_covByPartition_iff'
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 : α
hF : M.Flat F
he : e ∈ M.E \ F
hcl : M.cl (insert e F) = F
hf : f ∉ M.E
⊢ False
Tactic:
exact he.2 <| hcl.subset (M.mem_cl_of_mem (mem_insert e F))
Proof state after:
no goals
Theorem: Matroid.flat_contract
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 : α
X C : Set α
⊢ (M ／ C).Flat (M.cl (X ∪ C) \ C)
Tactic:
rw [flat_iff_cl_self, contract_cl_eq, diff_union_self, ← M.cl_union_cl_right_eq,
  union_eq_self_of_subset_right (M.cl_subset_cl subset_union_right), cl_cl]
Proof state after:
no goals
Theorem: Matroid.flat_contract_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 : α
hC : autoParam (C ⊆ M.E) _auto✝
⊢ (M ／ C).Flat F ↔ M.Flat (F ∪ C) ∧ Disjoint F C
Tactic:
rw [flat_iff_cl_self, contract_cl_eq, subset_antisymm_iff, subset_diff, diff_subset_iff,
  union_comm C, ← and_assoc, and_congr_left_iff, flat_iff_cl_self, subset_antisymm_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 : α
hC : autoParam (C ⊆ M.E) _auto✝
⊢ Disjoint F C → M.cl (F ∪ C) ⊆ F ∪ C → (F ⊆ M.cl (F ∪ C) ↔ F ∪ C ⊆ M.cl (F ∪ C))
Theorem: Matroid.flat_contract_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 : α
hC : autoParam (C ⊆ M.E) _auto✝
⊢ Disjoint F C → M.cl (F ∪ C) ⊆ F ∪ C → (F ⊆ M.cl (F ∪ C) ↔ F ∪ C ⊆ M.cl (F ∪ C))
Tactic:
exact fun _ _ ↦ ⟨fun h ↦ M.subset_cl _ (union_subset (h.trans (M.cl_subset_ground _)) hC),
  fun h ↦ subset_union_left.trans h⟩
Proof state after:
no goals
Theorem: Matroid.flat_contract_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 : α
⊢ (M ／ C).Flat F ↔ M.Flat (F ∪ C ∩ M.E) ∧ Disjoint F (C ∩ M.E)
Tactic:
rw [← contract_inter_ground_eq, flat_contract_iff]
Proof state after:
no goals
Theorem: Matroid.Flat.union_flat_of_contract'
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 ／ C).Flat F
⊢ M.Flat (F ∪ M.cl C)
Tactic:
replace hF := (flat_contract_iff'.1 hF).1.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 : α
hF : M.cl (F ∪ C ∩ M.E) = F ∪ C ∩ M.E
⊢ M.Flat (F ∪ M.cl C)
Theorem: Matroid.Flat.union_flat_of_contract'
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.cl (F ∪ C ∩ M.E) = F ∪ C ∩ M.E
⊢ M.Flat (F ∪ M.cl C)
Tactic:
rw [← cl_union_cl_right_eq, cl_inter_ground] at hF
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.cl (F ∪ M.cl C) = F ∪ C ∩ M.E
⊢ M.Flat (F ∪ M.cl C)
Theorem: Matroid.Flat.union_flat_of_contract'
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.cl (F ∪ M.cl C) = F ∪ C ∩ M.E
⊢ M.Flat (F ∪ M.cl C)
Tactic:
rw [flat_iff_subset_cl_self (union_subset _ (M.cl_subset_ground _)), hF]
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.cl (F ∪ M.cl C) = F ∪ C ∩ M.E
⊢ F ∪ C ∩ M.E ⊆ F ∪ M.cl C

α : 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.cl (F ∪ M.cl C) = F ∪ C ∩ M.E
⊢ F ⊆ M.E
Theorem: Matroid.Flat.union_flat_of_contract'
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.cl (F ∪ M.cl C) = F ∪ C ∩ M.E
⊢ F ⊆ M.E
Tactic:
exact subset_union_left.trans (hF.symm.subset.trans (M.cl_subset_ground _))
Proof state after:
no goals
Theorem: Matroid.Flat.union_flat_of_contract'
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.cl (F ∪ M.cl C) = F ∪ C ∩ M.E
⊢ F ∪ C ∩ M.E ⊆ F ∪ M.cl C
Tactic:
exact union_subset_union_right _ <| (M.subset_cl _).trans (M.cl_inter_ground _).subset
Proof state after:
no goals
Theorem: Matroid.Nonloop.contract_flat_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 : α
he : M.Nonloop e
⊢ (M ／ e).Flat F ↔ M.Flat (insert e F) ∧ e ∉ F
Tactic:
rw [contract_elem, flat_contract_iff, union_singleton, disjoint_singleton_right]
Proof state after:
no goals
Theorem: Matroid.flat_restrict_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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (M ↾ R).Flat F ↔ ∃ F', M.Flat F' ∧ F = F' ∩ R
Tactic:
refine ⟨fun h ↦ ⟨M.cl F, M.cl_flat F, ?_⟩, ?_⟩
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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
h : (M ↾ R).Flat F
⊢ F = M.cl F ∩ R

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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (∃ F', M.Flat F' ∧ F = F' ∩ R) → (M ↾ R).Flat F
Theorem: Matroid.flat_restrict_iff
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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (∃ F', M.Flat F' ∧ F = F' ∩ R) → (M ↾ R).Flat F
Tactic:
rintro ⟨F, hF, rfl⟩
Proof state after:
case refine_2.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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
⊢ (M ↾ R).Flat (F ∩ R)
Theorem: Matroid.flat_restrict_iff
Proof state before:
case refine_2.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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
⊢ (M ↾ R).Flat (F ∩ R)
Tactic:
rw [flat_iff_subset_cl_self]
Proof state after:
case refine_2.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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
⊢ (M ↾ R).cl (F ∩ R) ⊆ F ∩ R
Theorem: Matroid.flat_restrict_iff
Proof state before:
case refine_2.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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
⊢ (M ↾ R).cl (F ∩ R) ⊆ F ∩ R
Tactic:
suffices M.cl (F ∩ R) ∩ R ⊆ F by simpa [inter_assoc, diff_eq_empty.2 hR]
Proof state after:
case refine_2.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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
⊢ M.cl (F ∩ R) ∩ R ⊆ F
Theorem: Matroid.flat_restrict_iff
Proof state before:
case refine_2.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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
⊢ M.cl (F ∩ R) ∩ R ⊆ F
Tactic:
exact inter_subset_left.trans (hF.cl_subset_of_subset inter_subset_left)
Proof state after:
no goals
Theorem: Matroid.flat_restrict_iff
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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
h : (M ↾ R).Flat F
⊢ F = M.cl F ∩ R
Tactic:
nth_rw 1 [← h.cl]
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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
h : (M ↾ R).Flat F
⊢ (M ↾ R).cl F = M.cl F ∩ R
Theorem: Matroid.flat_restrict_iff
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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
h : (M ↾ R).Flat F
⊢ (M ↾ R).cl F = M.cl F ∩ R
Tactic:
have hFR : F ⊆ R := h.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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
h : (M ↾ R).Flat F
hFR : F ⊆ R
⊢ (M ↾ R).cl F = M.cl F ∩ R
Theorem: Matroid.flat_restrict_iff
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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
h : (M ↾ R).Flat F
hFR : F ⊆ R
⊢ (M ↾ R).cl F = M.cl F ∩ R
Tactic:
simp [inter_eq_self_of_subset_left hFR, diff_subset, diff_eq_empty.2 hR]
Proof state after:
no goals
Theorem: Matroid.flat_restrict_iff
Proof state before:
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
this : M.cl (F ∩ R) ∩ R ⊆ F
⊢ (M ↾ R).cl (F ∩ R) ⊆ F ∩ R
Tactic:
simpa [inter_assoc, diff_eq_empty.2 hR]
Proof state after:
no goals
Theorem: Matroid.flat_delete_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 : α
D : Set α
⊢ (M ＼ D).Flat F ↔ ∃ F', M.Flat F' ∧ F = F' \ D
Tactic:
simp_rw [delete_eq_restrict, flat_restrict_iff diff_subset, ← inter_diff_assoc]
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 : α
D : Set α
⊢ (∃ F', M.Flat F' ∧ F = (F' ∩ M.E) \ D) ↔ ∃ F', M.Flat F' ∧ F = F' \ D
Theorem: Matroid.flat_delete_iff
Proof state before:
case mpr
α : 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 : α
D : Set α
⊢ (∃ F', M.Flat F' ∧ F = F' \ D) → ∃ F', M.Flat F' ∧ F = (F' ∩ M.E) \ D
Tactic:
rintro ⟨F, hF, rfl⟩
Proof state after:
case mpr.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 : α
D F : Set α
hF : M.Flat F
⊢ ∃ F', M.Flat F' ∧ F \ D = (F' ∩ M.E) \ D
Theorem: Matroid.flat_delete_iff
Proof state before:
case mpr.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 : α
D F : Set α
hF : M.Flat F
⊢ ∃ F', M.Flat F' ∧ F \ D = (F' ∩ M.E) \ D
Tactic:
refine ⟨F, hF, ?_⟩
Proof state after:
case mpr.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 : α
D F : Set α
hF : M.Flat F
⊢ F \ D = (F ∩ M.E) \ D
Theorem: Matroid.flat_delete_iff
Proof state before:
case mpr.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 : α
D F : Set α
hF : M.Flat F
⊢ F \ D = (F ∩ M.E) \ D
Tactic:
rw [inter_eq_self_of_subset_left hF.subset_ground]
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 : α
⊢ (M ＼ e).Flat F ↔ e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))
Tactic:
rw [deleteElem, flat_delete_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 : α
⊢ (∃ F', M.Flat F' ∧ F = F' \ {e}) ↔ e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))
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 : α
⊢ (∃ F', M.Flat F' ∧ F = F' \ {e}) ↔ e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))
Tactic:
constructor
Proof state after:
case mp
α : 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 : α
⊢ (∃ F', M.Flat F' ∧ F = F' \ {e}) → e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))

case mpr
α : 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 : α
⊢ e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F)) → ∃ F', M.Flat F' ∧ F = F' \ {e}
Theorem: Matroid.flat_deleteElem_iff
Proof state before:
case mpr
α : 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 : α
⊢ e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F)) → ∃ F', M.Flat F' ∧ F = F' \ {e}
Tactic:
rintro ⟨heF, (hF | hF)⟩ <;> exact ⟨_, hF, by simp [heF]⟩
Proof state after:
no goals
Theorem: Matroid.flat_deleteElem_iff
Proof state before:
case mp
α : 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 : α
⊢ (∃ F', M.Flat F' ∧ F = F' \ {e}) → e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))
Tactic:
rintro ⟨F, hF, rfl⟩
Proof state after:
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})))