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

State before:
α : Type u_1
ι : Type u_2
s t r : Set α
⊢ s \ t = s \ r ↔ t ∩ s = r ∩ s
Tactic:
rw [← diff_inter_self_eq_diff, ← diff_inter_self_eq_diff (t := r)]
State after:
α : Type u_1
ι : Type u_2
s t r : Set α
⊢ s \ (t ∩ s) = s \ (r ∩ s) ↔ t ∩ s = r ∩ s

State before:
α : Type u_1
ι : Type u_2
s t r : Set α
⊢ s \ (t ∩ s) = s \ (r ∩ s) ↔ t ∩ s = r ∩ s
Tactic:
refine' ⟨fun h ↦ _, fun h ↦ by rw [h]⟩
State after:
α : Type u_1
ι : Type u_2
s t r : Set α
h : s \ (t ∩ s) = s \ (r ∩ s)
⊢ t ∩ s = r ∩ s

State before:
α : Type u_1
ι : Type u_2
s t r : Set α
h : s \ (t ∩ s) = s \ (r ∩ s)
⊢ t ∩ s = r ∩ s
Tactic:
rw [← diff_diff_cancel_left inter_subset_right, h, diff_diff_cancel_left inter_subset_right]
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
s t r : Set α
h : t ∩ s = r ∩ s
⊢ s \ (t ∩ s) = s \ (r ∩ s)
Tactic:
rw [h]
State after:
no goals