Theorem: Matroid.Flat.covBy_iff_wcovBy_and_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₁
⊢ F₀ ⋖[M] F₁ ↔ (F₀ ⩿[M] F₁) ∧ F₀ ⊂ F₁
Tactic:
rw [hF₀.covBy_iff_wcovBy_and_ne hF₁, and_congr_right_iff, ssubset_iff_subset_ne,
  ne_eq, iff_and_self]
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₁
⊢ F₀ ⩿[M] F₁ → ¬F₀ = F₁ → F₀ ⊆ F₁

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₁ → F₀ ⊆ F₁
Tactic:
exact fun h _ ↦ h.subset
State after:
no goals