Theorem: Matroid.Flat.exists_covBy_right_of_ssubset (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₀
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
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₁)

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

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

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

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

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

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

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

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

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