internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Flat.covBy_iff_eq_cl_insert
Proof state before:
case refine_2.intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF₀ : M.Flat F₀
e : α
heF₀ : e ∈ M.E \ F₀
⊢ F₀ ⋖[M] M.cl (insert e F₀)
Tactic:
refine
  covBy_iff.2 ⟨hF₀, M.cl_flat _, (M.subset_cl_of_subset (subset_insert _ _) ?_).ssubset_of_ne ?_,
    fun F hF hF₀F hFF₁ ↦ ?_⟩
Proof state after:
case refine_2.intro.intro.refine_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF₀ : M.Flat F₀
e : α
heF₀ : e ∈ M.E \ F₀
⊢ insert e F₀ ⊆ M.E

case refine_2.intro.intro.refine_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF₀ : M.Flat F₀
e : α
heF₀ : e ∈ M.E \ F₀
⊢ F₀ ≠ M.cl (insert e F₀)

case refine_2.intro.intro.refine_3
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF₀ : M.Flat F₀
e : α
heF₀ : e ∈ M.E \ F₀
F : Set α
hF : M.Flat F
hF₀F : F₀ ⊆ F
hFF₁ : F ⊆ M.cl (insert e F₀)
⊢ F = F₀ ∨ F = M.cl (insert e F₀)
Theorem: Matroid.Flat.covBy_iff_eq_cl_insert
Proof state before:
case refine_2.intro.intro.refine_3
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF₀ : M.Flat F₀
e : α
heF₀ : e ∈ M.E \ F₀
F : Set α
hF : M.Flat F
hF₀F : F₀ ⊆ F
hFF₁ : F ⊆ M.cl (insert e F₀)
⊢ F = F₀ ∨ F = M.cl (insert e F₀)
Tactic:
refine hF₀F.eq_or_ssubset.elim (fun h ↦ Or.inl h.symm)
  (fun hss ↦ Or.inr (hFF₁.antisymm (hF.cl_subset_of_subset (insert_subset ?_ hF₀F))))
Proof state after:
case refine_2.intro.intro.refine_3
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF₀ : M.Flat F₀
e : α
heF₀ : e ∈ M.E \ F₀
F : Set α
hF : M.Flat F
hF₀F : F₀ ⊆ F
hFF₁ : F ⊆ M.cl (insert e F₀)
hss : F₀ ⊂ F
⊢ e ∈ F
Theorem: Matroid.Flat.covBy_iff_eq_cl_insert
Proof state before:
case refine_2.intro.intro.refine_3
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF₀ : M.Flat F₀
e : α
heF₀ : e ∈ M.E \ F₀
F : Set α
hF : M.Flat F
hF₀F : F₀ ⊆ F
hFF₁ : F ⊆ M.cl (insert e F₀)
hss : F₀ ⊂ F
⊢ e ∈ F
Tactic:
obtain ⟨f, hfF, hfF₀⟩ := exists_of_ssubset hss
Proof state after:
case refine_2.intro.intro.refine_3.intro.intro
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f✝ : α
hF₀ : M.Flat F₀
e : α
heF₀ : e ∈ M.E \ F₀
F : Set α
hF : M.Flat F
hF₀F : F₀ ⊆ F
hFF₁ : F ⊆ M.cl (insert e F₀)
hss : F₀ ⊂ F
f : α
hfF : f ∈ F
hfF₀ : f ∉ F₀
⊢ e ∈ F
Theorem: Matroid.Flat.covBy_iff_eq_cl_insert
Proof state before:
case refine_2.intro.intro.refine_3.intro.intro
α : Type u_1
M : Matroid α
I F✝ X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f✝ : α
hF₀ : M.Flat F₀
e : α
heF₀ : e ∈ M.E \ F₀
F : Set α
hF : M.Flat F
hF₀F : F₀ ⊆ F
hFF₁ : F ⊆ M.cl (insert e F₀)
hss : F₀ ⊂ F
f : α
hfF : f ∈ F
hfF₀ : f ∉ F₀
⊢ e ∈ F
Tactic:
exact mem_of_mem_of_subset (hF₀.cl_exchange ⟨hFF₁ hfF, hfF₀⟩).1
  (hF.cl_subset_of_subset (insert_subset hfF hF₀F))
