Theorem: Matroid.Nonloop.cl_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 : α
he : M.Nonloop e
⊢ M.cl {e} ⋖[M] L ↔ M.Line L ∧ e ∈ L
Tactic:
refine ⟨fun h ↦ ⟨⟨h.flat_right, ?_⟩,h.subset <| M.mem_cl_self e⟩,
  fun ⟨hL, heL⟩ ↦ by rwa [← hL.mem_iff_covBy he]⟩
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 : α
he : M.Nonloop e
h : M.cl {e} ⋖[M] L
⊢ M.er L = 2

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 : α
he : M.Nonloop e
h : M.cl {e} ⋖[M] L
⊢ M.er L = 2
Tactic:
rw [h.er_eq, er_cl_eq, he.er_eq]
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 : α
he : M.Nonloop e
h : M.cl {e} ⋖[M] L
⊢ 1 + 1 = 2

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 : α
he : M.Nonloop e
h : M.cl {e} ⋖[M] L
⊢ 1 + 1 = 2
Tactic:
rfl
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 : α
he : M.Nonloop e
x✝ : M.Line L ∧ e ∈ L
hL : M.Line L
heL : e ∈ L
⊢ M.cl {e} ⋖[M] L
Tactic:
rwa [← hL.mem_iff_covBy he]
State after:
no goals