Theorem: Matroid.truncate_loopyOn_eq (Matroid/Constructions/Truncate.lean)

State before:
α : Type u_1
M : Matroid α
E✝ I B : Set α
k : ℕ∞
E : Set α
⊢ (loopyOn E).truncate = loopyOn E
Tactic:
simp (config := {contextual := true}) [truncate, ModularCut.principal, eq_loopyOn_iff]
State after:
no goals