Proof state after:
no goals
Theorem: Matroid.Flat.covBy_iff_eq_cl_insert
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₀
h : F₀ ⋖[M] F₁
⊢ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)
Tactic:
obtain ⟨e, he, rfl⟩ := h.exists_eq_cl_insert
Proof state after:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF₀ : M.Flat F₀
e : α
h : F₀ ⋖[M] M.cl (insert e F₀)
he : e ∈ M.cl (insert e F₀) \ F₀
⊢ ∃ e_1 ∈ M.E \ F₀, M.cl (insert e F₀) = M.cl (insert e_1 F₀)
Theorem: Matroid.Flat.covBy_iff_eq_cl_insert
Proof state before:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF₀ : M.Flat F₀
e : α
h : F₀ ⋖[M] M.cl (insert e F₀)
he : e ∈ M.cl (insert e F₀) \ F₀
⊢ ∃ e_1 ∈ M.E \ F₀, M.cl (insert e F₀) = M.cl (insert e_1 F₀)
Tactic:
exact ⟨e, ⟨(M.cl_subset_ground _) he.1, he.2⟩, rfl⟩
Proof state after:
no goals
Theorem: Matroid.Flat.covBy_iff_eq_cl_insert
Proof state before:
case refine_2.intro.intro.refine_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF₀ : M.Flat F₀
e : α
heF₀ : e ∈ M.E \ F₀
⊢ insert e F₀ ⊆ M.E
Tactic:
rw [insert_eq, union_subset_iff, singleton_subset_iff]
Proof state after:
case refine_2.intro.intro.refine_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF₀ : M.Flat F₀
e : α
heF₀ : e ∈ M.E \ F₀
⊢ e ∈ M.E ∧ F₀ ⊆ M.E
Theorem: Matroid.Flat.covBy_iff_eq_cl_insert
Proof state before:
case refine_2.intro.intro.refine_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF₀ : M.Flat F₀
e : α
heF₀ : e ∈ M.E \ F₀
⊢ e ∈ M.E ∧ F₀ ⊆ M.E
Tactic:
exact ⟨heF₀.1, hF₀.subset_ground⟩
Proof state after:
no goals
Theorem: Matroid.Flat.covBy_iff_eq_cl_insert
Proof state before:
case refine_2.intro.intro.refine_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF₀ : M.Flat F₀
e : α
heF₀ : e ∈ M.E \ F₀
⊢ F₀ ≠ M.cl (insert e F₀)
Tactic:
exact fun h ↦ heF₀.2 (h.symm.subset (mem_cl_of_mem' _ (mem_insert _ _) heF₀.1))
Proof state after:
no goals
Theorem: Matroid.CovBy.er_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 : α
h : F ⋖[M] F'
⊢ M.er F' = M.er F + 1
Tactic:
obtain ⟨e, he, rfl⟩ := h.exists_eq_cl_insert
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
I F X Y F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f e : α
h : F ⋖[M] M.cl (insert e F)
he : e ∈ M.cl (insert e F) \ F
⊢ M.er (M.cl (insert e F)) = M.er F + 1
Theorem: Matroid.CovBy.er_eq
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
I F X Y F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f e : α
h : F ⋖[M] M.cl (insert e F)
he : e ∈ M.cl (insert e F) \ F
⊢ M.er (M.cl (insert e F)) = M.er F + 1
Tactic:
rw [er_cl_eq, h.flat_left.er_insert_eq_add_one]
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
I F X Y F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f e : α
h : F ⋖[M] M.cl (insert e F)
he : e ∈ M.cl (insert e F) \ F
⊢ e ∈ M.E \ F
Theorem: Matroid.CovBy.er_eq
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
I F X Y F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f e : α
h : F ⋖[M] M.cl (insert e F)
he : e ∈ M.cl (insert e F) \ F
⊢ e ∈ M.E \ F
Tactic:
exact ⟨M.cl_subset_ground _ he.1, he.2⟩
Proof state after:
no goals
Theorem: Matroid.cl_covBy_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.cl X ⋖[M] F ↔ ∃ e ∈ M.E \ M.cl X, F = M.cl (insert e X)
Tactic:
simp_rw [(M.cl_flat X).covBy_iff_eq_cl_insert, cl_insert_cl_eq_cl_insert]
Proof state after:
no goals
Theorem: Matroid.cl_covBy_cl_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.cl X ⋖[M] M.cl Y ↔ ∃ e ∈ M.E, e ∈ Y ∧ e ∉ M.cl X ∧ M.cl (insert e X) = M.cl Y
Tactic:
rw [cl_covBy_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 : α
⊢ (∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)) ↔ ∃ e ∈ M.E, e ∈ Y ∧ e ∉ M.cl X ∧ M.cl (insert e X) = M.cl Y
Theorem: Matroid.cl_covBy_cl_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 : α
⊢ (∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)) ↔ ∃ e ∈ M.E, e ∈ Y ∧ e ∉ M.cl X ∧ M.cl (insert e X) = M.cl Y
Tactic:
refine ⟨fun ⟨e, he, hYX⟩ ↦ ?_, fun ⟨e, he, _, heX, h_eq⟩ ↦ ⟨e, ⟨he, heX⟩, h_eq.symm⟩ ⟩
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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
⊢ ∃ e ∈ M.E, e ∈ Y ∧ e ∉ M.cl X ∧ M.cl (insert e X) = M.cl Y
Theorem: Matroid.cl_covBy_cl_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✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
⊢ ∃ e ∈ M.E, e ∈ Y ∧ e ∉ M.cl X ∧ M.cl (insert e X) = M.cl Y
Tactic:
by_contra! hcon
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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
⊢ False
Theorem: Matroid.cl_covBy_cl_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✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
⊢ False
Tactic:
have hY : Y ∩ M.E ⊆ M.cl X := by
  refine fun f hf ↦ by_contra fun hfX ↦ hcon f hf.2 hf.1 hfX ?_
  rw [hYX]
  apply cl_insert_eq_cl_insert_of_mem ⟨?_, hfX⟩
  rw [← hYX, ← cl_inter_ground]
  exact M.subset_cl _ (by aesop_mat) 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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
hY : Y ∩ M.E ⊆ M.cl X
⊢ False
Theorem: Matroid.cl_covBy_cl_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✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
hY : Y ∩ M.E ⊆ M.cl X
⊢ False
Tactic:
replace hY := M.cl_subset_cl_of_subset_cl hY
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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
hY : M.cl (Y ∩ M.E) ⊆ M.cl X
⊢ False
Theorem: Matroid.cl_covBy_cl_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✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
hY : M.cl (Y ∩ M.E) ⊆ M.cl X
⊢ False
Tactic:
rw [cl_inter_ground, hYX] at hY
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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
hY : M.cl (insert e X) ⊆ M.cl X
⊢ False
Theorem: Matroid.cl_covBy_cl_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✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
hY : M.cl (insert e X) ⊆ M.cl X
⊢ False
Tactic:
exact he.2 <| hY (M.mem_cl_of_mem' (mem_insert _ _) he.1)
Proof state after:
no goals
Theorem: Matroid.cl_covBy_cl_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✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
⊢ Y ∩ M.E ⊆ M.cl X
Tactic:
refine fun f hf ↦ by_contra fun hfX ↦ hcon f hf.2 hf.1 hfX ?_
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✝ : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ M.cl (insert f X) = M.cl Y
Theorem: Matroid.cl_covBy_cl_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✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ M.cl (insert f X) = M.cl Y
Tactic:
rw [hYX]
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✝ : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ M.cl (insert f X) = M.cl (insert e X)
Theorem: Matroid.cl_covBy_cl_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✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ M.cl (insert f X) = M.cl (insert e X)
Tactic:
apply cl_insert_eq_cl_insert_of_mem ⟨?_, hfX⟩
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✝ : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ f ∈ M.cl (insert e X)
Theorem: Matroid.cl_covBy_cl_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✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ f ∈ M.cl (insert e X)
Tactic:
rw [← hYX, ← cl_inter_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✝ : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ f ∈ M.cl (Y ∩ M.E)
Theorem: Matroid.cl_covBy_cl_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✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ f ∈ M.cl (Y ∩ M.E)
Tactic:
exact M.subset_cl _ (by aesop_mat) hf
Proof state after:
no goals
Theorem: Matroid.cl_covBy_cl_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✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ Y ∩ M.E ⊆ M.E
Tactic:
aesop_mat
Proof state after:
no goals
Theorem: Matroid.Indep.cl_diff_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 : α
hI : M.Indep I
he : e ∈ I
⊢ M.cl (I \ {e}) ⋖[M] M.cl I
Tactic:
simpa [cl_insert_cl_eq_cl_insert, he] using
  (M.cl_flat _).covBy_cl_insert (not_mem_cl_diff_of_mem hI he) (hI.subset_ground he)
Proof state after:
no goals
Theorem: Matroid.Indep.covBy_cl_insert
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 : α
hI : M.Indep I
he : e ∈ M.E \ M.cl I
⊢ M.cl I ⋖[M] M.cl (insert e I)
Tactic:
simpa [not_mem_of_mem_diff_cl he] using
  (hI.insert_indep_iff.2 <| .inl he).cl_diff_covBy (.inl rfl)
Proof state after:
no goals
Theorem: Matroid.Flat.covBy_iff_relRank_eq_one
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
⊢ F₀ ⋖[M] F ↔ F₀ ⊆ F ∧ M.relRank F₀ F = 1
Tactic:
simp_rw [hF₀.covBy_iff_eq_cl_insert, relRank_eq_one_iff hF.subset_ground, hF₀.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.Flat F₀
hF : M.Flat F
⊢ (∃ e ∈ M.E \ F₀, F = M.cl (insert e F₀)) ↔ F₀ ⊆ F ∧ ∃ e ∈ F \ F₀, F ⊆ M.cl (insert e F₀)
Theorem: Matroid.Flat.covBy_iff_relRank_eq_one
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
⊢ (∃ e ∈ M.E \ F₀, F = M.cl (insert e F₀)) ↔ F₀ ⊆ F ∧ ∃ e ∈ F \ F₀, F ⊆ M.cl (insert e F₀)
Tactic:
refine ⟨?_, fun ⟨hss, e, he, h⟩ ↦ ⟨e, ?_, h.antisymm ?_⟩⟩
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₀
hF : M.Flat F
⊢ (∃ e ∈ M.E \ F₀, F = M.cl (insert e F₀)) → F₀ ⊆ F ∧ ∃ e ∈ F \ F₀, F ⊆ M.cl (insert e F₀)

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₀
hF : M.Flat F
x✝ : F₀ ⊆ F ∧ ∃ e ∈ F \ F₀, F ⊆ M.cl (insert e F₀)
hss : F₀ ⊆ F
e : α
he : e ∈ F \ F₀
h : F ⊆ M.cl (insert e F₀)
⊢ e ∈ M.E \ F₀

case refine_3
α : Type 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
x✝ : F₀ ⊆ F ∧ ∃ e ∈ F \ F₀, F ⊆ M.cl (insert e F₀)
hss : F₀ ⊆ F
e : α
he : e ∈ F \ F₀
h : F ⊆ M.cl (insert e F₀)
⊢ M.cl (insert e F₀) ⊆ F
Theorem: Matroid.Flat.covBy_iff_relRank_eq_one
Proof state before:
case refine_3
α : Type 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
x✝ : F₀ ⊆ F ∧ ∃ e ∈ F \ F₀, F ⊆ M.cl (insert e F₀)
hss : F₀ ⊆ F
e : α
he : e ∈ F \ F₀
h : F ⊆ M.cl (insert e F₀)
⊢ M.cl (insert e F₀) ⊆ F
Tactic:
exact hF.cl_subset_iff_subset.2 <| insert_subset he.1 hss
Proof state after:
no goals
Theorem: Matroid.Flat.covBy_iff_relRank_eq_one
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₀
hF : M.Flat F
⊢ (∃ e ∈ M.E \ F₀, F = M.cl (insert e F₀)) → F₀ ⊆ F ∧ ∃ e ∈ F \ F₀, F ⊆ M.cl (insert e F₀)
Tactic:
rintro ⟨e, ⟨he, heE⟩, rfl⟩
Proof state after:
case refine_1.intro.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 : α
hF₀ : M.Flat F₀
e : α
he : e ∈ M.E
heE : e ∉ F₀
hF : M.Flat (M.cl (insert e F₀))
⊢ F₀ ⊆ M.cl (insert e F₀) ∧ ∃ e_1 ∈ M.cl (insert e F₀) \ F₀, M.cl (insert e F₀) ⊆ M.cl (insert e_1 F₀)
Theorem: Matroid.Flat.covBy_iff_relRank_eq_one
Proof state before:
case refine_1.intro.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 : α
hF₀ : M.Flat F₀
e : α
he : e ∈ M.E
heE : e ∉ F₀
hF : M.Flat (M.cl (insert e F₀))
⊢ F₀ ⊆ M.cl (insert e F₀) ∧ ∃ e_1 ∈ M.cl (insert e F₀) \ F₀, M.cl (insert e F₀) ⊆ M.cl (insert e_1 F₀)
Tactic:
refine ⟨M.subset_cl_of_subset (subset_insert _ _), ⟨e, ⟨?_, heE⟩, rfl.subset⟩⟩
Proof state after:
case refine_1.intro.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 : α
hF₀ : M.Flat F₀
e : α
he : e ∈ M.E
heE : e ∉ F₀
hF : M.Flat (M.cl (insert e F₀))
⊢ e ∈ M.cl (insert e F₀)
Theorem: Matroid.Flat.covBy_iff_relRank_eq_one
Proof state before:
case refine_1.intro.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 : α
hF₀ : M.Flat F₀
e : α
he : e ∈ M.E
heE : e ∉ F₀
hF : M.Flat (M.cl (insert e F₀))
⊢ e ∈ M.cl (insert e F₀)
Tactic:
exact M.mem_cl_of_mem (mem_insert _ _)
Proof state after:
no goals
Theorem: Matroid.Flat.covBy_iff_relRank_eq_one
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₀
hF : M.Flat F
x✝ : F₀ ⊆ F ∧ ∃ e ∈ F \ F₀, F ⊆ M.cl (insert e F₀)
hss : F₀ ⊆ F
e : α
he : e ∈ F \ F₀
h : F ⊆ M.cl (insert e F₀)
⊢ e ∈ M.E \ F₀
Tactic:
apply diff_subset_diff_left hF.subset_ground he
Proof state after:
no goals
Theorem: Matroid.Flat.exists_unique_flat_of_not_mem
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₀
⊢ ∃! F₁, e ∈ F₁ ∧ (F₀ ⋖[M] F₁)
Tactic:
simp_rw [hF₀.covBy_iff_eq_cl_insert]
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₀
⊢ ∃! F₁, e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)
Theorem: Matroid.Flat.exists_unique_flat_of_not_mem
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₀
⊢ ∃! F₁, e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)
Tactic:
use M.cl (insert e F₀)
Proof state after:
case h
α : Type 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₀
⊢ (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) (M.cl (insert e F₀)) ∧
    ∀ (y : Set α), (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) y → y = M.cl (insert e F₀)
Theorem: Matroid.Flat.exists_unique_flat_of_not_mem
Proof state before:
case h
α : Type 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₀
⊢ (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) (M.cl (insert e F₀)) ∧
    ∀ (y : Set α), (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) y → y = M.cl (insert e F₀)
Tactic:
refine' ⟨_, _⟩
Proof state after:
case h.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₀
⊢ (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) (M.cl (insert e F₀))

case h.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₀
⊢ ∀ (y : Set α), (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) y → y = M.cl (insert e F₀)
Theorem: Matroid.Flat.exists_unique_flat_of_not_mem
Proof state before:
case h.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₀
⊢ ∀ (y : Set α), (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) y → y = M.cl (insert e F₀)
Tactic:
simp only [exists_prop, and_imp, forall_exists_index]
Proof state after:
case h.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₀
⊢ ∀ (y : Set α), e ∈ y → ∀ x ∈ M.E \ F₀, y = M.cl (insert x F₀) → y = M.cl (insert e F₀)
Theorem: Matroid.Flat.exists_unique_flat_of_not_mem
Proof state before:
case h.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₀
⊢ ∀ (y : Set α), e ∈ y → ∀ x ∈ M.E \ F₀, y = M.cl (insert x F₀) → y = M.cl (insert e F₀)
Tactic:
rintro X heX f _ rfl
Proof state after:
case h.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₀
f : α
a✝ : f ∈ M.E \ F₀
heX : e ∈ M.cl (insert f F₀)
⊢ M.cl (insert f F₀) = M.cl (insert e F₀)
Theorem: Matroid.Flat.exists_unique_flat_of_not_mem
Proof state before:
case h.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₀
f : α
a✝ : f ∈ M.E \ F₀
heX : e ∈ M.cl (insert f F₀)
⊢ M.cl (insert f F₀) = M.cl (insert e F₀)
Tactic:
rw [hF₀.cl_insert_eq_cl_insert_of_mem ⟨heX, he.2⟩]
Proof state after:
no goals
Theorem: Matroid.Flat.exists_unique_flat_of_not_mem
Proof state before:
case h.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₀
⊢ (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) (M.cl (insert e F₀))
Tactic:
constructor
Proof state after:
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₀)

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₀)