𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h :
  ∀ (e e' : LocalHomeomorph M H),
    e ∈ atlas H M →
      e' ∈ atlas H M →
        ContDiffOn 𝕜 ⊤ (↑I ∘ ↑(LocalHomeomorph.symm e ≫ₕ e') ∘ ↑(ModelWithCorners.symm I))
          (↑(ModelWithCorners.symm I) ⁻¹' (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source ∩ range ↑I)
this : HasGroupoid M (contDiffGroupoid ⊤ I)
⊢ ∀ {e e' : LocalHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → LocalHomeomorph.symm e ≫ₕ e' ∈ contDiffGroupoid ⊤ I
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h :
  ∀ (e e' : LocalHomeomorph M H),
    e ∈ atlas H M →
      e' ∈ atlas H M →
        ContDiffOn 𝕜 ⊤ (↑I ∘ ↑(LocalHomeomorph.symm e ≫ₕ e') ∘ ↑(ModelWithCorners.symm I))
          (↑(ModelWithCorners.symm I) ⁻¹' (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source ∩ range ↑I)
⊢ ∀ {e e' : LocalHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → LocalHomeomorph.symm e ≫ₕ e' ∈ contDiffGroupoid ⊤ I
haveI : HasGroupoid M (contDiffGroupoid ∞ I) := hasGroupoid_of_pregroupoid _ (h _ _)
no goals
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h :
  ∀ (e e' : LocalHomeomorph M H),
    e ∈ atlas H M →
      e' ∈ atlas H M →
        ContDiffOn 𝕜 ⊤ (↑I ∘ ↑(LocalHomeomorph.symm e ≫ₕ e') ∘ ↑(ModelWithCorners.symm I))
          (↑(ModelWithCorners.symm I) ⁻¹' (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source ∩ range ↑I)
this : HasGroupoid M (contDiffGroupoid ⊤ I)
⊢ ∀ {e e' : LocalHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → LocalHomeomorph.symm e ≫ₕ e' ∈ contDiffGroupoid ⊤ I
apply StructureGroupoid.compatible