Domain and range of functions in composition.

Stream: new members

[Jeff Lee]

Hello! I am trying to prove that the composition of two PartialHomeomorph's are continuous on an obvious domain. However, I am having trouble making Lean realize that the range of the first function in the composition is equal to the domain of the second function in the composition when trying to use .comp:

import Mathlib.Tactic

open Set Function

/- X is a connected Hausdorff space -/
variable (X : Type*) [TopologicalSpace X] [ConnectedSpace X] [T2Space X]

/- Transition function continuous on reasonable domain. -/
lemma continuous_transition (a b : ℝ) (φ ψ : PartialHomeomorph X ℝ) (hCover : φ.source ∪ ψ.source = univ)
    (hφ : φ.target = univ) (hψ : ψ.target = univ) (hA : φ '' (φ.source ∩ ψ.source) = Iio a) (hB : ψ '' (φ.source ∩ ψ.source) = Ioi b) : Continuous ((Iio a).restrict (ψ ∘ φ.symm)) := by
  have hψCont : Continuous ((φ.symm '' (Iio a)).restrict ψ) := by
    refine ContinuousOn.restrict ?_
    have ψCont' : ContinuousOn ψ (ψ.source) := PartialHomeomorph.continuousOn ψ
    have : (↑φ.symm '' Iio a) ⊆ ψ.source := by
      rw [← hA]
      have : φ.symm '' (φ '' (φ.source ∩ ψ.source)) = φ.source ∩ ψ.source := by
        have : ∀ (x : (φ.source ∩ ψ.source : Set X)), φ.symm (φ (x)) = x := by
          intro x
          apply φ.left_inv
          -- simp_all only [ne_eq, inter_eq_right, not_false_eq_true, mem_Iio, or_true, implies_true]
          obtain ⟨val, property⟩ := x
          simp only
          exact mem_of_mem_inter_left property
        ext z
        simp only [mem_image, mem_inter_iff, exists_exists_and_eq_and]
        constructor
        · rintro ⟨x, ⟨hxφ, hxψ⟩, rfl⟩
          aesop
        · intro hz
          use z
          refine and_assoc.mpr ?_
          aesop
      rw [this]
      exact inter_subset_right

    exact ContinuousOn.mono ψCont' this

  have hφCont : Continuous ((Iio a).restrict φ.symm) := by
    refine ContinuousOn.restrict ?_
    have φCont' : ContinuousOn φ.symm φ.target := PartialHomeomorph.continuousOn_symm φ
    have : Iio a ⊆ φ.target := by
      rw [← hA]
      aesop
    exact ContinuousOn.mono φCont' this

  -- I would like to use obtain h := hψCont.comp hφCont, but it fails,
  -- which I assume is due to the fact that Lean needs the range of the first function in the composition
  -- to be equal to the domain of the second function in the composition.
  sorry

Should I define a new function of the type I want, specifying my desired domain and range or can I just include a proof that the range of the first function is equal to the domain of the second function and trust that Lean will figure it out by itself? Please let me know what the best way to approach this is. Thank you!

[Matt Diamond]

I would suggest defining f and g first and making sure they have the expected types. Lean thinks the codomain of (Iio a).restrict φ.symm is X and the domain of (φ.symm '' (Iio a)).restrict ψ is (φ.symm '' (Iio a)), so you would need to prove that those are in fact equal.