mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun y ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
hy : y ∈ {0}ᶜ
⊢ ‖y‖ ≠ 0

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : 0 ≤ r
rpos : 0 < r
f : E → E := fun y ↦ x + (r * ‖y‖⁻¹) • y
A : ContinuousOn f {0}ᶜ
B : IsPathConnected {0}ᶜ
C : IsPathConnected (f '' {0}ᶜ)
y : E
hy : y ∈ {0}ᶜ
⊢ ¬y = 0
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : r < 0
⊢ IsPreconnected (sphere x r)

Tactic:
simpa using

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : 1 < Module.rank ℝ E
x : E
r : ℝ
hr : r < 0
⊢ IsPreconnected ∅
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv

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
a : E
inst✝ : CompleteSpace E
hf : HasStrictFDerivAt f (↑f') a
⊢ HasStrictFDerivAt (↑(toOpenPartialHomeomorph f hf)) (↑f') (↑(toOpenPartialHomeomorph f hf).symm (f a))

Tactic:
simpa using

Goal state after:
𝕜 : 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
a : E
inst✝ : CompleteSpace E
hf : HasStrictFDerivAt f (↑f') a
⊢ HasStrictFDerivAt f (↑f') a
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case inl
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : w a ≠ 1
hwa : w a < 1
⊢ 0 < log (w a) / log (v a)

Tactic:
simpa using

Goal state after:
case inl
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : w a ≠ 1
hwa : w a < 1
⊢ 0 < log (w a) / log (v a)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
this :
  ∀ {a : F},
    a ≠ 0 → v a ≠ 1 → ∀ {b : F}, b ≠ 0 → v b ≠ 1 → log (v b) / log (w b) ≠ log (v a) / log (w a) → 1 < v a → False
ha : v a ≤ 1
⊢ 1 < v a⁻¹

Tactic:
simpa using

Goal state after:
case inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
this :
  ∀ {a : F},
    a ≠ 0 → v a ≠ 1 → ∀ {b : F}, b ≠ 0 → v b ≠ 1 → log (v b) / log (w b) ≠ log (v a) / log (w a) → 1 < v a → False
ha : v a ≤ 1
⊢ 1 < (v a)⁻¹
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
this :
  ∀ {a : F},
    a ≠ 0 →
      v a ≠ 1 → ∀ {b : F}, b ≠ 0 → v b ≠ 1 → log (v b) / log (w b) ≠ log (v a) / log (w a) → 1 < v a → 1 < v b → False
hb : v b ≤ 1
⊢ 1 < v b⁻¹

Tactic:
simpa using

Goal state after:
case inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
this :
  ∀ {a : F},
    a ≠ 0 →
      v a ≠ 1 → ∀ {b : F}, b ≠ 0 → v b ≠ 1 → log (v b) / log (w b) ≠ log (v a) / log (w a) → 1 < v a → 1 < v b → False
hb : v b ≤ 1
⊢ 1 < (v b)⁻¹
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: case hbc
𝕜 : 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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := ⋯
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := ⋯
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
z : E
hz : z ∈ closedBall b ε
hgz : g z ∈ closedBall b ε
v : E := ⋯
⊢ ‖z + v - z‖ ≤ ↑f'symm.nnnorm * dist (f z) y

Tactic:
simpa using

Goal state after:
case hbc
𝕜 : 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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
z : E
hz : z ∈ closedBall b ε
hgz : g z ∈ closedBall b ε
v : E := f'symm.toFun (y - f z)
⊢ ‖v‖ ≤ ↑f'symm.nnnorm * ‖y - f z‖
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
z₀ : 𝕜
hf : analyticOrderAt f z₀ = ⊤
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
by unfold analyticOrderAt at hf; split_ifs at hf with h <;> simp [*] at *

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
z₀ : 𝕜
⊢ EventuallyConst f (𝓝 z₀) ↔ analyticOrderAt (fun x ↦ f x - f z₀) z₀ = ⊤

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ (∃ c, f =ᶠ[𝓝 z₀] fun x ↦ c) ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = f z₀
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
x✝ : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F)) ∧ Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
hi : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F))
right✝ : Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
x : F
h : Filter.Tendsto (fun n ↦ WithAbs.toAbs v x ^ n) Filter.atTop (𝓝 0)
⊢ Filter.Tendsto (fun n ↦ WithAbs.toAbs w x ^ n) Filter.atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
x✝ : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F)) ∧ Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
hi : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F))
right✝ : Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
x : F
h : Filter.Tendsto (fun n ↦ WithAbs.toAbs v x ^ n) Filter.atTop (𝓝 0)
⊢ Filter.Tendsto (fun n ↦ WithAbs.toAbs w x ^ n) Filter.atTop (𝓝 0)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
x✝ : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F)) ∧ Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
hi : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F))
right✝ : Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
x : F
h : Filter.Tendsto (fun n ↦ WithAbs.toAbs w x ^ n) Filter.atTop (𝓝 0)
⊢ Filter.Tendsto (fun n ↦ WithAbs.toAbs v x ^ n) Filter.atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
x✝ : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F)) ∧ Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
hi : IsEmbedding ⇑(WithAbs.congr v w (RingEquiv.refl F))
right✝ : Function.Surjective ⇑(WithAbs.congr v w (RingEquiv.refl F))
x : F
h : Filter.Tendsto (fun n ↦ WithAbs.toAbs w x ^ n) Filter.atTop (𝓝 0)
⊢ Filter.Tendsto (fun n ↦ WithAbs.toAbs v x ^ n) Filter.atTop (𝓝 0)
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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ↑n ≤ ⊤ ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
simpa using

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : u = w
⊢ (v u) (a u)⁻¹ < 1

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : u = w
⊢ a u = 0 ∨ 1 < (v u) (a u)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : u = w
hlt : (v u) (a u)⁻¹ < 1
⊢ Tendsto
    (fun i ↦
      (WithAbs.equiv (v u)).symm (1 / (1 + (a u)⁻¹ ^ i)) * (WithAbs.equiv (v u)).symm ((WithAbs.equiv (v u)) (z u)))
    atTop (𝓝 (z u))

Tactic:
simpa using

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : u = w
hlt : (v u) (a u)⁻¹ < 1
⊢ Tendsto (fun i ↦ (1 + (WithAbs.toAbs (v u) (a u) ^ i)⁻¹)⁻¹ * z u) atTop (𝓝 (z u))
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h✝ : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
x✝ : ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
hg_ne : ⋯.choose < n
this : ContinuousAt (fun z ↦ (z - z₀) ^ (n - m) • h z) z₀
⊢ (fun z ↦ (z - z₀) ^ (n - m) • h z) z₀ = 0

Tactic:
simp [m, Nat.sub_ne_zero_of_lt hg_ne]

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this✝ : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : ¬u = w
hgt : 1 < (v u) (a w)⁻¹
this : Tendsto (fun n ↦ ‖WithAbs.toAbs (v u) (1 / (1 + (a w)⁻¹ ^ n))‖) atTop (𝓝 0)
⊢ Tendsto
    (fun i ↦
      (WithAbs.equiv (v u)).symm (1 / (1 + (a w)⁻¹ ^ i)) * (WithAbs.equiv (v u)).symm ((WithAbs.equiv (v w)) (z w)))
    atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this✝ : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : ¬u = w
hgt : 1 < (v u) (a w)⁻¹
this : Tendsto (fun n ↦ ‖WithAbs.toAbs (v u) (1 / (1 + (a w)⁻¹ ^ n))‖) atTop (𝓝 0)
⊢ Tendsto (fun i ↦ (1 + (WithAbs.toAbs (v u) (a w) ^ i)⁻¹)⁻¹ * WithAbs.toAbs (v u) (z w).ofAbs) atTop (𝓝 0)
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
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z₀ = analyticOrderAt g z₀

Tactic:
refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ?_

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : AnalyticAt 𝕜 f z₀
n : ℕ
⊢ ↑n ≤ analyticOrderAt f z₀ ↔ ↑n ≤ analyticOrderAt g z₀
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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt (-f) z₀ = analyticOrderAt f z₀

Tactic:
refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ?_

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
⊢ ↑n ≤ analyticOrderAt (-f) z₀ ↔ ↑n ≤ analyticOrderAt f z₀
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 g : 𝕜 → E
z₀ : 𝕜
⊢ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f - g) z₀

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
⊢ analyticOrderAt f z₀ ≤ analyticOrderAt (f + -g) z₀ ∨ analyticOrderAt g z₀ ≤ analyticOrderAt (f + -g) z₀
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 g : 𝕜 → E
z₀ : 𝕜
hfg : analyticOrderAt f z₀ < analyticOrderAt g z₀
⊢ analyticOrderAt (f + g) z₀ ≤ analyticOrderAt f z₀

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : analyticOrderAt f z₀ < analyticOrderAt g z₀
⊢ analyticOrderAt (f + g) z₀ ≤ analyticOrderAt f z₀
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 g : 𝕜 → E
z₀ : 𝕜
hfg : analyticOrderAt f z₀ < analyticOrderAt g z₀
⊢ analyticOrderAt f z₀ ≤ analyticOrderAt (f + g) z₀

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : analyticOrderAt f z₀ < analyticOrderAt g z₀
⊢ analyticOrderAt f z₀ ≤ analyticOrderAt (f + g) z₀
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg✝ : analyticOrderAt f z₀ ≠ analyticOrderAt g z₀
hfg : analyticOrderAt f z₀ < analyticOrderAt g z₀
⊢ analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g z₀)

Tactic:
simpa using

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg✝ : analyticOrderAt f z₀ ≠ analyticOrderAt g z₀
hfg : analyticOrderAt f z₀ < analyticOrderAt g z₀
⊢ analyticOrderAt (f + g) z₀ = analyticOrderAt f z₀
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : analyticOrderAt f z₀ ≠ analyticOrderAt g z₀
hgf : analyticOrderAt g z₀ < analyticOrderAt f z₀
⊢ analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g z₀)

Tactic:
simpa using

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hfg : analyticOrderAt f z₀ ≠ analyticOrderAt g z₀
hgf : analyticOrderAt g z₀ < analyticOrderAt f z₀
⊢ analyticOrderAt (f + g) z₀ = analyticOrderAt g z₀
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case coe.e_a
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
⊢ analyticOrderAt (deriv f) x = ↑s

Tactic:
obtain ⟨U, hUf, hUo, hUx⟩ := eventually_nhds_iff.mp (hfF.and hFa.eventually_analyticAt)

Goal state after:
case coe.e_a
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
⊢ analyticOrderAt (deriv f) x = ↑s
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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
this : CauchySeq u
x : E
hx : Tendsto u atTop (𝓝 x)
xmem : x ∈ closedBall b ε
hx' : Tendsto u atTop (𝓝[closedBall b ε] x)
T1 : Tendsto (f ∘ u) atTop (𝓝 (f x))
⊢ Tendsto (fun n ↦ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y) atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
𝕜 : 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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
this : CauchySeq u
x : E
hx : Tendsto u atTop (𝓝 x)
xmem : x ∈ closedBall b ε
hx' : Tendsto u atTop (𝓝[closedBall b ε] x)
T1 : Tendsto (f ∘ u) atTop (𝓝 (f x))
⊢ Tendsto (fun n ↦ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y) atTop (𝓝 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
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
⊢ (fun z ↦ ↑(s + 1) • F z) x ≠ 0

Tactic:
simpa using

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
⊢ ¬↑s + 1 = 0 ∧ ¬F x = 0