Theorem: Matroid.FlatOf.covBy_iff (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 : α
F₀ F₁ : FlatOf M
⊢ F₀ ⋖ F₁ ↔ ↑F₀ ⋖[M] ↑F₁
Tactic:
simp only [Matroid.CovBy, coe_flat, exists_true_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 : α
F₀ F₁ : FlatOf M
⊢ F₀ ⋖ F₁ ↔ ⋯.toFlatOf ⋖ ⋯.toFlatOf

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 : α
F₀ F₁ : FlatOf M
⊢ F₀ ⋖ F₁ ↔ ⋯.toFlatOf ⋖ ⋯.toFlatOf
Tactic:
rfl
State after:
no goals