-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem ofSet_mem_contDiffGroupoid {s : Set H} (hs : IsOpen s) :
    PartialHomeomorph.ofSet s hs ∈ contDiffGroupoid n I

Proof state:
n : WithTop ℕ∞
𝕜 : 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
s : Set H
hs : IsOpen s
⊢ PartialHomeomorph.ofSet s hs ∈ contDiffGroupoid n I

Tactic:
rw [contDiffGroupoid, mem_groupoid_of_pregroupoid]

Result:
n : WithTop ℕ∞
𝕜 : 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
s : Set H
hs : IsOpen s
⊢ (contDiffPregroupoid n I).property (↑(PartialHomeomorph.ofSet s hs)) (PartialHomeomorph.ofSet s hs).source ∧
    (contDiffPregroupoid n I).property (↑(PartialHomeomorph.ofSet s hs).symm) (PartialHomeomorph.ofSet s hs).target

Proof state:
n : WithTop ℕ∞
𝕜 : 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
s : Set H
hs : IsOpen s
⊢ (contDiffPregroupoid n I).property (↑(PartialHomeomorph.ofSet s hs)) (PartialHomeomorph.ofSet s hs).source ∧
    (contDiffPregroupoid n I).property (↑(PartialHomeomorph.ofSet s hs).symm) (PartialHomeomorph.ofSet s hs).target

Tactic:
suffices h : ContDiffOn 𝕜 n (I ∘ I.symm) (I.symm ⁻¹' s ∩ range I) by
  simp [h, contDiffPregroupoid]

Result:
n : WithTop ℕ∞
𝕜 : 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
s : Set H
hs : IsOpen s
⊢ ContDiffOn 𝕜 n (↑I ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)

Proof state:
n : WithTop ℕ∞
𝕜 : 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
s : Set H
hs : IsOpen s
⊢ ContDiffOn 𝕜 n (↑I ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)

Tactic:
have : ContDiffOn 𝕜 n id (univ : Set E) := contDiff_id.contDiffOn

Result:
n : WithTop ℕ∞
𝕜 : 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
s : Set H
hs : IsOpen s
this : ContDiffOn 𝕜 n id univ
⊢ ContDiffOn 𝕜 n (↑I ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)

Proof state:
n : WithTop ℕ∞
𝕜 : 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
s : Set H
hs : IsOpen s
this : ContDiffOn 𝕜 n id univ
⊢ ContDiffOn 𝕜 n (↑I ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)

Tactic:
exact this.congr_mono (fun x hx => I.right_inv hx.2) (subset_univ _)

Result:
no goals

Proof state:
n : WithTop ℕ∞
𝕜 : 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
s : Set H
hs : IsOpen s
h : ContDiffOn 𝕜 n (↑I ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)
⊢ (contDiffPregroupoid n I).property (↑(PartialHomeomorph.ofSet s hs)) (PartialHomeomorph.ofSet s hs).source ∧
    (contDiffPregroupoid n I).property (↑(PartialHomeomorph.ofSet s hs).symm) (PartialHomeomorph.ofSet s hs).target

Tactic:
simp [h, contDiffPregroupoid]

Result:
no goals