awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a : ℝ
⊢ Eq (α := Set ℂ) (frontier {z : ℂ | a < z.im}) {z : ℂ | z.im = a}

Tactic:
simpa only [frontier_Ioi] using frontier_preimage_im (Ioi a)

Premises used: Set.Ioi, frontier_Ioi, Complex.frontier_preimage_im
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
s t : Set ℝ
⊢ closure (s ×ℂ t) = closure s ×ℂ closure t

Tactic:
simpa only [← preimage_eq_preimage equivRealProdCLM.symm.toHomeomorph.surjective,
    equivRealProdCLM.symm.toHomeomorph.preimage_closure] using @closure_prod_eq _ _ _ _ s t

Premises used: ContinuousLinearEquiv.symm, Complex.equivRealProdCLM, Set.preimage_eq_preimage, Homeomorph.preimage_closure, ContinuousLinearEquiv.toHomeomorph, Homeomorph.surjective, closure_prod_eq
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
s t : Set ℝ
rw : interior (re ⁻¹' s ∩ im ⁻¹' t) = interior s ×ℂ interior t
rw₁ : interior (re ⁻¹' s ∩ im ⁻¹' t) = re ⁻¹' interior s ∩ im ⁻¹' interior t
rw₂ : interior (re ⁻¹' s) ∩ interior (im ⁻¹' t) = re ⁻¹' interior s ∩ im ⁻¹' interior t
rw₃ : re ⁻¹' interior s ∩ interior (im ⁻¹' t) = re ⁻¹' interior s ∩ im ⁻¹' interior t
rw₄ rw₅ : re ⁻¹' interior s ∩ im ⁻¹' interior t = re ⁻¹' interior s ∩ im ⁻¹' interior t
⊢ interior (s ×ℂ t) = interior s ×ℂ interior t

Tactic:
rw [reProdIm, reProdIm, interior_inter, interior_preimage_re, interior_preimage_im]

Premises used: interior_inter, Complex.interior_preimage_re, Complex.interior_preimage_im, Complex.reProdIm
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
s t : Set ℝ
⊢ frontier (s ×ℂ t) = closure s ×ℂ frontier t ∪ frontier s ×ℂ closure t

Tactic:
simpa only [← preimage_eq_preimage equivRealProdCLM.symm.toHomeomorph.surjective,
    equivRealProdCLM.symm.toHomeomorph.preimage_frontier] using frontier_prod_eq s t

Premises used: ContinuousLinearEquiv.symm, frontier_prod_eq, Complex.equivRealProdCLM, Homeomorph.preimage_frontier, Set.preimage_eq_preimage, ContinuousLinearEquiv.toHomeomorph, Homeomorph.surjective
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a b : ℝ
⊢ Eq (α := Set ℂ) (frontier {z : ℂ | a ≤ z.re ∧ b ≤ z.im}) {z : ℂ | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ b ≤ z.im}

Tactic:
simpa only [closure_Ici, frontier_Ici] using frontier_reProdIm (Ici a) (Ici b)

Premises used: Set.Ici, frontier_Ici, closure_Ici, Complex.frontier_reProdIm
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
a b : ℝ
⊢ Eq (α := Set ℂ) (frontier {z : ℂ | a ≤ z.re ∧ z.im ≤ b}) {z : ℂ | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ z.im ≤ b}

Tactic:
simpa only [closure_Ici, closure_Iic, frontier_Ici, frontier_Iic] using
    frontier_reProdIm (Ici a) (Iic b)

Premises used: Set.Ici, frontier_Ici, closure_Ici, closure_Iic, frontier_Iic, Set.Iic, Complex.frontier_reProdIm
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
s t : Set ℝ
hs : IsOpen s
ht : IsOpen t
⊢ IsOpen (s ×ℂ t)

Tactic:
(hs.preimage continuous_re).inter (ht.preimage continuous_im)

Premises used: Complex.continuous_re, Complex.reProdIm, IsOpen.inter, IsOpen.preimage, Complex.continuous_im
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
s t : Set ℝ
hs : IsClosed s
ht : IsClosed t
⊢ IsClosed (s ×ℂ t)

Tactic:
(hs.preimage continuous_re).inter (ht.preimage continuous_im)

