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

Goal state before:
pp: case inr
𝕜 : 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
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
⊢ Surjective f

Tactic:
·

Goal state after:
case inr
𝕜 : 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
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑f'.symm‖₊⁻¹
⊢ Surjective f
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case «1»
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
y : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_14 })
h' :
  ∀ {a b : X.obj (op { obj := ⦋0⦌, property := ⋯ })} (e : Edge a b),
    ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
h₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 2 _proof_12 _proof_15).op)) y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk e₁₂)) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 0 _proof_12 _proof_15).op)) y
⊢ (((truncation 2).obj (nerve C)).spine 2 _proof_14
          (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)))).arrow
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    (((truncation 2).obj (nerve C)).spine 2 _proof_14 y).arrow ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
·

Goal state after:
case «1»
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
y : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_14 })
h' :
  ∀ {a b : X.obj (op { obj := ⦋0⦌, property := ⋯ })} (e : Edge a b),
    ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
h₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 2 _proof_12 _proof_15).op)) y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk e₁₂)) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 0 _proof_12 _proof_15).op)) y
⊢ (((truncation 2).obj (nerve C)).spine 2 _proof_14
          (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)))).arrow
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    (((truncation 2).obj (nerve C)).spine 2 _proof_14 y).arrow ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case coe.a
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z
⊢ 1 ≤ r

pp: case a
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z
⊢ r ≤ 1

Tactic:
·

Goal state after:
case coe.a
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z
⊢ 1 ≤ r
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case a
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z
⊢ r ≤ 1

Tactic:
·

Goal state after:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z
⊢ r ≤ 1
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
x : 𝕜
hf : AnalyticAt 𝕜 f x
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
⊢ r ≠ 0

Tactic:
by lia

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
x : 𝕜
hf : AnalyticAt 𝕜 f x
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
⊢ r - 1 ≠ 0

Tactic:
by lia

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

Goal state before:
pp: case neg
𝕜 : 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
⊢ ↑(n + 1) ≤ analyticOrderAt f z₀ ↔ ∀ i < n + 1, iteratedDeriv i f z₀ = 0

pp: case pos
𝕜 : 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
⊢ ↑(n + 1) ≤ analyticOrderAt f z₀ ↔ ∀ i < n + 1, iteratedDeriv i f z₀ = 0

Tactic:
·

Goal state after:
case neg
𝕜 : 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
⊢ ↑(n + 1) ≤ analyticOrderAt f z₀ ↔ ∀ i < n + 1, iteratedDeriv i f z₀ = 0
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 lia

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

Goal state before:
pp: case refine_1
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ (ComposableArrows.mk₁ (nerve.homEquiv (f.map φ))).left =
    ComposableArrows.left ((ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge)

pp: case refine_2
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ (ComposableArrows.mk₁ (nerve.homEquiv (f.map φ))).right =
    ComposableArrows.right ((ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge)

Tactic:
·

Goal state after:
case refine_1
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ (ComposableArrows.mk₁ (nerve.homEquiv (f.map φ))).left =
    ComposableArrows.left ((ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case refine_2
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ (ComposableArrows.mk₁ (nerve.homEquiv (f.map φ))).right =
    ComposableArrows.right ((ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge)

Tactic:
·

Goal state after:
case refine_2
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ (ComposableArrows.mk₁ (nerve.homEquiv (f.map φ))).right =
    ComposableArrows.right ((ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge)
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case e'_5
𝕜 : 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
x✝¹ : 𝕜 → E
x✝ : 𝕜
⊢ x✝ = x✝ - 0

pp: case convert_2
𝕜 : 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
⊢ ↑n ≤ analyticOrderAt (fun i ↦ f i - ∑ i_1 ∈ Finset.range n, (i ^ i_1 / ↑i_1.factorial) • iteratedDeriv i_1 f 0) 0

Tactic:
·

Goal state after:
case e'_5
𝕜 : 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
x✝¹ : 𝕜 → E
x✝ : 𝕜
⊢ x✝ = x✝ - 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case convert_2
𝕜 : 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
⊢ ↑n ≤ analyticOrderAt (fun i ↦ f i - ∑ i_1 ∈ Finset.range n, (i ^ i_1 / ↑i_1.factorial) • iteratedDeriv i_1 f 0) 0

Tactic:
·

Goal state after:
case convert_2
𝕜 : 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
⊢ ↑n ≤ analyticOrderAt (fun i ↦ f i - ∑ i_1 ∈ Finset.range n, (i ^ i_1 / ↑i_1.factorial) • iteratedDeriv i_1 f 0) 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case refine_1
𝕜 : 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
⊢ AnalyticAt 𝕜
    (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))
    0

pp: case refine_2
𝕜 : 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
z : 𝕜
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      z ^ n •
        (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))
          z

Tactic:
·

Goal state after:
case refine_1
𝕜 : 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
⊢ AnalyticAt 𝕜
    (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))
    0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: case zero
⊢ -(-1) ^ 0 / ↑0 = iteratedDeriv 0 log 1 / ↑(Nat.factorial 0)

pp: case succ
n : ℕ
⊢ -(-1) ^ (n + 1) / ↑(n + 1) = iteratedDeriv (n + 1) log 1 / ↑(n + 1).factorial

Tactic:
·

Goal state after:
case zero
⊢ -(-1) ^ 0 / ↑0 = iteratedDeriv 0 log 1 / ↑(Nat.factorial 0)
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case refine_2
𝕜 : 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
z : 𝕜
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      z ^ n •
        (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))
          z

Tactic:
·

Goal state after:
case refine_2
𝕜 : 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
z : 𝕜
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      z ^ n •
        (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))
          z
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:
rw [edgeMk_id, SSet.Edge.toTruncated_id, SSet.Truncated.Edge.map_id]
    exact nerve.homEquiv_id _

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

Goal state before:
pp: case pos
𝕜 : 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
z : 𝕜
hz : z ∈ U
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      z ^ n •
        (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))
          z

pp: case neg
𝕜 : 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
z : 𝕜
hz : z ∉ U
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      z ^ n •
        (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))
          z

Tactic:
·

Goal state after:
case pos
𝕜 : 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
z : 𝕜
hz : z ∈ U
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      z ^ n •
        (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))
          z
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : 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
z : 𝕜
hz : z ∉ U
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      z ^ n •
        (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))
          z

Tactic:
·

Goal state after:
case neg
𝕜 : 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
z : 𝕜
hz : z ∉ U
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      z ^ n •
        (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))
          z
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : 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
z : 𝕜
hz : z ∉ U
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      (f z - ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0)

pp: case neg.ha
𝕜 : 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
z : 𝕜
hz : z ∉ U
⊢ z ^ n ≠ 0

Tactic:
·

Goal state after:
case neg
𝕜 : 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
z : 𝕜
hz : z ∉ U
⊢ f z =
    ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 +
      (f z - ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0)
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg.ha
𝕜 : 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
z : 𝕜
hz : z ∉ U
⊢ z ^ n ≠ 0

Tactic:
·

Goal state after:
case neg.ha
𝕜 : 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
z : 𝕜
hz : z ∉ U
⊢ z ^ n ≠ 0
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
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
n : ℕ
h : ∀ i < n + 1, iteratedDeriv i f z₀ = 0
k : ℕ
hk : k < n
⊢ k + 1 < n + 1

Tactic:
by lia

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
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
n : ℕ
h : ∀ i < n, iteratedDeriv (i + 1) f z₀ = 0
k : ℕ
hk : k + 1 < n + 1
⊢ k < n

Tactic:
by lia

Goal state after: