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

State before:
𝕜 : Type
inst✝³ : NontriviallyNormedField 𝕜
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
M : Type
inst✝ : TopologicalSpace M
f : PartialHomeomorph M E
⊢ AnalyticOn 𝕜 (↑𝓘(𝕜, E) ∘ ↑(f.symm.trans f) ∘ ↑𝓘(𝕜, E).symm) (↑𝓘(𝕜, E) '' (f.symm.trans f).source)
Tactic:
apply AnalyticOn.congr (f := fun z ↦ z)
State after:
case hs
𝕜 : Type
inst✝³ : NontriviallyNormedField 𝕜
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
M : Type
inst✝ : TopologicalSpace M
f : PartialHomeomorph M E
⊢ IsOpen (↑𝓘(𝕜, E) '' (f.symm.trans f).source)

case hf
𝕜 : Type
inst✝³ : NontriviallyNormedField 𝕜
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
M : Type
inst✝ : TopologicalSpace M
f : PartialHomeomorph M E
⊢ AnalyticOn 𝕜 (fun z => z) (↑𝓘(𝕜, E) '' (f.symm.trans f).source)

case hg
𝕜 : Type
inst✝³ : NontriviallyNormedField 𝕜
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
M : Type
inst✝ : TopologicalSpace M
f : PartialHomeomorph M E
⊢ EqOn (fun z => z) (↑𝓘(𝕜, E) ∘ ↑(f.symm.trans f) ∘ ↑𝓘(𝕜, E).symm) (↑𝓘(𝕜, E) '' (f.symm.trans f).source)

State before:
case hs
𝕜 : Type
inst✝³ : NontriviallyNormedField 𝕜
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
M : Type
inst✝ : TopologicalSpace M
f : PartialHomeomorph M E
⊢ IsOpen (↑𝓘(𝕜, E) '' (f.symm.trans f).source)
Tactic:
simp only [modelWithCornersSelf_coe, id_eq, image_id', PartialHomeomorph.trans_toPartialEquiv,
  PartialHomeomorph.symm_toPartialEquiv, PartialEquiv.trans_source, PartialEquiv.symm_source,
  PartialHomeomorph.coe_coe_symm]
State after:
case hs
𝕜 : Type
inst✝³ : NontriviallyNormedField 𝕜
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
M : Type
inst✝ : TopologicalSpace M
f : PartialHomeomorph M E
⊢ IsOpen (f.target ∩ ↑f.symm ⁻¹' f.source)

State before:
case hs
𝕜 : Type
inst✝³ : NontriviallyNormedField 𝕜
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
M : Type
inst✝ : TopologicalSpace M
f : PartialHomeomorph M E
⊢ IsOpen (f.target ∩ ↑f.symm ⁻¹' f.source)
Tactic:
exact f.isOpen_inter_preimage_symm f.open_source
State after:
no goals

State before:
case hf
𝕜 : Type
inst✝³ : NontriviallyNormedField 𝕜
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
M : Type
inst✝ : TopologicalSpace M
f : PartialHomeomorph M E
⊢ AnalyticOn 𝕜 (fun z => z) (↑𝓘(𝕜, E) '' (f.symm.trans f).source)
Tactic:
exact analyticOn_id _
State after:
no goals

State before:
case hg
𝕜 : Type
inst✝³ : NontriviallyNormedField 𝕜
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
M : Type
inst✝ : TopologicalSpace M
f : PartialHomeomorph M E
⊢ EqOn (fun z => z) (↑𝓘(𝕜, E) ∘ ↑(f.symm.trans f) ∘ ↑𝓘(𝕜, E).symm) (↑𝓘(𝕜, E) '' (f.symm.trans f).source)
Tactic:
intro x m
State after:
case hg
𝕜 : Type
inst✝³ : NontriviallyNormedField 𝕜
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
M : Type
inst✝ : TopologicalSpace M
f : PartialHomeomorph M E
x : E
m : x ∈ ↑𝓘(𝕜, E) '' (f.symm.trans f).source
⊢ (fun z => z) x = (↑𝓘(𝕜, E) ∘ ↑(f.symm.trans f) ∘ ↑𝓘(𝕜, E).symm) x

State before:
case hg
𝕜 : Type
inst✝³ : NontriviallyNormedField 𝕜
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
M : Type
inst✝ : TopologicalSpace M
f : PartialHomeomorph M E
x : E
m : x ∈ ↑𝓘(𝕜, E) '' (f.symm.trans f).source
⊢ (fun z => z) x = (↑𝓘(𝕜, E) ∘ ↑(f.symm.trans f) ∘ ↑𝓘(𝕜, E).symm) x
Tactic:
simp only [modelWithCornersSelf_coe, id, image_id', PartialHomeomorph.trans_toPartialEquiv,
  PartialHomeomorph.symm_toPartialEquiv, PartialEquiv.trans_source, PartialEquiv.symm_source,
  PartialHomeomorph.coe_coe_symm, mem_inter_iff, mem_preimage, Function.comp,
  modelWithCornersSelf_coe_symm, PartialHomeomorph.coe_trans] at m ⊢
State after:
case hg
𝕜 : Type
inst✝³ : NontriviallyNormedField 𝕜
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
M : Type
inst✝ : TopologicalSpace M
f : PartialHomeomorph M E
x : E
m : x ∈ f.target ∧ ↑f.symm x ∈ f.source
⊢ x = ↑f (↑f.symm x)

State before:
case hg
𝕜 : Type
inst✝³ : NontriviallyNormedField 𝕜
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
M : Type
inst✝ : TopologicalSpace M
f : PartialHomeomorph M E
x : E
m : x ∈ f.target ∧ ↑f.symm x ∈ f.source
⊢ x = ↑f (↑f.symm x)
Tactic:
rw [f.right_inv m.1]
State after:
no goals