internlm/Lean-Github huggingface dataset:
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
case hX.intro.intro.intro.refine_1
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ IsClosed (ball x r)

case hX.intro.intro.intro.refine_2
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ x ∈ ball x r ∧ y ∉ ball x r
Tactic:
rw [e]
Proof state after:
case hX.intro.intro.intro.refine_1
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ IsClosed (closedBall x r)

case hX.intro.intro.intro.refine_2
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ x ∈ ball x r ∧ y ∉ ball x r
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
case hX.intro.intro.intro.refine_1
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ IsClosed (closedBall x r)

case hX.intro.intro.intro.refine_2
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ x ∈ ball x r ∧ y ∉ ball x r
Tactic:
exact isClosed_ball
Proof state after:
case hX.intro.intro.intro.refine_2
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ x ∈ ball x r ∧ y ∉ ball x r
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
case hX.intro.intro.intro.refine_2
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ x ∈ ball x r ∧ y ∉ ball x r
Tactic:
use mem_ball_self rp
Proof state after:
case right
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ y ∉ ball x r
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
case right
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ y ∉ ball x r
Tactic:
simp only [mem_ball, not_lt]
Proof state after:
case right
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ r ≤ dist y x
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
case right
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ r ≤ dist y x
Tactic:
rw [dist_comm]
Proof state after:
case right
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ r ≤ dist x y
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
case right
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
e : ball x r = closedBall x r
⊢ r ≤ dist x y
Tactic:
exact rxy.le
Proof state after:
no goals
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
⊢ R.Countable
Tactic:
have e : R = range (uncurry dist) := by
  apply Set.ext; intro r; simp only [mem_setOf, mem_range, Prod.exists, uncurry, ← hR]; rfl
Proof state after:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
e : R = range (uncurry dist)
⊢ R.Countable
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
e : R = range (uncurry dist)
⊢ R.Countable
Tactic:
rw [e]
Proof state after:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
e : R = range (uncurry dist)
⊢ (range (uncurry dist)).Countable
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
e : R = range (uncurry dist)
⊢ (range (uncurry dist)).Countable
Tactic:
exact countable_range _
Proof state after:
no goals
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
⊢ R = range (uncurry dist)
Tactic:
apply Set.ext
Proof state after:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
⊢ ∀ (x : ℝ), x ∈ R ↔ x ∈ range (uncurry dist)
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
⊢ ∀ (x : ℝ), x ∈ R ↔ x ∈ range (uncurry dist)
Tactic:
intro r
Proof state after:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
r : ℝ
⊢ r ∈ R ↔ r ∈ range (uncurry dist)
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
r : ℝ
⊢ r ∈ R ↔ r ∈ range (uncurry dist)
Tactic:
simp only [mem_setOf, mem_range, Prod.exists, uncurry, ← hR]
Proof state after:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
r : ℝ
⊢ (∃ x y, dist x y = r) ↔ ∃ a b, dist a b = r
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
r : ℝ
⊢ (∃ x y, dist x y = r) ↔ ∃ a b, dist a b = r
Tactic:
rfl
Proof state after:
no goals
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
⊢ ¬Ioo 0 (dist x y) ⊆ R
Tactic:
by_contra h
Proof state after:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
h : Ioo 0 (dist x y) ⊆ R
⊢ False
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
h : Ioo 0 (dist x y) ⊆ R
⊢ False
Tactic:
exact not_countable_Ioo xy (rc.mono h)
Proof state after:
no goals
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
⊢ ball x r = closedBall x r
Tactic:
apply Set.ext
Proof state after:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
⊢ ∀ (x_1 : X), x_1 ∈ ball x r ↔ x_1 ∈ closedBall x r
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
⊢ ∀ (x_1 : X), x_1 ∈ ball x r ↔ x_1 ∈ closedBall x r
Tactic:
intro z
Proof state after:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
z : X
⊢ z ∈ ball x r ↔ z ∈ closedBall x r
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
z : X
⊢ z ∈ ball x r ↔ z ∈ closedBall x r
Tactic:
simp only [mem_ball, mem_closedBall]
Proof state after:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
z : X
⊢ dist z x < r ↔ dist z x ≤ r
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rr : r ∉ R
rp : 0 < r
rxy : r < dist x y
z : X
⊢ dist z x < r ↔ dist z x ≤ r
Tactic:
simp only [mem_setOf, not_exists, ← hR] at rr
Proof state after:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rp : 0 < r
rxy : r < dist x y
z : X
rr : ∀ (x x_1 : X), ¬dist x x_1 = r
⊢ dist z x < r ↔ dist z x ≤ r
Theorem: Countable.totallyDisconnectedSpace
Proof state before:
case h
X : Type
inst✝¹ : MetricSpace X
inst✝ : Countable X
R : Set ℝ
hR : {r | ∃ x y, dist x y = r} = R
rc : R.Countable
x y : X
xy : 0 < dist x y
r : ℝ
rp : 0 < r
rxy : r < dist x y
z : X
rr : ∀ (x x_1 : X), ¬dist x x_1 = r
⊢ dist z x < r ↔ dist z x ≤ r
Tactic:
simp only [Ne.le_iff_lt (rr z x)]
Proof state after:
no goals
Theorem: IsCountable.isTotallyDisconnected
Proof state before:
X : Type
inst✝ : MetricSpace X
s : Set X
h : s.Countable
⊢ IsTotallyDisconnected s
Tactic:
rw [← isTotallyDisconnected_iff_totally_disconnected_subtype]
Proof state after:
X : Type
inst✝ : MetricSpace X
s : Set X
h : s.Countable
⊢ TotallyDisconnectedSpace ↑s
Theorem: IsCountable.isTotallyDisconnected
Proof state before:
X : Type
inst✝ : MetricSpace X
s : Set X
h : s.Countable
⊢ TotallyDisconnectedSpace ↑s
Tactic:
exact @Countable.totallyDisconnectedSpace _ _ (countable_coe_iff.mpr h)
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.zz
Proof state before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ ↑(extChartAt I z).symm (c, i.z').2 = z
Tactic:
simp only [Prod.snd, Cinv.z', PartialEquiv.left_inv _ (mem_extChartAt_source _ _)]
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.fa'
Proof state before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ AnalyticAt ℂ i.f' (c, i.z')
Tactic:
have fa := i.fa
Proof state after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
⊢ AnalyticAt ℂ i.f' (c, i.z')
Theorem: ComplexInverseFun.Cinv.fa'
Proof state before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
⊢ AnalyticAt ℂ i.f' (c, i.z')
Tactic:
simp only [holomorphicAt_iff, uncurry, extChartAt_prod, Function.comp, PartialEquiv.prod_coe_symm,
  PartialEquiv.prod_coe] at fa
Proof state after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
fa :
  ContinuousAt (uncurry f) (c, z) ∧
    AnalyticAt ℂ (fun x => ↑(extChartAt I (f c z)) (f (↑(extChartAt I c).symm x.1) (↑(extChartAt I z).symm x.2)))
      (↑(extChartAt I c) c, ↑(extChartAt I z) z)
⊢ AnalyticAt ℂ i.f' (c, i.z')
Theorem: ComplexInverseFun.Cinv.fa'
Proof state before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
fa :
  ContinuousAt (uncurry f) (c, z) ∧
    AnalyticAt ℂ (fun x => ↑(extChartAt I (f c z)) (f (↑(extChartAt I c).symm x.1) (↑(extChartAt I z).symm x.2)))
      (↑(extChartAt I c) c, ↑(extChartAt I z) z)
⊢ AnalyticAt ℂ i.f' (c, i.z')
Tactic:
exact fa.2
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.has_df'
Proof state before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt (I.prod I) I i.f' (c, i.z') i.df'
Tactic:
apply HasMFDerivAt.comp (I' := I) (c, i.z')
Proof state after:
case hg
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt I I (↑(extChartAt I (f c z))) (f (c, i.z').1 (↑(extChartAt I z).symm (c, i.z').2)) i.de'

case hf
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt (I.prod I) I (fun x => f x.1 (↑(extChartAt I z).symm x.2)) (c, i.z') i.df
Theorem: ComplexInverseFun.Cinv.has_df'
Proof state before:
case hg
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt I I (↑(extChartAt I (f c z))) (f (c, i.z').1 (↑(extChartAt I z).symm (c, i.z').2)) i.de'
Tactic:
rw [i.zz]
Proof state after:
case hg
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt I I (↑(extChartAt I (f c z))) (f (c, i.z').1 z) i.de'
Theorem: ComplexInverseFun.Cinv.has_df'
Proof state before:
case hg
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt I I (↑(extChartAt I (f c z))) (f (c, i.z').1 z) i.de'
Tactic:
exact (HolomorphicAt.extChartAt (mem_extChartAt_source _ _)).mdifferentiableAt.hasMFDerivAt
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.has_df'
Proof state before:
case hf
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt (I.prod I) I (fun x => f x.1 (↑(extChartAt I z).symm x.2)) (c, i.z') i.df
Tactic:
simp only [Cinv.df]
Proof state after:
case hf
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt (I.prod I) I (fun x => f x.1 (↑(extChartAt I z).symm x.2)) (c, i.z')
    (i.dfc.comp dc + i.dfz.comp (i.de.comp dz))
Theorem: ComplexInverseFun.Cinv.has_df'
Proof state before:
case hf
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt (I.prod I) I (fun x => f x.1 (↑(extChartAt I z).symm x.2)) (c, i.z')
    (i.dfc.comp dc + i.dfz.comp (i.de.comp dz))
Tactic:
apply MDifferentiableAt.hasMFDerivAt_comp2 (J := I) (co := cms)
Proof state after:
case hf.fd
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ MDifferentiableAt (I.prod I) I (uncurry f) ((c, i.z').1, ↑(extChartAt I z).symm (c, i.z').2)

case hf.gh
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt (I.prod I) I (fun y => y.1) (c, i.z') dc

case hf.hh
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt (I.prod I) I (fun y => ↑(extChartAt I z).symm y.2) (c, i.z') (i.de.comp dz)

case hf.fh0
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Theorem: ComplexInverseFun.Cinv.has_df'
Proof state before:
case hf.fd
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ MDifferentiableAt (I.prod I) I (uncurry f) ((c, i.z').1, z)

case hf.gh
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt (I.prod I) I (fun y => y.1) (c, i.z') dc

case hf.hh
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt (I.prod I) I (fun y => ↑(extChartAt I z).symm y.2) (c, i.z') (i.de.comp dz)

case hf.fh0
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Tactic:
exact i.fa.mdifferentiableAt
Proof state after:
case hf.gh
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt (I.prod I) I (fun y => y.1) (c, i.z') dc

case hf.hh
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt (I.prod I) I (fun y => ↑(extChartAt I z).symm y.2) (c, i.z') (i.de.comp dz)

case hf.fh0
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Theorem: ComplexInverseFun.Cinv.has_df'
Proof state before:
case hf.gh
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt (I.prod I) I (fun y => y.1) (c, i.z') dc

case hf.hh
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt (I.prod I) I (fun y => ↑(extChartAt I z).symm y.2) (c, i.z') (i.de.comp dz)

case hf.fh0
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Tactic:
apply hasMFDerivAt_fst
Proof state after:
case hf.hh
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt (I.prod I) I (fun y => ↑(extChartAt I z).symm y.2) (c, i.z') (i.de.comp dz)

case hf.fh0
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
i : Cinv f c z
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz