How to work with subtypes

Stream: new members

[Michał Pacholski]

I'm having problems proving statements about subtypes, e.g. I have goal

orig orig' : ℝ
⊢ Continuous fun x ↦ ⟨↑x + orig - orig', trivial⟩

which arose from the following attempt in constructing GlueData:

import Mathlib.Topology.Gluing
import Mathlib.Topology.MetricSpace.Pseudo.Defs
import Mathlib.Analysis.Normed.Ring.Basic
import Mathlib.Topology.Algebra.Ring.Real

open CategoryTheory Topology

def realsGlueDataCore'' : TopCat.GlueData.MkCore := by
  constructor
  -- "charts" are parametrized by their origin
  case J => exact ℝ
  -- each "chart" is the whole real line
  case U => intro i; exact (TopCat.of ℝ)
  -- overlap is always the whole real line
  case V => intro i j; exact ⊤
  -- transition maps are translations
  case t =>
    intro orig orig'
    constructor
    constructor
    case hom'.toFun =>
      intro x
      exact ⟨x.val + orig - orig', trivial⟩
    case hom'.continuous_toFun =>
      unfold autoParam
      -- But how do I unpack this goal?
      -- orig orig' : ℝ
      -- ⊢ Continuous fun x ↦ ⟨↑x + orig - orig', trivial⟩
      sorry
  case V_id => sorry
  case t_id => sorry
  case t_inter => sorry

Proving the statement, without the subtype constructor in the function definition is, naturally straightforward:

import Mathlib.Analysis.Normed.Ring.Basic
import Mathlib.Topology.Algebra.Ring.Real

example (orig orig' : ℝ) : Continuous fun x ↦ x + orig - orig' := by continuity
example (orig orig' : ℝ) : Continuous fun x ↦ x + orig - orig' :=
  Continuous.add (Continuous.add continuous_id continuous_const) continuous_const

but I cannot use any of those methods immediately in my previous code. How should I do it then?

[Aaron Liu]

use docs#Topology.IsInducing.continuous_iff with docs#Topology.IsInducing.subtypeVal

[Michał Pacholski]

That's brilliant, thank you!

[Aaron Liu]

that's the universal property :smiling_face:

[Kevin Buzzard]

Here's how I did it. First I isolated the next step and asked Lean what it was called:

example (S : Set ℝ) (X : Type*) [TopologicalSpace X] (f : X → S)
    (hf : Continuous (fun x ↦ (f x).1)) : Continuous f := by
  exact? -- try this: exact continuous_induced_rng.mpr hf

and then I applied the next step and then automation took over:

    case hom'.continuous_toFun =>
      unfold autoParam
      suffices Continuous fun (x : (⊤ : Set ℝ)) ↦ x + orig - orig' from continuous_induced_rng.mpr this
      fun_prop

Aaron's solution is probably better, but I don't know this part of the library at all, I'm just showing you how to figure out how to move ahead when you're in this situation.

[Aaron Liu]

what kind of name is continuous_induced_rng

[Aaron Liu]

is that rng supposed to be "range"

[Aaron Liu]

that should probably be renamed?

[Kevin Buzzard]

I suspect "range" is more likely than "random number generator" yes.

[Michał Pacholski]

@Kevin Buzzard it's a very clever trick. Now I see that continuous_induced_rng.mpr was there also when I tried apply? on the goal, but I didn't notice that among the options.