Continuity of composition with subtypes

Stream: Is there code for X?

[Gareth Ma]

import Mathlib.Topology.Covering
import Mathlib.Topology.UnitInterval

open Int Topology Metric Set Filter AddSubgroup

example {f : ℝ → ℝ} {A : Set ℝ} (hf : ContinuousOn f A) :
    ContinuousOn (fun x ↦ (⟨f x, ⟨0, True.intro⟩⟩ : ℝ × { x : ℝ // True })) A := by
  sorry

How should I prove something like this? continuity fails. If it's just <f x, 0> then I can prove by writing it as $x \mapsto f(x) \mapsto (f(x), 0)$

[Gareth Ma]

Nevermind, I thin I just use ContinuousOn.prod... oops

[Gareth Ma]

example {f : ℝ → ℝ} {A : Set ℝ} (hf : ContinuousOn f A) :
    ContinuousOn (fun x ↦ (⟨f x, ⟨0, True.intro⟩⟩ : ℝ × { _x : ℝ // True })) A := by
  apply ContinuousOn.prod hf
  change ContinuousOn ((fun d ↦ (⟨d, True.intro⟩ : { _x : ℝ // True })) ∘ (fun _ ↦ 0)) A
  exact ContinuousOn.comp (t := {0}) (by simp) continuousOn_const (by simp [MapsTo])

[Gareth Ma]

example {f : ℝ → ℝ} {A : Set ℝ} (hf : ContinuousOn f A) :
    ContinuousOn (fun x ↦ (⟨f x, ⟨0, True.intro⟩⟩ : ℝ × { _x : ℝ // True })) A :=
  hf.prod continuousOn_const

I guess this is what overthinking looks like in Lean
(Of course Lean knows 0 = <0, ...>...)

[Gareth Ma]

(deleted)