Theorem: Set.inter_insert_eq (Matroid/ForMathlib/Set.lean)

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

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