[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
e : α ≃ β
h₁ : UniformContinuous e.toFun
h₂ : UniformContinuous e.invFun
e' : α ≃ β
h₁' : UniformContinuous e'.toFun
h₂' : UniformContinuous e'.invFun
h :
  { toEquiv := e, uniformContinuous_toFun := h₁, uniformContinuous_invFun := h₂ }.toEquiv =
    { toEquiv := e', uniformContinuous_toFun := h₁', uniformContinuous_invFun := h₂' }.toEquiv
⊢ { toEquiv := e, uniformContinuous_toFun := h₁, uniformContinuous_invFun := h₂ } =
    { toEquiv := e', uniformContinuous_toFun := h₁', uniformContinuous_invFun := h₂' }
[PROOFSTEP]
simpa only [mk.injEq]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g ↑f
x : β
⊢ ↑(UniformEquiv.symm f) (↑f (g x)) = ↑(UniformEquiv.symm f) x
[PROOFSTEP]
rw [hg x]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g ↑f
this : g = ↑(UniformEquiv.symm f)
⊢ Function.LeftInverse g ↑f
[PROOFSTEP]
convert f.left_inv
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g ↑f
this : g = ↑(UniformEquiv.symm f)
⊢ Function.RightInverse g ↑f
[PROOFSTEP]
convert f.right_inv using 1
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g ↑f
this : g = ↑(UniformEquiv.symm f)
⊢ UniformContinuous
    { toFun := ↑f, invFun := g, left_inv := (_ : Function.LeftInverse g ↑f),
        right_inv := (_ : Function.RightInverse g ↑f) }.invFun
[PROOFSTEP]
convert f.symm.uniformContinuous
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
h : α ≃ᵤ β
⊢ UniformInducing (↑(UniformEquiv.symm h) ∘ ↑h)
[PROOFSTEP]
simp only [symm_comp_self, uniformInducing_id]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
h : α ≃ᵤ β
⊢ UniformSpace.comap (↑h) inst✝² = inst✝³
[PROOFSTEP]
ext : 1
[GOAL]
case a
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
h : α ≃ᵤ β
⊢ uniformity α = uniformity α
[PROOFSTEP]
exact h.uniformInducing.comap_uniformity
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α → β
hf : UniformEmbedding f
⊢ UniformContinuous (Equiv.ofInjective f (_ : Function.Injective f)).invFun
[PROOFSTEP]
rw [hf.toUniformInducing.uniformContinuous_iff, Equiv.invFun_as_coe, Equiv.self_comp_ofInjective_symm]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α → β
hf : UniformEmbedding f
⊢ UniformContinuous Subtype.val
[PROOFSTEP]
exact uniformContinuous_subtype_val
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
⊢ UniformContinuous (Equiv.prodAssoc α β γ).invFun
[PROOFSTEP]
rw [Equiv.invFun, Equiv.prodAssoc]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
⊢ UniformContinuous
    { toFun := fun p => (p.fst.fst, p.fst.snd, p.snd), invFun := fun p => ((p.fst, p.snd.fst), p.snd.snd),
        left_inv :=
          (_ :
            ∀ (x : (α × β) × γ),
              (fun p => ((p.fst, p.snd.fst), p.snd.snd)) ((fun p => (p.fst.fst, p.fst.snd, p.snd)) x) = x),
        right_inv :=
          (_ :
            ∀ (x : α × β × γ),
              (fun p => (p.fst.fst, p.fst.snd, p.snd)) ((fun p => ((p.fst, p.snd.fst), p.snd.snd)) x) = x) }.2
[PROOFSTEP]
exact
  (uniformContinuous_fst.prod_mk (uniformContinuous_fst.comp uniformContinuous_snd)).prod_mk
    (uniformContinuous_snd.comp uniformContinuous_snd)
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
src✝ : ULift α ≃ α := Equiv.ulift
⊢ UniformContinuous
    { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }.invFun
[PROOFSTEP]
have hf : UniformInducing (@Equiv.ulift.{v, u} α).toFun := ⟨rfl⟩
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
src✝ : ULift α ≃ α := Equiv.ulift
hf : UniformInducing Equiv.ulift.toFun
⊢ UniformContinuous
    { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }.invFun
[PROOFSTEP]
simp_rw [hf.uniformContinuous_iff]
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
src✝ : ULift α ≃ α := Equiv.ulift
hf : UniformInducing Equiv.ulift.toFun
⊢ UniformContinuous (Equiv.ulift.toFun ∘ Equiv.ulift.invFun)
[PROOFSTEP]
exact uniformContinuous_id
[GOAL]
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α ≃ β
hf : UniformInducing ↑f
⊢ UniformContinuous
    (↑f ∘
      { toFun := f.toFun, invFun := f.invFun, left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
          right_inv := (_ : Function.RightInverse f.invFun f.toFun) }.invFun)
[PROOFSTEP]
simpa using uniformContinuous_id
