mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
x : F
hx : x ∈ f '' s
y : F
hy : y ∈ f '' s
⊢ ‖↑(hf.toPartialEquiv hc).symm x - ↑(hf.toPartialEquiv hc).symm y - ↑f'.symm (x - y)‖ ≤
    ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖x - y‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
z₀ : 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
n : ℕ
IH : ∀ {f : 𝕜 → E}, AnalyticAt 𝕜 f z₀ → (↑n ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0)
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hfz : f z₀ = 0
⊢ analyticOrderAt (deriv f) z₀ + 1 = analyticOrderAt f z₀

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
x : X.obj (op { obj := ⦋2⦌, property := _proof_14 })
y : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_14 })
h₂ :
  ComposableArrows.mk₁ (F.map (homMk (Edge.mk' ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x)))) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 2 _proof_12 _proof_15).op)) y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk (Edge.mk' ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x)))) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 0 _proof_12 _proof_15).op)) y
⊢ ComposableArrows.mk₁ (F.map (homMk (Edge.mk' ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_12 _proof_15).op)) x)))) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 1 _proof_12 _proof_15).op)) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
hf : AnalyticAt 𝕜 f z₀
⊢ ↑n ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })
⊢ F.mapArrow.obj (Arrow.mk (homMk (Edge.id x))) =
    ComposableArrows.arrowEquiv
      ((ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (σ₂ 0 _proof_13 _proof_11).op))
        (nerveEquiv.symm (F.obj (mk x))))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
ε : ℝ
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Subsingleton F ∨ c < f'.toNonlinearRightInverse.nnnorm⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CharZero 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
horder : analyticOrderAt f z₀ = ↑n + 1
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg₀ : g z₀ ≠ 0
hfg : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ (fun x1 x2 ↦ x1 + x2) n 1 • g z
⊢ f z₀ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CharZero 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
horder : analyticOrderAt f z₀ = ↑n + 1
⊢ analyticOrderAt (deriv f) z₀ = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C : Type u
inst✝ : SmallCategory C
F : X.HomotopyCategory ⥤ C
x y : X.obj (op { obj := ⦋0⦌, property := _proof_11 })
e : Edge x y
⊢ (ConcreteCategory.hom ((homToNerveMk F).app (op { obj := ⦋1⦌, property := Edge._proof_2 }))) e.edge =
    ComposableArrows.mk₁ (F.map (homMk e))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
x : X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ (descOfTruncation (homToNerveMk F)).obj (mk x) = F.obj (mk x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
ε : ℝ
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
⊢ E ≃ₜ F

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
x y : X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
f : Edge x y
⊢ (nerve.homEquiv.symm (nerve.homEquiv (f.map (homToNerveMk F)))).edge = (nerve.homEquiv.symm (F.map (homMk f))).edge

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
x y : X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
f : Edge x y
⊢ (descOfTruncation (homToNerveMk F)).map (homMk f) = eqToHom ⋯ ≫ F.map (homMk f) ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
inst✝ : CharZero 𝕜
n' : ℕ
hk : ∀ {n : ℕ}, ↑n = analyticOrderAt f z₀ → n ≠ 0 → n' ≤ n → analyticOrderAt (deriv^[n'] f) z₀ = ↑(n - n')
n : ℕ
Hn : ↑n = analyticOrderAt f z₀
Hpos : n ≠ 0
Hk : n' + 1 ≤ n
⊢ n' ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
inst✝ : CharZero 𝕜
n' : ℕ
hk : ∀ {n : ℕ}, ↑n = analyticOrderAt f z₀ → n ≠ 0 → n' ≤ n → analyticOrderAt (deriv^[n'] f) z₀ = ↑(n - n')
n : ℕ
Hn : ↑n = analyticOrderAt f z₀
Hpos : n ≠ 0
Hk : n' + 1 ≤ n
⊢ n - n'.succ + 1 = n - n'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: x : ℂ
h : x ∈ slitPlane
h0 : x ≠ 0
⊢ HasStrictDerivAt (↑expOpenPartialHomeomorph) x (↑expOpenPartialHomeomorph.symm x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: f : ℂ → ℂ
f' x : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun t ↦ log (f t)) (f' / f x) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: f : ℝ → ℂ
x : ℝ
f' : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun t ↦ log (f t)) (f' / f x) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasDerivAt (fun t ↦ log (f t)) (f' / f x) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
inst✝ : CharZero 𝕜
n' : ℕ
hk : ∀ {n : ℕ}, ↑n = analyticOrderAt f z₀ → n ≠ 0 → n' ≤ n → analyticOrderAt (deriv^[n'] f) z₀ = ↑(n - n')
n : ℕ
Hn : ↑n = analyticOrderAt f z₀
Hpos : n ≠ 0
Hk : n' + 1 ≤ n
⊢ analyticOrderAt (deriv^[n'] f) z₀ = ↑n - ↑n'.succ + 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: f : ℝ → ℂ
x : ℝ
f' : ℂ
h₁ : HasDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasDerivAt (fun t ↦ log (f t)) (f' / f x) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
k n : ℕ
inst✝ : CharZero 𝕜
⊢ ↑n = analyticOrderAt f z₀ → n ≠ 0 → k ≤ n → analyticOrderAt (deriv^[k] f) z₀ = ↑(n - k)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun t ↦ log (f t)) (f' / f x) s x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
⊢ AnalyticAt 𝕜 (fun z ↦ ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: f : ℝ → ℂ
s : Set ℝ
x : ℝ
f' : ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun t ↦ log (f t)) (f' / f x) s x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv

Goal state before:
pp: f : ℂ → ℂ
x : ℂ
h₁ : DifferentiableAt ℂ f x
h₂ : f x ∈ slitPlane
⊢ deriv (log ∘ f) x = logDeriv f x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
s : X.obj (op { obj := ⦋1⦌, property := ⋯ })
⊢ (ConcreteCategory.hom ((homToNerveMk (descOfTruncation φ)).app (op { obj := ⦋1⦌, property := ⋯ }))) s =
    (ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
this : AnalyticAt 𝕜 (fun z ↦ ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0) 0
i : ℕ
hi : i < n
⊢ AnalyticAt 𝕜 f 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: z : ℂ
m : z ∈ slitPlane
⊢ AnalyticAt ℂ log z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
⊢ (fun z ↦ f z ^ g z) =ᶠ[𝓝[insert x s] x] fun z ↦ cexp (log (f z) * g z)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
⊢ AnalyticWithinAt ℂ (fun z ↦ f z ^ g z) s x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
fa : AnalyticAt ℂ f x
ga : AnalyticAt ℂ g x
m : f x ∈ slitPlane
⊢ AnalyticAt ℂ (fun z ↦ f z ^ g z) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ Real.log = fun x ↦ (log ↑x).re

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
⊢ ∃ F,
    AnalyticAt 𝕜 F 0 ∧
      ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ AnalyticAt ℝ Real.log x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: n : ℕ
x : ℂ
hx : x ∈ slitPlane
⊢ deriv log =ᶠ[𝓝 x] Inv.inv

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C : Type u
inst✝¹ : SmallCategory C
D : Type u
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
G : C ⥤ D
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ (ComposableArrows.mk₁ (G.map (F.map (homMk f)))).hom =
    eqToHom ⋯ ≫
      ComposableArrows.hom
          ((ConcreteCategory.hom (((truncation 2).map (nerveMap G)).app (op { obj := ⦋1⦌, property := ⋯ })))
            (ComposableArrows.mk₁ (F.map (homMk f)))) ≫
        eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
⊢ ?m.89

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C : Type u
inst✝¹ : SmallCategory C
D : Type u
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
G : C ⥤ D
s : X.obj (op { obj := ⦋1⦌, property := ⋯ })
⊢ (ConcreteCategory.hom ((homToNerveMk (F ⋙ G)).app (op { obj := ⦋1⦌, property := ⋯ }))) s =
    (ConcreteCategory.hom ((homToNerveMk F ≫ (truncation 2).map (nerveMap G)).app (op { obj := ⦋1⦌, property := ⋯ }))) s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: n : ℕ
x : ℂ
hx : x ∈ slitPlane
⊢ iteratedDeriv (n + 1) log x = (-1) ^ n * ↑n.factorial * x ^ (-↑n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X'✝ X✝ : Truncated 2
Y✝ : Cat
x✝¹ : X'✝ ⟶ X✝
x✝ : X✝ ⟶ nerveFunctor₂.obj Y✝
⊢ ((Cat.Hom.equivFunctor (hoFunctor₂.obj X'✝) Y✝).trans HomotopyCategory.functorEquiv).symm (x✝¹ ≫ x✝) =
    hoFunctor₂.map x✝¹ ≫ ((Cat.Hom.equivFunctor (hoFunctor₂.obj X✝) Y✝).trans HomotopyCategory.functorEquiv).symm x✝

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: this :
  (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n log 1 / ↑n.factorial
⊢ 1 ∈ slitPlane

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
x : C
⊢ ⦋0⦌.len ≤ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: this :
  (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) =
    FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n log 1 / ↑n.factorial
⊢ HasFPowerSeriesAt log (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : U ∈ 𝓝 0
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / ↑i.factorial) • iteratedDeriv i f 0 + y ^ n • F y
⊢ ∀ a ∈ U,
    F a = if a ∈ U then F a else (a ^ n)⁻¹ • (f a - ∑ i ∈ Finset.range n, (a ^ i / ↑i.factorial) • iteratedDeriv i f 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F 0
hF : ∀ᶠ (z : 𝕜) in 𝓝 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
U : Set 𝕜
hU0 : U ∈ 𝓝 0
hU' : ∀ y ∈ U, f y = ∑ i ∈ Finset.range n, (y ^ i / ↑i.factorial) • iteratedDeriv i f 0 + y ^ n • F y
⊢ F =ᶠ[𝓝 0] fun z ↦
    if z ∈ U then F z else (z ^ n)⁻¹ • (f z - ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: ⊢ HasFPowerSeriesAt log (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
x : C
⊢ homEquiv ((edgeMk (𝟙 x)).toTruncated.map φ) =
    𝟙 (nerveEquiv ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _proof_11 }))) (nerveEquiv.symm x)))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: ⊢ HasFPowerSeriesAt (fun x ↦ log (1 + x)) (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: r : ENNReal
hp : HasFPowerSeriesOnBall log (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n) 1 r
⊢ HasFPowerSeriesOnBall log
    (FormalMultilinearSeries.restrictScalars ℝ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ -(-1) ^ n / ↑n))
    (ofRealCLM 1) r

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ homEquiv ((edgeMk (f ≫ g)).toTruncated.map φ) =
    homEquiv ((edgeMk f).toTruncated.map φ) ≫ homEquiv ((edgeMk g).toTruncated.map φ)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
f : (nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋1⦌, property := ⋯ })
⊢ (ConcreteCategory.hom ((nerveFunctor₂.map (functorOfNerveMap φ).toCatHom).app (op { obj := ⦋1⦌, property := ⋯ }))) f =
    (ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: ⊢ HasFPowerSeriesAt Real.log (FormalMultilinearSeries.ofScalars ℝ fun n ↦ -(-1) ^ n / ↑n) 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
x : C
⊢ (functorOfNerveMap ((SSet.truncation 2).map (nerveMap F))).obj x = F.obj x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: ⊢ HasFPowerSeriesAt (fun x ↦ Real.log (1 + x)) (FormalMultilinearSeries.ofScalars ℝ fun n ↦ -(-1) ^ n / ↑n) 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
x y : C
f : x ⟶ y
⊢ (functorOfNerveMap ((SSet.truncation 2).map (nerveMap F))).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
X✝ Y✝ : Cat
x✝ : X✝ ⟶ Y✝
⊢ (functorOfNerveMap (nerveFunctor₂.map x✝)).toCatHom = x✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : Category.{u, u} C
inst✝ : Category.{u, u} D
⊢ IsIso (prodComparison (nerveFunctor ⋙ hoFunctor ⋙ nerveFunctor) (Cat.of C) (Cat.of D))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
x : 𝔸
n : ℕ
⊢ ((ordinaryHypergeometricSeries 𝔸 a b c n) fun x_1 ↦ x) =
    ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
x : 𝔸
⊢ (fun n ↦ (ordinaryHypergeometricSeries 𝔸 a b c n) fun x_1 ↦ x) = fun n ↦
    ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : Category.{u, u} C
inst✝ : Category.{u, u} D
⊢ IsIso (nerveFunctor.map (prodComparison hoFunctor (nerve C) (nerve D)))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : Category.{u, u} C
inst✝ : Category.{u, u} D
⊢ IsIso (prodComparison hoFunctor (nerve C) (nerve D))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n : ℕ
⊢ ((ordinaryHypergeometricSeries 𝔸 a b c n) fun x ↦ 0) = Pi.single 0 1 n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
⊢ ₂F₁ a b c 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: D X : SSet
H : ∀ (m : ℕ), IsIso (prodComparison hoFunctor D Δ[m])
⊢ IsIso
    ((CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}).whiskerLeft
      (prodComparisonNatTrans hoFunctor D))

Tactic:
by

Goal state after: