mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order = emultiplicity X φ

Tactic:
classical
  rcases eq_or_ne φ 0 with (rfl | hφ)
  · simp
  cases ho : order φ with
  | top => simp [hφ] at ho
  | coe n =>
    have hn : φ.order.toNat = n := by simp [ho]
    rw [← hn, eq_comm]
    apply le_antisymm _
    · apply le_emultiplicity_of_pow_dvd
      apply X_pow_order_dvd
    · apply Order.le_of_lt_add_one
      rw [← not_le, ← Nat.cast_one, ← Nat.cast_add, ← pow_dvd_iff_le_emultiplicity]
      rintro ⟨ψ, H⟩
      have := congr_arg (coeff n) H
      rw [X_pow_mul, coeff_mul_of_lt_order, ← hn] at this
      · exact coeff_order hφ this
      · rw [X_pow_eq, order_monomial]
        split_ifs
        · simp
        · rw [← hn, ENat.natCast_lt_natCast]
          simp

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ divXPowOrder 1 = 1

Tactic:
ext k
  simp

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
inst✝² : UniformSpace R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : UniformSpace S
φ : R →+* S
a : σ → S
f : MvPolynomial σ R
⊢ eval₂ φ a ↑f = MvPolynomial.eval₂ φ a f

Tactic:
have : ∃ p : MvPolynomial σ R, (p : MvPowerSeries σ R) = f := ⟨f, rfl⟩
  rw [eval₂, dif_pos this]
  congr
  rw [← MvPolynomial.coe_inj, this.choose_spec]

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case succ
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
n✝ : ℕ
hn : g_min (n✝ + 1) = true
⊢ g (n✝ + 1) = true

Tactic:
simp at hn

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
i j : ℕ
hab : (q ^ i, q ^ j) ∈ (q ^ k).divisorsAntidiagonal
h :
  (q ^ i, q ^ j) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (q ^ i, q ^ j).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (q ^ i, q ^ j).2 =
    0

Tactic:
Nat.mem_divisorsAntidiagonal,

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
hq : 1 < q
k : ℕ
hs :
  Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal
i j : ℕ
hab : (q ^ i, q ^ j).1 * (q ^ i, q ^ j).2 = q ^ k ∧ q ^ k ≠ 0
h :
  (q ^ i, q ^ j) ∉
    Finset.map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ })
      (Finset.antidiagonal k)
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (q ^ i, q ^ j).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (q ^ i, q ^ j).2 =
    0
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : PowerSeries R
hf : PowerSeries.constantCoeff f = 1
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ((ofPowerSeries (p ^ k)) f) (m * n) = ((ofPowerSeries (p ^ k)) f) m * ((ofPowerSeries (p ^ k)) f) n

Tactic:
rw [ofPowerSeries_pow p hk.ne']

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : PowerSeries R
hf : PowerSeries.constantCoeff f = 1
m n : ℕ
hmn : m.Coprime n
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) (m * n) =
    ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) m *
      ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) n
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ a✝ : σ → MvPowerSeries τ S
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : IsUniformAddGroup T✝
inst✝⁹ : IsTopologicalRing T✝
inst✝⁸ : IsLinearTopology T✝ T✝
inst✝⁷ : Algebra R✝ T✝
ε : MvPowerSeries τ S →ₐ[R✝] T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ((coeff n) fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) (f * g)) =
    (coeff n) ((fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) f) * fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) g)

Tactic:
coeff_apply,

Goal state after:
σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ a✝ : σ → MvPowerSeries τ S
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : IsUniformAddGroup T✝
inst✝⁹ : IsTopologicalRing T✝
inst✝⁸ : IsLinearTopology T✝ T✝
inst✝⁷ : Algebra R✝ T✝
ε : MvPowerSeries τ S →ₐ[R✝] T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (n.prod fun s m ↦ a s ^ m) * (coeff n) (f * g) =
    (coeff n) ((fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) f) * fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) g)
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ a✝ : σ → MvPowerSeries τ S
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : IsUniformAddGroup T✝
inst✝⁹ : IsTopologicalRing T✝
inst✝⁸ : IsLinearTopology T✝ T✝
inst✝⁷ : Algebra R✝ T✝
ε : MvPowerSeries τ S →ₐ[R✝] T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ ((x.1 + x.2).prod fun s m ↦ a s ^ m) * ((coeff x.1) f * (coeff x.2) g) =
    ((coeff x.1) fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) f) *
      (coeff x.2) fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) g

Tactic:
simp only [coeff_apply]

Goal state after:
σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ a✝ : σ → MvPowerSeries τ S
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : IsUniformAddGroup T✝
inst✝⁹ : IsTopologicalRing T✝
inst✝⁸ : IsLinearTopology T✝ T✝
inst✝⁷ : Algebra R✝ T✝
ε : MvPowerSeries τ S →ₐ[R✝] T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ ((x.1 + x.2).prod fun s m ↦ a s ^ m) * (f x.1 * g x.2) =
    (x.1.prod fun s m ↦ a s ^ m) * f x.1 * ((x.2.prod fun s m ↦ a s ^ m) * g x.2)
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
h : ¬n = 0
⊢ ((coeff n) fun n ↦ (n.prod fun s m ↦ 0 ^ m) * (coeff n) x) = 0

Tactic:
simp only [coeff_apply]

Goal state after:
case neg
σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
h : ¬n = 0
⊢ (n.prod fun s m ↦ 0 ^ m) * x n = 0
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: case inl
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
U : (i : ι) → Set (E i)
x : (i : ι) → E i
r : ℝ≥0∞
c : ι → 𝕜
hr₀ : 0 < r
hI : ∅.Finite
hU : ∀ i ∈ ∅, Balanced 𝕜 (U i)
hI₀ : ∅ = univ ∨ (∃ i ∈ ∅, x i ≠ 0) ∨ (𝓝[≠] 0).NeBot
hr : ⨆ i ∈ ∅, egauge 𝕜 (U i) (x i) < r
hc : ∀ i ∈ ∅, x i ∈ c i • U i
hcr : ∀ i ∈ ∅, ‖c i‖ₑ < r
⊢ ∃ c₀, (c₀ ≠ 0 ∨ ∅ = univ) ∧ (∀ i ∈ ∅, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
obtain hι | hbot : IsEmpty ι ∨ (𝓝[≠] (0 : 𝕜)).NeBot := by simpa [@eq_comm _ ∅] using hI₀
      · use 0
        simp [@eq_comm _ ∅, hι, hr₀]
      · rcases exists_enorm_lt 𝕜 hr₀.ne' with ⟨c₀, hc₀, hc₀r⟩
        exact ⟨c₀, .inl hc₀, by simp, hc₀r⟩

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ ∑ᶠ (d : ℕ), (coeff d) P * (coeff (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ d) =
    ∑ᶠ (d : ℕ), (coeff d) P * ((coeff (n + 1 + 1)) (B ^ d) - if d = 1 then k else 0)

pp: R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ ∑ᶠ (d : ℕ), (coeff d) P * ((coeff (n + 1 + 1)) (B ^ d) - if d = 1 then k else 0) = 0

Tactic:
· refine finsum_congr fun i ↦ ?_
        · congr 1
          obtain (_ | _ | i) := i
          · simp
          · simp [← sub_eq_add_neg]
          · simp only [add_assoc, Nat.reduceAdd]
            rw [add_comm B, add_pow, map_sum, Finset.sum_eq_single (a := 0)]
            · simp
            · rintro (_ | _ | j) hj hj'
              · simp at hj'
              · simp [mul_comm (C k), hB', mul_assoc, coeff_X_pow_mul']
              · rw [← neg_mul, mul_pow, ← pow_mul, mul_comm (_ ^ _)]
                simp [mul_assoc, coeff_X_pow_mul']
            · simp

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ ∑ᶠ (d : ℕ), (coeff d) P * ((coeff (n + 1 + 1)) (B ^ d) - if d = 1 then k else 0) = 0
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
hc : 1 < ‖c‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝², non_trivial := ⋯ }
h₀ : 0 ≠ 0 ∨ ‖x‖ ≠ 0
⊢ ‖x‖ₑ ≠ 0

Tactic:
simpa [enorm, ← NNReal.coe_eq_zero] using h₀

Goal state after:
Module: Mathlib.Analysis.Calculus.TangentCone.DimOne

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
⊢ y ∈ tangentConeAt 𝕜 s x

Tactic:
apply mem_tangentConeAt_of_frequently (𝓝[≠] x) (fun z ↦ y / (z - x)) (· - x)

Goal state after:
case hd₀
𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
⊢ Tendsto (fun x_1 ↦ x_1 - x) (𝓝[≠] x) (𝓝 0)

case hds
𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
⊢ ∃ᶠ (n : 𝕜) in 𝓝[≠] x, x + (n - x) ∈ s

case hcd
𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
⊢ Tendsto (fun n ↦ (y / (n - x)) • (n - x)) (𝓝[≠] x) (𝓝 y)
Module: Mathlib.Analysis.Calculus.FDeriv.Congr

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s t : Set E
inst✝ : T1Space E
h : s =ᶠ[𝓝[≠] x] t
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x

Tactic:
exact hasFDerivWithinAt_congr_set_nhdsNE h

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Congr

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f₀ f₁ : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
⊢ f₀ =ᶠ[pure x] f₁

Tactic:
by assumption

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Const

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
s : Set E
hf : Injective ⇑(fderivWithin 𝕜 f s x)
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
nontriviality E

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
s : Set E
hf : Injective ⇑(fderivWithin 𝕜 f s x)
a✝ : Nontrivial E
⊢ DifferentiableWithinAt 𝕜 f s x
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ deriv f x = 0

Tactic:
by
  unfold deriv
  rw [fderiv_zero_of_not_differentiableAt h]
  simp

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
this✝ :
  (𝓝 0).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 0 ∧ Balanced 𝕜 (If.2 i)) fun If ↦
    If.1.pi fun i ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ x ∈ I, U x ∈ 𝓝 0
Ub : ∀ x ∈ I, Balanced 𝕜 (U x)
this :
  ∀ i ∈ I,
    ∀ᶠ (V : Set F) in (𝓝 0).smallSets,
      ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ ↑ε * egauge 𝕜 V (g x)
⊢ ∃ j ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, (egauge 𝕜 (I.pi fun i ↦ U i) fun i ↦ f i x) ≤ ↑ε * egauge 𝕜 j (g x)

Tactic:
rcases (hIf.eventually_all.mpr this).exists_mem_of_smallSets with ⟨V, hV₀, hV⟩

Goal state after:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
this✝ :
  (𝓝 0).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 0 ∧ Balanced 𝕜 (If.2 i)) fun If ↦
    If.1.pi fun i ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ x ∈ I, U x ∈ 𝓝 0
Ub : ∀ x ∈ I, Balanced 𝕜 (U x)
this :
  ∀ i ∈ I,
    ∀ᶠ (V : Set F) in (𝓝 0).smallSets,
      ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ ↑ε * egauge 𝕜 V (g x)
V : Set F
hV₀ : V ∈ 𝓝 0
hV : ∀ i ∈ I, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ ↑ε * egauge 𝕜 V (g x)
⊢ ∃ j ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, (egauge 𝕜 (I.pi fun i ↦ U i) fun i ↦ f i x) ≤ ↑ε * egauge 𝕜 j (g x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
this✝ :
  (𝓝 0).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 0 ∧ Balanced 𝕜 (If.2 i)) fun If ↦
    If.1.pi fun i ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ x ∈ I, U x ∈ 𝓝 0
Ub : ∀ x ∈ I, Balanced 𝕜 (U x)
this : ∀ i ∈ I, ∀ᶠ (V : Set F) in (𝓝 0).smallSets, ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)
⊢ ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, (egauge 𝕜 (I.pi fun i ↦ U i) fun i ↦ f i x) ≤ egauge 𝕜 j (g x)

Tactic:
rcases (hIf.eventually_all.mpr this).exists_mem_of_smallSets with ⟨V, hV₀, hV⟩

Goal state after:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
this✝ :
  (𝓝 0).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 0 ∧ Balanced 𝕜 (If.2 i)) fun If ↦
    If.1.pi fun i ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ x ∈ I, U x ∈ 𝓝 0
Ub : ∀ x ∈ I, Balanced 𝕜 (U x)
this : ∀ i ∈ I, ∀ᶠ (V : Set F) in (𝓝 0).smallSets, ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)
V : Set F
hV₀ : V ∈ 𝓝 0
hV : ∀ i ∈ I, ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)
⊢ ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, (egauge 𝕜 (I.pi fun i ↦ U i) fun i ↦ f i x) ≤ egauge 𝕜 j (g x)
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: case a
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
C : ℝ
⊢ ∃ i', ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ i'), ↑r

Tactic:
use ‖p 1‖ ⊔ C / r

Goal state after:
case h
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
C : ℝ
⊢ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ max ‖p 1‖ (C / ↑r)), ↑r
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ Metric.eball x r
this : y - x ∈ Metric.eball 0 r
⊢ x + (y - x) ∈ insert x s

Tactic:
by simpa only [add_sub_cancel] using hy.1

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ x_1, ∃ (_ : x ≤ x_1), c x_1 = 0
ti : ℕ
hti : ∀ (b : ℕ), ti ≤ b → ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ ≠ ∞
zi : ℕ
hzi : ti ≤ zi
z : c zi = 0
n : ℕ
hmn : zi ≤ n
a : ofScalars E c n = 0
⊢ ofScalars E c (n + 1) = 0

Tactic:
nontriviality E

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ x_1, ∃ (_ : x ≤ x_1), c x_1 = 0
ti : ℕ
hti : ∀ (b : ℕ), ti ≤ b → ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ ≠ ∞
zi : ℕ
hzi : ti ≤ zi
z : c zi = 0
n : ℕ
hmn : zi ≤ n
a : ofScalars E c n = 0
a✝ : Nontrivial E
⊢ ofScalars E c (n + 1) = 0
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A✝ : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : ↑r' < r
yr'_2 : ‖y‖ < ↑r'
S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n
k : ℕ
hk : ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4
A : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
w : E
hw : ‖w‖₊ < r'
i : ℕ
_hi : i ∈ Finset.range (n - k)
⊢ ‖(p (i + k)) fun x ↦ w‖ ≤ ‖p (i + k)‖ * ‖w‖ ^ (i + k)

Tactic:
exact ((p (i + k)).le_opNorm _).trans_eq (by simp)

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

Goal state before:
pp: case h
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length
j : Fin c.length
this : c ≠ Composition.single k ⋯
⊢ c.blocksFun j < n

Tactic:
Composition.ne_single_iff

Goal state after:
case h
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
c : Composition k
hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length
j : Fin c.length
this : ∀ (i : Fin c.length), c.blocksFun i < k
⊢ c.blocksFun j < n