Marginally generalize checks

Author: robertmaxton42

MathlibTest/Delab/TopologicalSpace.lean

@@ -3,32 +3,30 @@ import Mathlib.Topology.Order
 open TopologicalSpace
 open scoped Topology
 
-variable (p : ℕ → Prop) (s : Set ℕ)
+-- TODO If and when `(try)SynthInstance` in `#check` is fixed, replace `ℕ` and `Prop` with variables
 
--- For unary ops, we check that `induced p inferInstance` triggers the delab and `inferInstance` does not
+variable {α : Type*} [TopologicalSpace α] (f : ℕ → α) (p : ℕ → Prop) (s : Set ℕ)
 
-/-- info: IsOpen[induced p inferInstance] s ↔ IsOpen s : Prop -/
-#guard_msgs(info) in
-#check IsOpen[induced p inferInstance] s ↔ IsOpen[inferInstance] s
+-- For unary ops, we check that `induced p inferInstance` triggers the delab and `inferInstance` does not
 
-/-- info: IsClosed[induced p inferInstance] s ↔ IsClosed s : Prop -/
+/-- info: IsOpen[induced f inferInstance] s ↔ IsOpen s : Prop -/
 #guard_msgs(info) in
-#check IsClosed[induced p inferInstance] s ↔ IsClosed[inferInstance] s
+#check IsOpen[induced f inferInstance] s ↔ IsOpen[inferInstance] s
 
-/-- info: closure[induced p inferInstance] s = closure s : Prop -/
+/-- info: IsClosed[induced f inferInstance] s ↔ IsClosed s : Prop -/
 #guard_msgs(info) in
-#check closure[induced p inferInstance] s = closure[inferInstance] s
+#check IsClosed[induced f inferInstance] s ↔ IsClosed[inferInstance] s
 
-/-- info: Continuous[induced p inferInstance, inferInstance] p ↔ Continuous[inferInstance, coinduced p inferInstance] p : Prop -/
+/-- info: closure[induced f inferInstance] s = closure s : Prop -/
 #guard_msgs(info) in
-#check Continuous[induced p inferInstance, inferInstance] p ↔ Continuous[inferInstance, coinduced p inferInstance] p
+#check closure[induced f inferInstance] s = closure[inferInstance] s
 
--- For binary ops, we check that `(co)induced p inferInstance` in either or both slots triggers the delab
+-- For binary ops, we check that `(co)induced f inferInstance` in either or both slots triggers the delab
 -- and `inferInstance` in both slots does not
 
-/-- info: Continuous[induced p inferInstance, inferInstance] p ↔ Continuous[inferInstance, coinduced p inferInstance] p : Prop -/
+/-- info: Continuous[induced f inferInstance, inferInstance] f ↔ Continuous[inferInstance, coinduced f inferInstance] f : Prop -/
 #guard_msgs(info) in
-#check Continuous[induced p inferInstance, inferInstance] p ↔ Continuous[inferInstance, coinduced p inferInstance] p
+#check Continuous[induced f inferInstance, inferInstance] f ↔ Continuous[inferInstance, coinduced f inferInstance] f
 
 /-- info: Continuous[induced p inferInstance, coinduced p inferInstance] p ↔ Continuous p : Prop -/
 #guard_msgs(info) in