Theorem: Matroid.Flat.covBy_iff_eq_cl_insert (Matroid/Flat.lean)

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₀
⊢ F₀ ⋖[M] F₁ ↔ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)
Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
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₀
h : F₀ ⋖[M] F₁
⊢ ∃ e ∈ M.E \ 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₀
⊢ (∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) → F₀ ⋖[M] F₁

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₀
⊢ (∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) → F₀ ⋖[M] F₁
Tactic:
rintro ⟨e, heF₀, rfl⟩
State after:
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₀)

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₁ ↦ ?_⟩
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₀)

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

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

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))
State after:
no goals

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

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⟩
State after:
no goals

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]
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

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⟩
State after:
no goals

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))
State after:
no goals