refine le_antisymm ?_ (one_le_girth _)
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ (loopyOn E).girth = 1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ (loopyOn E).girth ≤ 1