Theorem: Set.subset_of_eq (Jordan/Mathlib/Set.lean)

State before:
α✝¹ : Type u_1
α✝ : Type ?u.14727
β : Type ?u.14730
G : Type ?u.14733
X : Type ?u.14736
ι : Sort ?u.14739
κ : ι → Sort ?u.14744
α : Type u_2
s t : Set α
h : s = t
⊢ s ⊆ t
Tactic:
rw [h]
State after:
no goals