Theorem: Matroid.FlatOf.wcovBy_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.WCovBy, 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