Premises used: Complex.continuous_re, Complex.reProdIm, IsClosed.preimage, IsClosed.inter, Complex.continuous_im
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
s t : Set ℝ
hs : IsBounded s
ht : IsBounded t
⊢ IsBounded (s ×ℂ t)

Tactic:
antilipschitz_equivRealProd.isBounded_preimage (hs.prod ht)

Premises used: Set.Mem, setOf, Bornology.IsBounded.prod, Set.prod, AntilipschitzWith.isBounded_preimage, Complex.antilipschitz_equivRealProd, Set.inter, Complex.reProdIm, Set.preimage
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
α : Type u_1
ι : Type u_2
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
K : Set α
hf : TendstoUniformlyOn f g p K
⊢ TendstoUniformlyOn (β := ℝ) (fun (n : ι) (x : α) ↦ (f n x).re) (fun (y : α) ↦ (g y).re) p K

Tactic:
apply UniformContinuous.comp_tendstoUniformlyOn uniformContinuous_re hf

Premises used: Complex.uniformContinuous_re, UniformContinuous.comp_tendstoUniformlyOn
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
α : Type u_1
ι : Type u_2
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformly f g p
⊢ TendstoUniformly (β := ℝ) (fun (n : ι) (x : α) ↦ (f n x).re) (fun (y : α) ↦ (g y).re) p

Tactic:
apply UniformContinuous.comp_tendstoUniformly uniformContinuous_re hf

Premises used: Complex.uniformContinuous_re, UniformContinuous.comp_tendstoUniformly
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
α : Type u_1
ι : Type u_2
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
K : Set α
hf : TendstoUniformlyOn f g p K
⊢ TendstoUniformlyOn (β := ℝ) (fun (n : ι) (x : α) ↦ (f n x).im) (fun (y : α) ↦ (g y).im) p K

Tactic:
apply UniformContinuous.comp_tendstoUniformlyOn uniformContinuous_im hf

Premises used: Complex.uniformContinuous_im, UniformContinuous.comp_tendstoUniformlyOn
-- Module: Mathlib.Analysis.Complex.ReImTopology
Goal:
α : Type u_1
ι : Type u_2
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformly f g p
⊢ TendstoUniformly (β := ℝ) (fun (n : ι) (x : α) ↦ (f n x).im) (fun (y : α) ↦ (g y).im) p

Tactic:
apply UniformContinuous.comp_tendstoUniformly uniformContinuous_im hf

Premises used: Complex.uniformContinuous_im, UniformContinuous.comp_tendstoUniformly
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' (↑z : ℂ)
⊢ HasStrictFDerivAt ofReal ofRealCLM z

Tactic:
have A : HasStrictFDerivAt ((↑) : ℝ → ℂ) ofRealCLM z := ofRealCLM.hasStrictFDerivAt
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' (↑z : ℂ)
A : HasStrictFDerivAt ofReal ofRealCLM z
⊢ HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars (A := ℂ) ℝ (ContinuousLinearMap.smulRight (S := ℂ) 1 e'))
    ((ofRealCLM : (a : ℝ) → ℂ) z)

Tactic:
have B :
    HasStrictFDerivAt e ((ContinuousLinearMap.smulRight 1 e' : ℂ →L[ℂ] ℂ).restrictScalars ℝ)
      (ofRealCLM z) :=
    h.hasStrictFDerivAt.restrictScalars ℝ
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' (↑z : ℂ)
A : HasStrictFDerivAt ofReal ofRealCLM z
B :
  HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars (A := ℂ) ℝ (ContinuousLinearMap.smulRight (S := ℂ) 1 e'))
    ((ofRealCLM : (a : ℝ) → ℂ) z)
⊢ HasStrictFDerivAt re reCLM (e ((ofRealCLM : (a : ℝ) → ℂ) z))

Tactic:
have C : HasStrictFDerivAt re reCLM (e (ofRealCLM z)) := reCLM.hasStrictFDerivAt
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' (↑z : ℂ)
A : HasStrictFDerivAt ofReal ofRealCLM z
B :
  HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars (A := ℂ) ℝ (ContinuousLinearMap.smulRight (S := ℂ) 1 e'))
    ((ofRealCLM : (a : ℝ) → ℂ) z)
C : HasStrictFDerivAt re reCLM (e ((ofRealCLM : (a : ℝ) → ℂ) z))
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ (e (↑x : ℂ)).re) e'.re z

Tactic:
simpa using (C.comp z (B.comp z A)).hasStrictDerivAt

Premises used: HasStrictFDerivAt.hasStrictDerivAt, HasStrictFDerivAt.comp
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' (↑z : ℂ)
⊢ HasFDerivAt ofReal ofRealCLM z

Tactic:
have A : HasFDerivAt ((↑) : ℝ → ℂ) ofRealCLM z := ofRealCLM.hasFDerivAt
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' (↑z : ℂ)
A : HasFDerivAt ofReal ofRealCLM z
⊢ HasFDerivAt e (ContinuousLinearMap.restrictScalars (A := ℂ) ℝ (ContinuousLinearMap.smulRight (S := ℂ) 1 e'))
    ((ofRealCLM : (a : ℝ) → ℂ) z)

Tactic:
have B :
    HasFDerivAt e ((ContinuousLinearMap.smulRight 1 e' : ℂ →L[ℂ] ℂ).restrictScalars ℝ)
      (ofRealCLM z) :=
    h.hasFDerivAt.restrictScalars ℝ
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' (↑z : ℂ)
A : HasFDerivAt ofReal ofRealCLM z
B :
  HasFDerivAt e (ContinuousLinearMap.restrictScalars (A := ℂ) ℝ (ContinuousLinearMap.smulRight (S := ℂ) 1 e'))
    ((ofRealCLM : (a : ℝ) → ℂ) z)
⊢ HasFDerivAt re reCLM (e ((ofRealCLM : (a : ℝ) → ℂ) z))

Tactic:
have C : HasFDerivAt re reCLM (e (ofRealCLM z)) := reCLM.hasFDerivAt
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' (↑z : ℂ)
A : HasFDerivAt ofReal ofRealCLM z
B :
  HasFDerivAt e (ContinuousLinearMap.restrictScalars (A := ℂ) ℝ (ContinuousLinearMap.smulRight (S := ℂ) 1 e'))
    ((ofRealCLM : (a : ℝ) → ℂ) z)
C : HasFDerivAt re reCLM (e ((ofRealCLM : (a : ℝ) → ℂ) z))
⊢ HasDerivAt (fun (x : ℝ) ↦ (e (↑x : ℂ)).re) e'.re z

Tactic:
simpa using (C.comp z (B.comp z A)).hasDerivAt

Premises used: HasFDerivAt.hasDerivAt, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e (↑z : ℂ)
⊢ ContDiffAt ℝ n ofReal z

Tactic:
have A : ContDiffAt ℝ n ((↑) : ℝ → ℂ) z := ofRealCLM.contDiff.contDiffAt
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e (↑z : ℂ)
A : ContDiffAt ℝ n ofReal z
⊢ ContDiffAt ℝ n e (↑z : ℂ)

Tactic:
have B : ContDiffAt ℝ n e z := h.restrict_scalars ℝ
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e (↑z : ℂ)
A : ContDiffAt ℝ n ofReal z
B : ContDiffAt ℝ n e (↑z : ℂ)
⊢ ContDiffAt ℝ n re (e (↑z : ℂ))

Tactic:
have C : ContDiffAt ℝ n re (e z) := reCLM.contDiff.contDiffAt
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e (↑z : ℂ)
A : ContDiffAt ℝ n ofReal z
B : ContDiffAt ℝ n e (↑z : ℂ)
C : ContDiffAt ℝ n re (e (↑z : ℂ))
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ (e (↑x : ℂ)).re) z

Tactic:
C.comp z (B.comp z A)

Premises used: ContDiffAt.comp
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e (↑z : ℂ)
A : ContDiffAt ℝ n ofReal z
B : ContDiffAt ℝ n e (↑z : ℂ)
C : ContDiffAt ℝ n re (e (↑z : ℂ))
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ (e (↑x : ℂ)).re) z

Tactic:
exact C.comp z (B.comp z A)

Premises used: ContDiffAt.comp
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
e : ℂ → ℂ
n : ℕ∞ω
h : ContDiff ℂ n e
⊢ ContDiff ℝ (F := ℝ) n fun (x : ℝ) ↦ (e (↑x : ℂ)).re

Tactic:
contDiff_iff_contDiffAt.2 fun _ => h.contDiffAt.real_of_complex

Premises used: Iff.mpr, ContDiffAt.real_of_complex, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
f' : E
h : HasStrictDerivAt f f' x
⊢ HasStrictFDerivAt f (reCLM.smulRight f' + HSMul.hSMul (β := ℂ →L[ℝ] E) I (imCLM.smulRight f')) x

Tactic:
simpa only [Complex.restrictScalars_toSpanSingleton'] using h.hasStrictFDerivAt.restrictScalars ℝ

Premises used: Real, HasStrictFDerivAt.restrictScalars, HasStrictDerivAt.hasStrictFDerivAt, Complex.restrictScalars_toSpanSingleton'
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
f' : E
h : HasDerivAt f f' x
⊢ HasFDerivAt f (reCLM.smulRight f' + HSMul.hSMul (β := ℂ →L[ℝ] E) I (imCLM.smulRight f')) x

Tactic:
simpa only [Complex.restrictScalars_toSpanSingleton'] using h.hasFDerivAt.restrictScalars ℝ

Premises used: Real, HasFDerivAt.restrictScalars, HasDerivAt.hasFDerivAt, Complex.restrictScalars_toSpanSingleton'
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
x : ℂ
f' : E
h : HasDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f (reCLM.smulRight f' + HSMul.hSMul (β := ℂ →L[ℝ] E) I (imCLM.smulRight f')) s x

Tactic:
simpa only [Complex.restrictScalars_toSpanSingleton'] using h.hasFDerivWithinAt.restrictScalars ℝ

Premises used: Real, HasDerivWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.restrictScalars, Complex.restrictScalars_toSpanSingleton'
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
f : ℂ → ℂ
f' x : ℂ
h : HasStrictDerivAt f f' x
⊢ HasStrictFDerivAt f (HSMul.hSMul (β := ℂ →L[ℝ] ℂ) f' 1) x

Tactic:
simpa only [Complex.restrictScalars_toSpanSingleton] using h.hasStrictFDerivAt.restrictScalars ℝ

Premises used: Real, HasStrictFDerivAt.restrictScalars, HasStrictDerivAt.hasStrictFDerivAt, Complex.restrictScalars_toSpanSingleton
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
f : ℂ → ℂ
f' x : ℂ
h : HasDerivAt f f' x
⊢ HasFDerivAt f (HSMul.hSMul (β := ℂ →L[ℝ] ℂ) f' 1) x

Tactic:
simpa only [Complex.restrictScalars_toSpanSingleton] using h.hasFDerivAt.restrictScalars ℝ

Premises used: Real, HasFDerivAt.restrictScalars, HasDerivAt.hasFDerivAt, Complex.restrictScalars_toSpanSingleton
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
f : ℂ → ℂ
s : Set ℂ
f' x : ℂ
h : HasDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f (HSMul.hSMul (β := ℂ →L[ℝ] ℂ) f' 1) s x

Tactic:
simpa only [Complex.restrictScalars_toSpanSingleton] using h.hasFDerivWithinAt.restrictScalars ℝ

Premises used: Real, HasDerivWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.restrictScalars, Complex.restrictScalars_toSpanSingleton
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
e : ℂ → ℂ
e' : ℂ
z : ℝ
hf : HasDerivAt e e' (↑z : ℂ)
⊢ HasDerivAt (fun (y : ℝ) ↦ e (↑y : ℂ)) e' z

Tactic:
simpa only [ofRealCLM_apply, ofReal_one, mul_one] using hf.comp z ofRealCLM.hasDerivAt

Premises used: ContinuousLinearMap.hasDerivAt, HasDerivAt.comp, Complex.ofReal_one, Complex.ofRealCLM, Complex.ofRealCLM_apply, mul_one
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt f u z
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑(f y) : ℂ)) (↑u : ℂ) z

Tactic:
simpa only [ofRealCLM_apply, ofReal_one, real_smul, mul_one] using
    ofRealCLM.hasDerivAt.scomp z hf

Premises used: Complex.real_smul, ContinuousLinearMap.hasDerivAt, Complex.ofReal_one, Complex.ofRealCLM, Complex.ofRealCLM_apply, HasDerivAt.scomp, mul_one
-- Module: Mathlib.Analysis.Complex.RealDeriv
Goal:
z : ℝ
f : ℝ → ℝ
s : Set ℝ
u : ℝ
hf : HasDerivWithinAt f u s z
⊢ HasDerivWithinAt (fun (y : ℝ) ↦ (↑(f y) : ℂ)) (↑u : ℂ) s z

Tactic:
simpa only [Function.comp_apply, ofRealCLM_apply] using
    ofRealCLM.hasFDerivAt.comp_hasDerivWithinAt z hf

Premises used: ContinuousLinearMap.hasFDerivAt, Complex.ofRealCLM, Complex.ofRealCLM_apply, HasFDerivAt.comp_hasDerivWithinAt, Function.comp_apply
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
rcases :
  ∀ (R : ℝ) (hR0 : 0 < R) (hRs : closedBall c R ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}),
    AnalyticAt ℂ f c
⊢ AnalyticAt ℂ f c

Tactic:
rcases (nhdsWithin_hasBasis nhds_basis_closedBall _).mem_iff.1 hd with ⟨R, hR0, hRs⟩

Premises used: Filter.HasBasis.mem_iff, Iff.mp, nhdsWithin_hasBasis, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ
hR0 : 0 < R
hRs : closedBall c R ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
⊢ 0 ≤ R

Tactic:
hR0.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ
hR0 : 0 < R
hRs : closedBall c R ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
lift :
  ∀ (R : ℝ≥0) (hR0 : 0 < (↑R : ℝ))
    (hRs : closedBall c (↑R : ℝ) ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}), AnalyticAt ℂ f c
⊢ AnalyticAt ℂ f c

Tactic:
lift R to ℝ≥0 using hR0.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ≥0
hR0 : 0 < (↑R : ℝ)
hRs : closedBall c (↑R : ℝ) ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
⊢ ContinuousOn f (closedBall c (↑R : ℝ))

Tactic:
fun z hz => ContinuousAt.continuousWithinAt ?_

Premises used: ContinuousAt.continuousWithinAt, ContinuousOn
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ≥0
hR0 : 0 < (↑R : ℝ)
hRs : closedBall c (↑R : ℝ) ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
refine : ∀ (z : ℂ) (hz : z ∈ closedBall c (↑R : ℝ)), ContinuousAt f z
⊢ ContinuousOn f (closedBall c (↑R : ℝ))

Tactic:
refine fun z hz => ContinuousAt.continuousWithinAt ?_

Premises used: ContinuousAt.continuousWithinAt
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ≥0
hR0 : 0 < (↑R : ℝ)
hRs : closedBall c (↑R : ℝ) ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
z : ℂ
hz : z ∈ closedBall c (↑R : ℝ)
inl :
  ∀ (hd : ∀ᶠ (z : ℂ) in 𝓝[≠] z, DifferentiableAt ℂ f z) (hc : ContinuousAt f z)
    (hRs : closedBall z (↑R : ℝ) ∩ {z}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x})
    (hz : z ∈ closedBall z (↑R : ℝ)), ContinuousAt f z
inr : ∀ (hne : z ≠ c), ContinuousAt f z
⊢ ContinuousAt f z

Tactic:
rcases eq_or_ne z c with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ≥0
hR0 : 0 < (↑R : ℝ)
z : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] z, DifferentiableAt ℂ f z
hc : ContinuousAt f z
hRs : closedBall z (↑R : ℝ) ∩ {z}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
hz : z ∈ closedBall z (↑R : ℝ)
⊢ ContinuousAt f z

Tactic:
hc
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ≥0
hR0 : 0 < (↑R : ℝ)
hRs : closedBall c (↑R : ℝ) ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
z : ℂ
hz : z ∈ closedBall c (↑R : ℝ)
hne : z ≠ c
⊢ ContinuousAt f z

Tactic:
(hRs ⟨hz, hne⟩).continuousAt

Premises used: DifferentiableAt.continuousAt, And.intro
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ≥0
hR0 : 0 < (↑R : ℝ)
z : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] z, DifferentiableAt ℂ f z
hc : ContinuousAt f z
hRs : closedBall z (↑R : ℝ) ∩ {z}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
hz : z ∈ closedBall z (↑R : ℝ)
⊢ ContinuousAt f z

Tactic:
exacts [hc, (hRs ⟨hz, hne⟩).continuousAt]
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ≥0
hR0 : 0 < (↑R : ℝ)
hRs : closedBall c (↑R : ℝ) ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
⊢ ContinuousOn f (closedBall c (↑R : ℝ))

Tactic:
replace hc : ContinuousOn f (closedBall c R) := by
    refine fun z hz => ContinuousAt.continuousWithinAt ?_
    rcases eq_or_ne z c with (rfl | hne)
    exacts [hc, (hRs ⟨hz, hne⟩).continuousAt]
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
R : ℝ≥0
hR0 : 0 < (↑R : ℝ)
hRs : closedBall c (↑R : ℝ) ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
hc : ContinuousOn f (closedBall c (↑R : ℝ))
⊢ AnalyticAt ℂ f c

Tactic:
(hasFPowerSeriesOnBall_of_differentiable_off_countable (countable_singleton c) hc
    (fun z hz => hRs (diff_subset_diff_left ball_subset_closedBall hz)) hR0).analyticAt

Premises used: Metric.ball_subset_closedBall, Set.diff_subset_diff_left, HasFPowerSeriesOnBall.analyticAt, Set.countable_singleton, Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
R : ℝ≥0
hR0 : 0 < (↑R : ℝ)
hRs : closedBall c (↑R : ℝ) ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
hc : ContinuousOn f (closedBall c (↑R : ℝ))
⊢ AnalyticAt ℂ f c

Tactic:
exact (hasFPowerSeriesOnBall_of_differentiable_off_countable (countable_singleton c) hc
    (fun z hz => hRs (diff_subset_diff_left ball_subset_closedBall hz)) hR0).analyticAt

Premises used: Metric.ball_subset_closedBall, Set.diff_subset_diff_left, HasFPowerSeriesOnBall.analyticAt, Set.countable_singleton, Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hs : s ∈ 𝓝 c
⊢ DifferentiableOn ℂ f (s \ {c}) ∧ ContinuousAt f c ↔ DifferentiableOn ℂ f s

Tactic:
⟨?_, fun hd => ⟨hd.mono diff_subset, (hd.differentiableAt hs).continuousAt⟩⟩

Premises used: Set.diff_subset, DifferentiableAt.continuousAt, DifferentiableOn.differentiableAt, And.intro, Iff.intro, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hs : s ∈ 𝓝 c
refine : DifferentiableOn ℂ f (s \ {c}) ∧ ContinuousAt f c → DifferentiableOn ℂ f s
⊢ DifferentiableOn ℂ f (s \ {c}) ∧ ContinuousAt f c ↔ DifferentiableOn ℂ f s

Tactic:
refine ⟨?_, fun hd => ⟨hd.mono diff_subset, (hd.differentiableAt hs).continuousAt⟩⟩
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hs : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
hc : ContinuousAt f c
x : ℂ
hx : x ∈ s
inl : ∀ (hs : s ∈ 𝓝 x) (hd : DifferentiableOn ℂ f (s \ {x})) (hc : ContinuousAt f x), DifferentiableWithinAt ℂ f s x
inr : ∀ (hne : x ≠ c), DifferentiableWithinAt ℂ f s x
⊢ DifferentiableWithinAt ℂ f s x

Tactic:
rcases eq_or_ne x c with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
x : ℂ
hx : x ∈ s
hs : s ∈ 𝓝 x
hd : DifferentiableOn ℂ f (s \ {x})
hc : ContinuousAt f x
⊢ DifferentiableWithinAt ℂ f s x

Tactic:
(analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt
      ?_ hc).differentiableAt.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, AnalyticAt.differentiableAt, Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
x : ℂ
hx : x ∈ s
hs : s ∈ 𝓝 x
hd : DifferentiableOn ℂ f (s \ {x})
hc : ContinuousAt f x
inl : ∀ᶠ (z : ℂ) in 𝓝[≠] x, DifferentiableAt ℂ f z
⊢ DifferentiableWithinAt ℂ f s x

Tactic:
refine (analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt
      ?_ hc).differentiableAt.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, AnalyticAt.differentiableAt, Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt