ext L
case h.e'_2.h.e'_2
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
⊢ (fun L => M.Line L ∧ e ∈ L) = fun F => M.Flat F ∧ M.er F = ↑1 + 1 ∧ e ∈ F
case h.e'_2.h.e'_2.h.a
α : Type u_1
M : Matroid α
e : α
he : M.Nonloop e
L : Set α
⊢ M.Line L ∧ e ∈ L ↔ M.Flat L ∧ M.er L = ↑1 + 1 ∧ e ∈ L