Theorem: mem_analyticGroupoid (Ray/AnalyticManifold/AnalyticManifold.lean)

State before:
𝕜 : Type
inst✝³ : NontriviallyNormedField 𝕜
E A : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : TopologicalSpace A
I : ModelWithCorners 𝕜 E A
f : PartialHomeomorph A A
⊢ f ∈ analyticGroupoid I ↔
    f ∈ contDiffGroupoid ⊤ I ∧
      (AnalyticOn 𝕜 (↑I ∘ ↑f ∘ ↑I.symm) (↑I.symm ⁻¹' f.source ∩ interior (range ↑I)) ∧
          ↑I ∘ ↑f ∘ ↑I.symm '' (↑I.symm ⁻¹' f.source ∩ interior (range ↑I)) ⊆ interior (range ↑I)) ∧
        AnalyticOn 𝕜 (↑I ∘ ↑f.symm ∘ ↑I.symm) (↑I.symm ⁻¹' f.target ∩ interior (range ↑I)) ∧
          ↑I ∘ ↑f.symm ∘ ↑I.symm '' (↑I.symm ⁻¹' f.target ∩ interior (range ↑I)) ⊆ interior (range ↑I)
Tactic:
rfl
State after:
no goals