mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
⊢ (if hq : 1 < q then
      { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) (f + g)) 0, map_zero' := ⋯ }
    else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f + g))) =
    (if hq : 1 < q then { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0, map_zero' := ⋯ }
      else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f)) +
      if hq : 1 < q then
        { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0, map_zero' := ⋯ }
      else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g)

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
⊢ (if hq : 1 < q then
        { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) (f + g)) 0, map_zero' := ⋯ }
      else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f + g)))
      n =
    ((if hq : 1 < q then
          { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0, map_zero' := ⋯ }
        else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f)) +
        if hq : 1 < q then
          { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0, map_zero' := ⋯ }
        else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g))
      n
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
x : R
⊢ (if hq : 1 < q then
      {
        toFun :=
          Function.extend (fun x ↦ q ^ x) (fun x_1 ↦ (PowerSeries.coeff x_1) ((algebraMap R (PowerSeries R)) x)) 0,
        map_zero' := ⋯ }
    else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff ((algebraMap R (PowerSeries R)) x))) =
    (algebraMap R (ArithmeticFunction R)) x

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
x : R
n : ℕ
⊢ (if hq : 1 < q then
        {
          toFun :=
            Function.extend (fun x ↦ q ^ x) (fun x_1 ↦ (PowerSeries.coeff x_1) ((algebraMap R (PowerSeries R)) x)) 0,
          map_zero' := ⋯ }
      else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff ((algebraMap R (PowerSeries R)) x)))
      n =
    ((algebraMap R (ArithmeticFunction R)) x) n
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
⊢ (ofPowerSeries (q ^ k)) f = (ofPowerSeries q) (PowerSeries.subst (PowerSeries.X ^ k) f)

Tactic:
ext n

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
⊢ ((ofPowerSeries (q ^ k)) f) n = ((ofPowerSeries q) (PowerSeries.subst (PowerSeries.X ^ k) f)) n
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case pos
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : k ∣ n
⊢ (coeff n) (subst (X ^ k) f) = (algebraMap R S) ((coeff (n / k)) f)

Tactic:
rw [coeff_subst' (.X_pow hk), finsum_eq_single _ (n / k), ← pow_mul, Nat.mul_div_cancel' h,
      coeff_X_pow_self, Algebra.algebraMap_eq_smul_one]
    intro j hj
    rw [← pow_mul, coeff_X_pow, if_neg, smul_zero]
    contrapose hj
    rw [hj, Nat.mul_div_cancel_left j hk.pos]

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

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
⊢ (algebraMap R S) ((coeff (0 / k)) f) = (algebraMap R S) (constantCoeff f)

Tactic:
Nat.zero_div,

Goal state after:
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
⊢ (algebraMap R S) ((coeff 0) f) = (algebraMap R S) (constantCoeff f)
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝⁴ : CommRing R
τ : Type u_4
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
a : σ → MvPowerSeries τ S
f : MvPowerSeries σ R
inst✝¹ : Finite τ
x : σ → ℕ
k : ℕ
inst✝ : Finite σ
h : ∀ (i : σ), constantCoeff (a i) = 0
hx : ∀ (i : σ), k ≤ x i
⊢ (truncTotal k) (subst a f) = (truncTotal k) (subst (fun i ↦ ↑((truncTotal (x i)) (a i))) ↑((truncTotal k) f))

Tactic:
rw [truncTotal_subst_eq_truncTotal_sum_subst_truncTotal_of_le
      (hasSubst_of_constantCoeff_zero h) h hx,
    truncTotal_eq_sum, ← substAlgHom_apply
      (hasSubst_of_constantCoeff_zero h).truncTotal, map_sum]
  simp

Goal state after:
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
⊢ (fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) (f * g)) =
    (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:
ext n

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 : σ →₀ ℕ
⊢ ((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)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
r : R
f : R⟦X⟧
⊢ (rescale r) f = (MvPowerSeries.rescale fun x ↦ r) f

Tactic:
ext n

Goal state after:
R : Type u_2
inst✝ : CommRing R
r : R
f : R⟦X⟧
n : ℕ
⊢ (coeff n) ((rescale r) f) = (coeff n) ((MvPowerSeries.rescale fun x ↦ r) f)
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
f : MvPowerSeries σ R
a b : σ → R
⊢ (rescale b) ((rescale a) f) = (rescale (a * b)) f

Tactic:
ext n

Goal state after:
σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
f : MvPowerSeries σ R
a b : σ → R
n : σ →₀ ℕ
⊢ (coeff n) ((rescale b) ((rescale a) f)) = (coeff n) ((rescale (a * b)) f)
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
⊢ (rescale a) f = subst (a • X) f

Tactic:
ext n

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff n) ((rescale a) f) = (coeff n) (subst (a • X) f)
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), PowerSeries.constantCoeff (f i) = 1
n✝ n : ℕ
i : ι
hi : n + 1 ≤ q i
⊢ ((ofPowerSeries (q i)) (f i)) n = 1 n

Tactic:
rcases n with rfl | rfl | n

Goal state after:
case zero
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), PowerSeries.constantCoeff (f i) = 1
n : ℕ
i : ι
hi : 0 + 1 ≤ q i
⊢ ((ofPowerSeries (q i)) (f i)) 0 = 1 0

case succ.zero
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), PowerSeries.constantCoeff (f i) = 1
n : ℕ
i : ι
hi : 0 + 1 + 1 ≤ q i
⊢ ((ofPowerSeries (q i)) (f i)) (0 + 1) = 1 (0 + 1)

case succ.succ
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), PowerSeries.constantCoeff (f i) = 1
n✝ : ℕ
i : ι
n : ℕ
hi : n + 1 + 1 + 1 ≤ q i
⊢ ((ofPowerSeries (q i)) (f i)) (n + 1 + 1) = 1 (n + 1 + 1)
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)
⊢ subst P.substInv P = X

Tactic:
ext n

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
⊢ (coeff n) (subst P.substInv P) = (coeff n) X
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0∞), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ε * egauge 𝕜 V (g x)

Tactic:
obtain ⟨V, hV₀, hV⟩ := h.exists_eventuallyLE_mul U hU

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
⊢ ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0∞), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ε * egauge 𝕜 V (g x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : U ∈ 𝓝 0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V (g x)
W : Set G
hW₀ : W ∈ 𝓝 0
hW : (fun x ↦ egauge 𝕜 V (g x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 W (k x)
x : α
hx₁ : egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x)
⊢ egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x) → egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)

Tactic:
hx₂

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : U ∈ 𝓝 0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V (g x)
W : Set G
hW₀ : W ∈ 𝓝 0
hW : (fun x ↦ egauge 𝕜 V (g x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 W (k x)
x : α
hx₁ : egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x)
hx₂ : egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
⊢ egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =o[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : U ∈ 𝓝 0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
W : Set G
hW₀ : W ∈ 𝓝 0
hW : (fun x ↦ egauge 𝕜 V (g x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx₁ : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
⊢ egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x) → egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)

Tactic:
hx₂

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =o[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : U ∈ 𝓝 0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
W : Set G
hW₀ : W ∈ 𝓝 0
hW : (fun x ↦ egauge 𝕜 V (g x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx₁ : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
hx₂ : egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
⊢ egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =o[𝕜; l] k
U : Set E
hU₀ : U ∈ 𝓝 0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V (g x)
W : Set G
hW₀ : W ∈ 𝓝 0
hW : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 V (g x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx₁ : egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x)
⊢ egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x) → egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)

Tactic:
hx₂

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =o[𝕜; l] k
U : Set E
hU₀ : U ∈ 𝓝 0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V (g x)
W : Set G
hW₀ : W ∈ 𝓝 0
hW : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 V (g x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx₁ : egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x)
hx₂ : egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
⊢ egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k 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₁ : 𝕜 → F
x : 𝕜
hL : f₁ =ᶠ[𝓝 x] f
⊢ (fderiv 𝕜 f₁ x) 1 = (fderiv 𝕜 f x) 1

Tactic:
rwa [Filter.EventuallyEq.fderiv_eq]

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

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
f' : E →L[𝕜] F
x : E
s : Set E
⊢ ((fun x' ↦ f x' - f x - f' (x' - x)) =o[𝕜; 𝓝[insert x s] x] fun x' ↦ x' - x) ↔
    (fun x' ↦ f x' - f x - f' (x' - x)) =o[𝕜; 𝓝[s] x] fun x' ↦ x' - x

Tactic:
apply isLittleOTVS_insert

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
f' : E →L[𝕜] F
x : E
s : Set E
⊢ f x - f x - f' (x - x) = 0
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: 𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
⊢ constFormalMultilinearSeries 𝕜 E 0 = 0

Tactic:
ext n

Goal state after:
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
n : ℕ
x✝ : Fin n → E
⊢ (constFormalMultilinearSeries 𝕜 E 0 n) x✝ = (0 n) x✝
Module: Mathlib.Analysis.Analytic.ChangeOrigin

Goal state before:
pp: case e'_5
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
r r' : ℝ≥0
hr : ↑r + ↑r' < p.radius
n : ℕ
⊢ (fun s ↦ ‖p (n - s.card + s.card)‖₊ * r ^ s.card * r' ^ (n - s.card)) = fun s ↦
    ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))

