m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
⊢ ⊤ ≤ contDiffGroupoid 0 I
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
⊢ contDiffGroupoid 0 I = continuousGroupoid H
apply le_antisymm le_top
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ u ∈ (contDiffGroupoid 0 I).members
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
⊢ ⊤ ≤ contDiffGroupoid 0 I
intro u _
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ u ∈ contDiffGroupoid 0 I
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ u ∈ (contDiffGroupoid 0 I).members
change u ∈ contDiffGroupoid 0 I
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ Pregroupoid.property
      {
        property := fun f s =>
          ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I),
        comp :=
          (_ :
            ∀ {f g : H → H} {u v : Set H},
              ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I) →
                ContDiffOn 𝕜 0 (↑I ∘ g ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' v ∩ range ↑I) →
                  IsOpen u →
                    IsOpen v →
                      IsOpen (u ∩ f ⁻¹' v) →
                        (fun f s =>
                            ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I))
                              (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I))
                          (g ∘ f) (u ∩ f ⁻¹' v)),
        id_mem :=
          (_ : ContDiffOn 𝕜 0 (↑I ∘ id ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' univ ∩ range ↑I)),
        locality :=
          (_ :
            ∀ {f : H → H} {u : Set H},
              IsOpen u →
                (∀ (x : H),
                    x ∈ u →
                      ∃ v,
                        IsOpen v ∧
                          x ∈ v ∧
                            (fun f s =>
                                ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I))
                                  (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I))
                              f (u ∩ v)) →
                  ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I)),
        congr :=
          (_ :
            ∀ {f g : H → H} {u : Set H},
              IsOpen u →
                (∀ (x : H), x ∈ u → g x = f x) →
                  ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I) →
                    ContDiffOn 𝕜 0 (↑I ∘ g ∘ ↑(ModelWithCorners.symm I))
                      (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I)) }
      (↑u) u.source ∧
    Pregroupoid.property
      {
        property := fun f s =>
          ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I),
        comp :=
          (_ :
            ∀ {f g : H → H} {u v : Set H},
              ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I) →
                ContDiffOn 𝕜 0 (↑I ∘ g ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' v ∩ range ↑I) →
                  IsOpen u →
                    IsOpen v →
                      IsOpen (u ∩ f ⁻¹' v) →
                        (fun f s =>
                            ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I))
                              (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I))
                          (g ∘ f) (u ∩ f ⁻¹' v)),
        id_mem :=
          (_ : ContDiffOn 𝕜 0 (↑I ∘ id ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' univ ∩ range ↑I)),
        locality :=
          (_ :
            ∀ {f : H → H} {u : Set H},
              IsOpen u →
                (∀ (x : H),
                    x ∈ u →
                      ∃ v,
                        IsOpen v ∧
                          x ∈ v ∧
                            (fun f s =>
                                ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I))
                                  (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I))
                              f (u ∩ v)) →
                  ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I)),
        congr :=
          (_ :
            ∀ {f g : H → H} {u : Set H},
              IsOpen u →
                (∀ (x : H), x ∈ u → g x = f x) →
                  ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I) →
                    ContDiffOn 𝕜 0 (↑I ∘ g ∘ ↑(ModelWithCorners.symm I))
                      (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I)) }
      (↑(LocalHomeomorph.symm u)) u.target
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ u ∈ contDiffGroupoid 0 I
rw [contDiffGroupoid, mem_groupoid_of_pregroupoid]
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ ContinuousOn (↑I ∘ ↑u ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u.source ∩ range ↑I) ∧
    ContinuousOn (↑I ∘ ↑(LocalHomeomorph.symm u) ∘ ↑(ModelWithCorners.symm I))
      (↑(ModelWithCorners.symm I) ⁻¹' u.target ∩ range ↑I)
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ Pregroupoid.property
      {
        property := fun f s =>
          ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I),
        comp :=
          (_ :
            ∀ {f g : H → H} {u v : Set H},
              ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I) →
                ContDiffOn 𝕜 0 (↑I ∘ g ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' v ∩ range ↑I) →
                  IsOpen u →
                    IsOpen v →
                      IsOpen (u ∩ f ⁻¹' v) →
                        (fun f s =>
                            ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I))
                              (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I))
                          (g ∘ f) (u ∩ f ⁻¹' v)),
        id_mem :=
          (_ : ContDiffOn 𝕜 0 (↑I ∘ id ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' univ ∩ range ↑I)),
        locality :=
          (_ :
            ∀ {f : H → H} {u : Set H},
              IsOpen u →
                (∀ (x : H),
                    x ∈ u →
                      ∃ v,
                        IsOpen v ∧
                          x ∈ v ∧
                            (fun f s =>
                                ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I))
                                  (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I))
                              f (u ∩ v)) →
                  ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I)),
        congr :=
          (_ :
            ∀ {f g : H → H} {u : Set H},
              IsOpen u →
                (∀ (x : H), x ∈ u → g x = f x) →
                  ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I) →
                    ContDiffOn 𝕜 0 (↑I ∘ g ∘ ↑(ModelWithCorners.symm I))
                      (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I)) }
      (↑u) u.source ∧
    Pregroupoid.property
      {
        property := fun f s =>
          ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I),
        comp :=
          (_ :
            ∀ {f g : H → H} {u v : Set H},
              ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I) →
                ContDiffOn 𝕜 0 (↑I ∘ g ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' v ∩ range ↑I) →
                  IsOpen u →
                    IsOpen v →
                      IsOpen (u ∩ f ⁻¹' v) →
                        (fun f s =>
                            ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I))
                              (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I))
                          (g ∘ f) (u ∩ f ⁻¹' v)),
        id_mem :=
          (_ : ContDiffOn 𝕜 0 (↑I ∘ id ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' univ ∩ range ↑I)),
        locality :=
          (_ :
            ∀ {f : H → H} {u : Set H},
              IsOpen u →
                (∀ (x : H),
                    x ∈ u →
                      ∃ v,
                        IsOpen v ∧
                          x ∈ v ∧
                            (fun f s =>
                                ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I))
                                  (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I))
                              f (u ∩ v)) →
                  ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I)),
        congr :=
          (_ :
            ∀ {f g : H → H} {u : Set H},
              IsOpen u →
                (∀ (x : H), x ∈ u → g x = f x) →
                  ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I) →
                    ContDiffOn 𝕜 0 (↑I ∘ g ∘ ↑(ModelWithCorners.symm I))
                      (↑(ModelWithCorners.symm I) ⁻¹' u ∩ range ↑I)) }
      (↑(LocalHomeomorph.symm u)) u.target
simp only [contDiffOn_zero]
case left
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ ContinuousOn (↑I ∘ ↑u ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u.source ∩ range ↑I)

case right
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ ContinuousOn (↑I ∘ ↑(LocalHomeomorph.symm u) ∘ ↑(ModelWithCorners.symm I))
    (↑(ModelWithCorners.symm I) ⁻¹' u.target ∩ range ↑I)
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ ContinuousOn (↑I ∘ ↑u ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u.source ∩ range ↑I) ∧
    ContinuousOn (↑I ∘ ↑(LocalHomeomorph.symm u) ∘ ↑(ModelWithCorners.symm I))
      (↑(ModelWithCorners.symm I) ⁻¹' u.target ∩ range ↑I)
constructor
case left
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ MapsTo (↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u.source ∩ range ↑I) u.source
case left
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ ContinuousOn (↑I ∘ ↑u ∘ ↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u.source ∩ range ↑I)
refine' I.continuous.comp_continuousOn (u.continuousOn.comp I.continuousOn_symm _)
no goals
case left
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ MapsTo (↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u.source ∩ range ↑I) u.source
exact (mapsTo_preimage _ _).mono_left (inter_subset_left _ _)
case right
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ MapsTo (↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u.target ∩ range ↑I)
    (LocalHomeomorph.symm u).toLocalEquiv.source
case right
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ ContinuousOn (↑I ∘ ↑(LocalHomeomorph.symm u) ∘ ↑(ModelWithCorners.symm I))
    (↑(ModelWithCorners.symm I) ⁻¹' u.target ∩ range ↑I)
refine' I.continuous.comp_continuousOn (u.symm.continuousOn.comp I.continuousOn_symm _)
no goals
case right
m n : ℕ∞
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_1
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type ?u.100926
inst✝ : TopologicalSpace M
u : LocalHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ MapsTo (↑(ModelWithCorners.symm I)) (↑(ModelWithCorners.symm I) ⁻¹' u.target ∩ range ↑I)
    (LocalHomeomorph.symm u).toLocalEquiv.source
exact (mapsTo_preimage _ _).mono_left (inter_subset_left _ _)