internlm/Lean-Github huggingface dataset:
Theorem: analyticGroupoid_prod
Proof state before:
case refine_1.hg
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace A
F B : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
I : ModelWithCorners 𝕜 E A
J : ModelWithCorners 𝕜 F B
f : PartialHomeomorph A A
g : PartialHomeomorph B B
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
ei : interior (range fun x => (↑I x.1, ↑J x.2)) = interior (range ↑I) ×ˢ interior (range ↑J)
fa :
  f ∈ contDiffGroupoid ⊤ I ∧
    (AnalyticOn 𝕜 (fun x => ↑I (↑f (↑I.symm x))) (↑I.symm ⁻¹' f.source ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.source ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f (↑I.symm x))) ⁻¹' interior (range ↑I)) ∧
      AnalyticOn 𝕜 (fun x => ↑I (↑f.symm (↑I.symm x))) (↑I.symm ⁻¹' f.target ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.target ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f.symm (↑I.symm x))) ⁻¹' interior (range ↑I)
ga :
  g ∈ contDiffGroupoid ⊤ J ∧
    (AnalyticOn 𝕜 (fun x => ↑J (↑g (↑J.symm x))) (↑J.symm ⁻¹' g.source ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.source ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g (↑J.symm x))) ⁻¹' interior (range ↑J)) ∧
      AnalyticOn 𝕜 (fun x => ↑J (↑g.symm (↑J.symm x))) (↑J.symm ⁻¹' g.target ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.target ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g.symm (↑J.symm x))) ⁻¹' interior (range ↑J)
x : E × F
m : (↑I.symm x.1 ∈ f.source ∧ ↑J.symm x.2 ∈ g.source) ∧ x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ ↑J.symm x.2 ∈ g.source ∧ x.2 ∈ interior (range ↑J)
Tactic:
exact ⟨m.1.2, (subset_of_eq ei m.2).2⟩
Proof state after:
no goals
Theorem: analyticGroupoid_prod
Proof state before:
case refine_2
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace A
F B : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
I : ModelWithCorners 𝕜 E A
J : ModelWithCorners 𝕜 F B
f : PartialHomeomorph A A
g : PartialHomeomorph B B
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
ei : interior (range fun x => (↑I x.1, ↑J x.2)) = interior (range ↑I) ×ˢ interior (range ↑J)
fa :
  f ∈ contDiffGroupoid ⊤ I ∧
    (AnalyticOn 𝕜 (fun x => ↑I (↑f (↑I.symm x))) (↑I.symm ⁻¹' f.source ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.source ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f (↑I.symm x))) ⁻¹' interior (range ↑I)) ∧
      AnalyticOn 𝕜 (fun x => ↑I (↑f.symm (↑I.symm x))) (↑I.symm ⁻¹' f.target ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.target ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f.symm (↑I.symm x))) ⁻¹' interior (range ↑I)
ga :
  g ∈ contDiffGroupoid ⊤ J ∧
    (AnalyticOn 𝕜 (fun x => ↑J (↑g (↑J.symm x))) (↑J.symm ⁻¹' g.source ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.source ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g (↑J.symm x))) ⁻¹' interior (range ↑J)) ∧
      AnalyticOn 𝕜 (fun x => ↑J (↑g.symm (↑J.symm x))) (↑J.symm ⁻¹' g.target ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.target ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g.symm (↑J.symm x))) ⁻¹' interior (range ↑J)
x : E × F
m0 : x ∈ (fun x => ↑I.symm x.1) ⁻¹' f.source
m1 : x ∈ (fun x => ↑J.symm x.2) ⁻¹' g.source
m2 : x ∈ interior (range ↑I) ×ˢ interior (range ↑J)
⊢ x ∈ (fun x => (↑I (↑f (↑I.symm x.1)), ↑J (↑g (↑J.symm x.2)))) ⁻¹' interior (range fun x => (↑I x.1, ↑J x.2))
Tactic:
exact subset_of_eq ei.symm ⟨fa.2.1.2 ⟨m0,m2.1⟩, ga.2.1.2 ⟨m1,m2.2⟩⟩
Proof state after:
no goals
Theorem: analyticGroupoid_prod
Proof state before:
case refine_3.hf
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace A
F B : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
I : ModelWithCorners 𝕜 E A
J : ModelWithCorners 𝕜 F B
f : PartialHomeomorph A A
g : PartialHomeomorph B B
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
ei : interior (range fun x => (↑I x.1, ↑J x.2)) = interior (range ↑I) ×ˢ interior (range ↑J)
fa :
  f ∈ contDiffGroupoid ⊤ I ∧
    (AnalyticOn 𝕜 (fun x => ↑I (↑f (↑I.symm x))) (↑I.symm ⁻¹' f.source ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.source ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f (↑I.symm x))) ⁻¹' interior (range ↑I)) ∧
      AnalyticOn 𝕜 (fun x => ↑I (↑f.symm (↑I.symm x))) (↑I.symm ⁻¹' f.target ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.target ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f.symm (↑I.symm x))) ⁻¹' interior (range ↑I)
ga :
  g ∈ contDiffGroupoid ⊤ J ∧
    (AnalyticOn 𝕜 (fun x => ↑J (↑g (↑J.symm x))) (↑J.symm ⁻¹' g.source ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.source ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g (↑J.symm x))) ⁻¹' interior (range ↑J)) ∧
      AnalyticOn 𝕜 (fun x => ↑J (↑g.symm (↑J.symm x))) (↑J.symm ⁻¹' g.target ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.target ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g.symm (↑J.symm x))) ⁻¹' interior (range ↑J)
x : E × F
m : (↑I.symm x.1 ∈ f.target ∧ ↑J.symm x.2 ∈ g.target) ∧ x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ ↑I.symm x.1 ∈ f.target ∧ x.1 ∈ interior (range ↑I)
Tactic:
exact ⟨m.1.1, (subset_of_eq ei m.2).1⟩
Proof state after:
no goals
Theorem: analyticGroupoid_prod
Proof state before:
case refine_3.hg
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace A
F B : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
I : ModelWithCorners 𝕜 E A
J : ModelWithCorners 𝕜 F B
f : PartialHomeomorph A A
g : PartialHomeomorph B B
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
ei : interior (range fun x => (↑I x.1, ↑J x.2)) = interior (range ↑I) ×ˢ interior (range ↑J)
fa :
  f ∈ contDiffGroupoid ⊤ I ∧
    (AnalyticOn 𝕜 (fun x => ↑I (↑f (↑I.symm x))) (↑I.symm ⁻¹' f.source ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.source ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f (↑I.symm x))) ⁻¹' interior (range ↑I)) ∧
      AnalyticOn 𝕜 (fun x => ↑I (↑f.symm (↑I.symm x))) (↑I.symm ⁻¹' f.target ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.target ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f.symm (↑I.symm x))) ⁻¹' interior (range ↑I)
ga :
  g ∈ contDiffGroupoid ⊤ J ∧
    (AnalyticOn 𝕜 (fun x => ↑J (↑g (↑J.symm x))) (↑J.symm ⁻¹' g.source ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.source ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g (↑J.symm x))) ⁻¹' interior (range ↑J)) ∧
      AnalyticOn 𝕜 (fun x => ↑J (↑g.symm (↑J.symm x))) (↑J.symm ⁻¹' g.target ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.target ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g.symm (↑J.symm x))) ⁻¹' interior (range ↑J)
x : E × F
m : (↑I.symm x.1 ∈ f.target ∧ ↑J.symm x.2 ∈ g.target) ∧ x ∈ interior (range fun x => (↑I x.1, ↑J x.2))
⊢ ↑J.symm x.2 ∈ g.target ∧ x.2 ∈ interior (range ↑J)
Tactic:
exact ⟨m.1.2, (subset_of_eq ei m.2).2⟩
Proof state after:
no goals
Theorem: analyticGroupoid_prod
Proof state before:
case refine_4
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace A
F B : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
I : ModelWithCorners 𝕜 E A
J : ModelWithCorners 𝕜 F B
f : PartialHomeomorph A A
g : PartialHomeomorph B B
er : (range fun x => (↑I x.1, ↑J x.2)) = range ↑I ×ˢ range ↑J
ei : interior (range fun x => (↑I x.1, ↑J x.2)) = interior (range ↑I) ×ˢ interior (range ↑J)
fa :
  f ∈ contDiffGroupoid ⊤ I ∧
    (AnalyticOn 𝕜 (fun x => ↑I (↑f (↑I.symm x))) (↑I.symm ⁻¹' f.source ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.source ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f (↑I.symm x))) ⁻¹' interior (range ↑I)) ∧
      AnalyticOn 𝕜 (fun x => ↑I (↑f.symm (↑I.symm x))) (↑I.symm ⁻¹' f.target ∩ interior (range ↑I)) ∧
        ↑I.symm ⁻¹' f.target ∩ interior (range ↑I) ⊆ (fun x => ↑I (↑f.symm (↑I.symm x))) ⁻¹' interior (range ↑I)
ga :
  g ∈ contDiffGroupoid ⊤ J ∧
    (AnalyticOn 𝕜 (fun x => ↑J (↑g (↑J.symm x))) (↑J.symm ⁻¹' g.source ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.source ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g (↑J.symm x))) ⁻¹' interior (range ↑J)) ∧
      AnalyticOn 𝕜 (fun x => ↑J (↑g.symm (↑J.symm x))) (↑J.symm ⁻¹' g.target ∩ interior (range ↑J)) ∧
        ↑J.symm ⁻¹' g.target ∩ interior (range ↑J) ⊆ (fun x => ↑J (↑g.symm (↑J.symm x))) ⁻¹' interior (range ↑J)
x : E × F
m0 : x ∈ (fun x => ↑I.symm x.1) ⁻¹' f.target
m1 : x ∈ (fun x => ↑J.symm x.2) ⁻¹' g.target
m2 : x ∈ interior (range ↑I) ×ˢ interior (range ↑J)
⊢ x ∈
    (fun x =>
        (↑I (↑(f.prod g).symm (↑I.symm x.1, ↑J.symm x.2)).1, ↑J (↑(f.prod g).symm (↑I.symm x.1, ↑J.symm x.2)).2)) ⁻¹'
      interior (range fun x => (↑I x.1, ↑J x.2))
Tactic:
exact subset_of_eq ei.symm ⟨fa.2.2.2 ⟨m0,m2.1⟩, ga.2.2.2 ⟨m1,m2.2⟩⟩
Proof state after:
no goals
Theorem: extChartAt_self_analytic
Proof 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)
Proof 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)
Theorem: extChartAt_self_analytic
Proof 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]
Proof 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)
Theorem: extChartAt_self_analytic
Proof 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
Proof state after:
no goals
Theorem: extChartAt_self_analytic
Proof 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 _
Proof state after:
no goals
Theorem: extChartAt_self_analytic
Proof 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
Proof 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
Theorem: extChartAt_self_analytic
Proof 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 ⊢
Proof 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)
Theorem: extChartAt_self_analytic
Proof 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]
Proof state after:
no goals
Theorem: holomorphicAt_iff
Proof state before:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
x : M
⊢ HolomorphicAt I J f x ↔
    ContinuousAt f x ∧ AnalyticAt 𝕜 (↑(extChartAt J (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Tactic:
simp only [HolomorphicAt, ChartedSpace.liftPropAt_iff, extChartAt, PartialHomeomorph.extend_coe,
  PartialHomeomorph.extend_coe_symm, Function.comp]
Proof state after:
no goals
Theorem: holomorphic_iff
Proof state before:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
⊢ Holomorphic I J f ↔
    Continuous f ∧ ∀ (x : M), AnalyticAt 𝕜 (↑(extChartAt J (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Tactic:
simp only [Holomorphic, holomorphicAt_iff, continuous_iff_continuousAt]
Proof state after:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
⊢ (∀ (x : M),
      ContinuousAt f x ∧ AnalyticAt 𝕜 (↑(extChartAt J (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)) ↔
    (∀ (x : M), ContinuousAt f x) ∧
      ∀ (x : M), AnalyticAt 𝕜 (↑(extChartAt J (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Theorem: holomorphic_iff
Proof state before:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
⊢ (∀ (x : M),
      ContinuousAt f x ∧ AnalyticAt 𝕜 (↑(extChartAt J (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)) ↔
    (∀ (x : M), ContinuousAt f x) ∧
      ∀ (x : M), AnalyticAt 𝕜 (↑(extChartAt J (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Tactic:
exact forall_and
Proof state after:
no goals
Theorem: analyticAt_iff_holomorphicAt
Proof state before:
𝕜 : Type
inst✝³² : NontriviallyNormedField 𝕜
E A : Type
inst✝³¹ : NormedAddCommGroup E
inst✝³⁰ : NormedSpace 𝕜 E
inst✝²⁹ : CompleteSpace E
inst✝²⁸ : TopologicalSpace A
F B : Type
inst✝²⁷ : NormedAddCommGroup F
inst✝²⁶ : NormedSpace 𝕜 F
inst✝²⁵ : CompleteSpace F
inst✝²⁴ : TopologicalSpace B
G C : Type
inst✝²³ : NormedAddCommGroup G
inst✝²² : NormedSpace 𝕜 G
inst✝²¹ : TopologicalSpace C
H D : Type
inst✝²⁰ : NormedAddCommGroup H
inst✝¹⁹ : NormedSpace 𝕜 H
inst✝¹⁸ : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹⁷ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁶ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹⁵ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹⁴ : TopologicalSpace P
inst✝¹³ : I.Boundaryless
inst✝¹² : ChartedSpace A M
cm : AnalyticManifold I M
inst✝¹¹ : J.Boundaryless
inst✝¹⁰ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁹ : K.Boundaryless
inst✝⁸ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁷ : L.Boundaryless
inst✝⁶ : ChartedSpace D P
cp : AnalyticManifold L P
inst✝⁵ : ChartedSpace A E
inst✝⁴ : AnalyticManifold I E
inst✝³ : ChartedSpace B F
inst✝² : AnalyticManifold J F
inst✝¹ : ExtChartEqRefl I
inst✝ : ExtChartEqRefl J
f : E → F
x : E
⊢ AnalyticAt 𝕜 f x ↔ HolomorphicAt I J f x
Tactic:
simp only [holomorphicAt_iff, extChartAt_eq_refl, PartialEquiv.refl_coe, PartialEquiv.refl_symm,
  Function.id_comp, Function.comp_id, id_eq, iff_and_self]
Proof state after:
𝕜 : Type
inst✝³² : NontriviallyNormedField 𝕜
E A : Type
inst✝³¹ : NormedAddCommGroup E
inst✝³⁰ : NormedSpace 𝕜 E
inst✝²⁹ : CompleteSpace E
inst✝²⁸ : TopologicalSpace A
F B : Type
inst✝²⁷ : NormedAddCommGroup F
inst✝²⁶ : NormedSpace 𝕜 F
inst✝²⁵ : CompleteSpace F
inst✝²⁴ : TopologicalSpace B
G C : Type
inst✝²³ : NormedAddCommGroup G
inst✝²² : NormedSpace 𝕜 G
inst✝²¹ : TopologicalSpace C
H D : Type
inst✝²⁰ : NormedAddCommGroup H
inst✝¹⁹ : NormedSpace 𝕜 H
inst✝¹⁸ : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹⁷ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁶ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹⁵ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹⁴ : TopologicalSpace P
inst✝¹³ : I.Boundaryless
inst✝¹² : ChartedSpace A M
cm : AnalyticManifold I M
inst✝¹¹ : J.Boundaryless
inst✝¹⁰ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁹ : K.Boundaryless
inst✝⁸ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁷ : L.Boundaryless
inst✝⁶ : ChartedSpace D P
cp : AnalyticManifold L P
inst✝⁵ : ChartedSpace A E
inst✝⁴ : AnalyticManifold I E
inst✝³ : ChartedSpace B F
inst✝² : AnalyticManifold J F
inst✝¹ : ExtChartEqRefl I
inst✝ : ExtChartEqRefl J
f : E → F
x : E
⊢ AnalyticAt 𝕜 f x → ContinuousAt f x
Theorem: analyticAt_iff_holomorphicAt
Proof state before:
𝕜 : Type
inst✝³² : NontriviallyNormedField 𝕜
E A : Type
inst✝³¹ : NormedAddCommGroup E
inst✝³⁰ : NormedSpace 𝕜 E
inst✝²⁹ : CompleteSpace E
inst✝²⁸ : TopologicalSpace A
F B : Type
inst✝²⁷ : NormedAddCommGroup F
inst✝²⁶ : NormedSpace 𝕜 F
inst✝²⁵ : CompleteSpace F
inst✝²⁴ : TopologicalSpace B
G C : Type
inst✝²³ : NormedAddCommGroup G
inst✝²² : NormedSpace 𝕜 G
inst✝²¹ : TopologicalSpace C
H D : Type
inst✝²⁰ : NormedAddCommGroup H
inst✝¹⁹ : NormedSpace 𝕜 H
inst✝¹⁸ : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹⁷ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁶ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹⁵ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹⁴ : TopologicalSpace P
inst✝¹³ : I.Boundaryless
inst✝¹² : ChartedSpace A M
cm : AnalyticManifold I M
inst✝¹¹ : J.Boundaryless
inst✝¹⁰ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁹ : K.Boundaryless
inst✝⁸ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁷ : L.Boundaryless
inst✝⁶ : ChartedSpace D P
cp : AnalyticManifold L P
inst✝⁵ : ChartedSpace A E
inst✝⁴ : AnalyticManifold I E
inst✝³ : ChartedSpace B F
inst✝² : AnalyticManifold J F
inst✝¹ : ExtChartEqRefl I
inst✝ : ExtChartEqRefl J
f : E → F
x : E
⊢ AnalyticAt 𝕜 f x → ContinuousAt f x
Tactic:
exact AnalyticAt.continuousAt
Proof state after:
no goals