pp: case convert_2
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
r r' : ℝ≥0
hr : ↑r + ↑r' < p.radius
n : ℕ
⊢ HasSum (fun s ↦ ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) (‖p n‖₊ * (r + r') ^ n)

Tactic:
· ext1 s
      rw [tsub_add_cancel_of_le (card_finset_fin_le _), mul_assoc]

Goal state after:
case convert_2
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
r r' : ℝ≥0
hr : ↑r + ↑r' < p.radius
n : ℕ
⊢ HasSum (fun s ↦ ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) (‖p n‖₊ * (r + r') ^ n)
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
⊢ ∀ (i : ℝ), ∃ i', ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ i), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ i'), ↑r

Tactic:
intro C

Goal state after:
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 + 1)‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ i'), ↑r
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
⊢ ∀ (i : ℝ), ∃ i', ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ i), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ i'), ↑r

Tactic:
intro C

Goal state after:
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
Module: Mathlib.Analysis.Analytic.ChangeOrigin

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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : z ∈ Metric.eball 0 (r - ‖y‖ₑ)
⊢ f (x + y + z) = (p.changeOrigin y).sum z

Tactic:
mem_eball_zero_iff,

Goal state after:
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖z‖ₑ < r - ‖y‖ₑ
⊢ f (x + y + z) = (p.changeOrigin y).sum z
Module: Mathlib.Analysis.Analytic.ChangeOrigin

Goal state before:
pp: case h'y
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
⊢ x + (y + z) ∈ insert x s

Tactic:
have : insert (x + y) s ⊆ insert (x + y) (insert x s) := by
          apply insert_subset_insert (subset_insert _ _)
        rw [insert_eq_of_mem hy] at this
        apply this
        simpa [add_assoc] using h'z

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fintype ι'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun x ↦ G) G'
m : ι → G
m' : ι' → G
⊢ ‖(f.currySum m) m'‖ ≤ (‖f‖ * ∏ i, ‖m i‖) * ∏ i, ‖m' i‖

Tactic:
simpa [Fintype.prod_sum_type, mul_assoc] using f.le_opNorm (Sum.elim m m')

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

Goal state before:
pp: case refine_2
𝕜 : 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
x : E
r : ℝ≥0∞
hf : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
⊢ ∀ {y : E}, y ∈ Metric.eball 0 r → HasSum (fun n ↦ (p n) fun x ↦ y) (f (x + y))

Tactic:
intro y hy
    rw [hf (x + y)]
    · convert! hasSum_zero
      rw [hp, zero_apply]
    · rwa [Metric.mem_eball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
        ← edist_zero_right, ← Metric.mem_eball]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
h : ofScalars E a₁✝ = ofScalars E a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext n

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
h : ofScalars E a₁✝ = ofScalars E a₂✝
n : ℕ
⊢ a₁✝ n = a₂✝ n