Theorem: Matroid.inter_insert_eq (Matroid/Old/ModularCut.lean)

State before:
α : Type u_1
A : Set α
b c : α
hne : b ≠ c
⊢ insert b A ∩ insert c A = A
Tactic:
rw [insert_eq, insert_eq, ← union_distrib_right, Disjoint.inter_eq _, empty_union]
State after:
α : Type u_1
A : Set α
b c : α
hne : b ≠ c
⊢ Disjoint {b} {c}

State before:
α : Type u_1
A : Set α
b c : α
hne : b ≠ c
⊢ Disjoint {b} {c}
Tactic:
rwa [disjoint_singleton]
State after:
no goals