-- Mathlib/Geometry/Manifold/AnalyticManifold.lean
theorem ofSet_mem_analyticGroupoid {s : Set H} (hs : IsOpen s) :
    PartialHomeomorph.ofSet s hs ∈ analyticGroupoid I

Proof state:
𝕜 : 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
⊢ AnalyticOn 𝕜 (↑I ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)

Tactic:
have hi : AnalyticOn 𝕜 id (univ : Set E) := analyticOn_id

Result:
𝕜 : 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
hi : AnalyticOn 𝕜 id univ
⊢ AnalyticOn 𝕜 (↑I ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)

Proof state:
𝕜 : 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 ∈ analyticGroupoid I

Tactic:
rw [analyticGroupoid, mem_groupoid_of_pregroupoid]

Result:
𝕜 : 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
⊢ (analyticPregroupoid I).property (↑(PartialHomeomorph.ofSet s hs)) (PartialHomeomorph.ofSet s hs).source ∧
    (analyticPregroupoid I).property (↑(PartialHomeomorph.ofSet s hs).symm) (PartialHomeomorph.ofSet s hs).target

Proof state:
𝕜 : 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 : AnalyticOn 𝕜 (↑I ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)
⊢ (analyticPregroupoid I).property (↑(PartialHomeomorph.ofSet s hs)) (PartialHomeomorph.ofSet s hs).source ∧
    (analyticPregroupoid I).property (↑(PartialHomeomorph.ofSet s hs).symm) (PartialHomeomorph.ofSet s hs).target

Tactic:
simp [h, analyticPregroupoid]

Result:
no goals

Proof state:
𝕜 : 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
hi : AnalyticOn 𝕜 id univ
⊢ AnalyticOn 𝕜 (↑I ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)

Tactic:
exact (hi.mono (subset_univ _)).congr (fun x hx ↦ I.right_inv hx.2)

Result:
no goals

Proof state:
𝕜 : 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
⊢ (analyticPregroupoid I).property (↑(PartialHomeomorph.ofSet s hs)) (PartialHomeomorph.ofSet s hs).source ∧
    (analyticPregroupoid I).property (↑(PartialHomeomorph.ofSet s hs).symm) (PartialHomeomorph.ofSet s hs).target

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

Result:
𝕜 : 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
⊢ AnalyticOn 𝕜 (↑I ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)