Theorem: Matroid.Line.mem_iff_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 : α
hL : M.Line L
he : M.Nonloop e
⊢ e ∈ L ↔ M.cl {e} ⋖[M] L
Tactic:
rw [(M.cl_flat {e}).covBy_iff_relRank_eq_one hL.flat, hL.flat.cl_subset_iff_subset,
  singleton_subset_iff, iff_self_and, relRank_cl_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 : α
hL : M.Line L
he : M.Nonloop e
⊢ e ∈ L → M.relRank {e} L = 1

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 : α
hL : M.Line L
he : M.Nonloop e
⊢ e ∈ L → M.relRank {e} L = 1
Tactic:
intro heL
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 : α
hL : M.Line L
he : M.Nonloop e
heL : e ∈ L
⊢ M.relRank {e} L = 1

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 : α
hL : M.Line L
he : M.Nonloop e
heL : e ∈ L
⊢ M.relRank {e} L = 1
Tactic:
rw [(M.rFin_singleton e).relRank_eq_sub (by simpa), he.er_eq, hL.er]
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 : α
hL : M.Line L
he : M.Nonloop e
heL : e ∈ L
⊢ 2 - 1 = 1

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 : α
hL : M.Line L
he : M.Nonloop e
heL : e ∈ L
⊢ 2 - 1 = 1
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 : α
hL : M.Line L
he : M.Nonloop e
heL : e ∈ L
⊢ {e} ⊆ L
Tactic:
simpa
State after:
no goals