α : Type u_1
β : Type ?u.15837
a b : α
ab : b = a
c : α
ac : c = a
⊢ b = c
α : Type u_1
β : Type ?u.15837
a b : α
ab : b ∈ pure a
c : α
ac : c ∈ pure a
⊢ b = c
rw [mem_pure] at ab ac
no goals
α : Type u_1
β : Type ?u.15837
a b : α
ab : b = a
c : α
ac : c = a
⊢ b = c
rwa [←ac] at ab