Theorem: Matroid.WCovBy.eq_or_covBy (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 : α
h : F₀ ⩿[M] F₁
⊢ F₀ = F₁ ∨ (F₀ ⋖[M] F₁)
Tactic:
rw [or_iff_not_imp_left]
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 : α
h : F₀ ⩿[M] F₁
⊢ ¬F₀ = F₁ → F₀ ⋖[M] 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 : α
h : F₀ ⩿[M] F₁
⊢ ¬F₀ = F₁ → F₀ ⋖[M] F₁
Tactic:
exact h.covBy_of_ne
State after:
no goals