mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ (algebraMap R S) ((coeff e) f) = (coeff e) f • (coeff e) (e.prod fun s e ↦ X s ^ e)

pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ ∀ (x : σ →₀ ℕ), x ≠ e → (coeff x) f • (coeff e) (x.prod fun s e ↦ X s ^ e) = 0

Tactic:
· rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_same,
      algebra_compatible_smul S, smul_eq_mul, mul_one]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ ∀ (x : σ →₀ ℕ), x ≠ e → (coeff x) f • (coeff e) (x.prod fun s e ↦ X s ^ e) = 0
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: a : ℝ
⊢ 𝔠 ≤ #↑(Iio a)

Tactic:
have h2 : (fun x => a + a - x) '' Iio a = Ioi a := by
    simp only [image_const_sub_Iio, add_sub_cancel_right]

Goal state after:
a : ℝ
h2 : (fun x ↦ a + a - x) '' Iio a = Ioi a
⊢ 𝔠 ≤ #↑(Iio a)
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
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
d : τ →₀ ℕ
hd : ↑((Finsupp.weight w) d) < ⨅ d, ⨅ (_ : (coeff d) f ≠ 0), (Finsupp.weight (weightedOrder w ∘ a)) d
⊢ ∀ (x : σ →₀ ℕ), (coeff x) f • (coeff d) (x.prod fun s e ↦ a s ^ e) = 0

Tactic:
intro x

Goal state after:
σ : 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
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
d : τ →₀ ℕ
hd : ↑((Finsupp.weight w) d) < ⨅ d, ⨅ (_ : (coeff d) f ≠ 0), (Finsupp.weight (weightedOrder w ∘ a)) d
x : σ →₀ ℕ
⊢ (coeff x) f • (coeff d) (x.prod fun s e ↦ a s ^ e) = 0
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 : ℕ
ha : HasSubst a
hx : ∀ (i : σ), k ≤ x i
⊢ (truncTotal k) (subst a f) = (truncTotal k) (subst (fun i ↦ ↑((truncTotal (x i)) (a i))) f)

Tactic:
by
  classical
  ext d
  by_cases hd : d.degree < k
  · rw [coeff_truncTotal _ hd, coeff_truncTotal _ hd, coeff_subst ha, coeff_subst, finsum_congr]
    · intro n
      simp_rw [Finsupp.prod, coeff_prod]
      congr! 3 with l hl i hi
      obtain ⟨hl₁, -⟩ := mem_finsuppAntidiag.mp hl
      have : (l i).degree ≤ d.degree :=
        hl₁ ▸ Finsupp.degree_mono (single_le_sum_of_canonicallyOrdered hi)
      exact_mod_cast (coeff_truncTotal_pow _ (by nlinarith [hx i])).symm
    · exact ha.truncTotal
  simp_rw [coeff_truncTotal_eq_zero _ (not_lt.mp hd)]

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
⊢ (fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) 1) = 1

Tactic:
ext1 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
n : σ →₀ ℕ
⊢ ((coeff n) fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) 1) = (coeff n) 1
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
⊢ (substAlgHom ha) X = a

Tactic:
by
  rw [← Polynomial.coe_X, substAlgHom_coe, Polynomial.aeval_X]

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
n : σ →₀ ℕ
⊢ ∀ x ∈ Finset.antidiagonal n,
    (n.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:
intro x

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 : (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ x ∈ Finset.antidiagonal n →
    (n.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
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
    classical
    rw [coeff_apply, coeff_mul, coeff_mul, Finset.mul_sum]
    apply Finset.sum_congr rfl
    intro x hx
    simp only [Finset.mem_antidiagonal] at hx
    rw [← hx]
    simp only [coeff_apply]
    rw [Finsupp.prod_of_support_subset _ Finsupp.support_add,
      Finsupp.prod_of_support_subset x.1 Finset.subset_union_left,
      Finsupp.prod_of_support_subset x.2 Finset.subset_union_right]
    · simp only [← mul_assoc]
      congr 1
      rw [mul_assoc, mul_comm (f x.1), ← mul_assoc]
      congr 1
      rw [← Finset.prod_mul_distrib]
      apply Finset.prod_congr rfl
      simp [pow_add]
    all_goals {simp}

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

Goal state before:
pp: case inr
𝕜 : 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
y : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
hne : x ≠ y
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x

Tactic:
rw [hne.nhdsWithin_compl_singleton] at h

Goal state after:
case inr
𝕜 : 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
y : E
h : s =ᶠ[𝓝 x] t
hne : x ≠ y
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DivisionSemiring 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
s : Set E
x y : E
α : Type u_3
l : Filter α
inst✝ : l.NeBot
c : α → 𝕜
hc₀ : Tendsto c l (𝓝[≠] 0)
hmem : ∀ᶠ (n : α) in l, x + c n • y ∈ s
⊢ y ∈ tangentConeAt 𝕜 s x

Tactic:
rw [tendsto_nhdsWithin_iff] at hc₀
  refine mem_tangentConeAt_of_seq l c⁻¹ (c · • y) ?_ hmem ?_
  · simpa using hc₀.1.smul (tendsto_const_nhds (x := y))
  · refine tendsto_nhds_of_eventually_eq <| hc₀.2.mono fun n hn ↦ ?_
    simp_all

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

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
a : ℝ≥0
ha : a ∈ Ioo 0 1
⊢ x + id a • (y - x) ∈ ⇑(AffineMap.lineMap x y) '' Ioo 0 1

Tactic:
use a, mod_cast ha

Goal state after:
case right
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
a : ℝ≥0
ha : a ∈ Ioo 0 1
⊢ (AffineMap.lineMap x y) ↑a = x + id a • (y - 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 : 𝕜
s : Set 𝕜
h : ¬AccPt x (𝓟 s)
⊢ derivWithin f s x = 0

Tactic:
derivWithin,

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬AccPt x (𝓟 s)
⊢ (fderivWithin 𝕜 f s x) 1 = 0
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 : 𝕜
s : Set 𝕜
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ derivWithin f s x = 0

Tactic:
derivWithin,

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ (fderivWithin 𝕜 f s x) 1 = 0
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
s : Set 𝕜
hfg : EqOn f g s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ EqOn (_root_.deriv f) (_root_.deriv g) s

Tactic:
intro x

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
s : Set 𝕜
hfg : EqOn f g s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
⊢ x ∈ s → _root_.deriv f x = _root_.deriv g x
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
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen[inst✝³] u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
⊢ DifferentiableOn 𝕜 f s

Tactic:
intro x

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
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen[inst✝³] u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
x : E
⊢ x ∈ s → DifferentiableWithinAt 𝕜 f s x
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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hs : IsOpen[inst✝³] s
ht : IsOpen[inst✝³] t
⊢ DifferentiableOn 𝕜 f (s ∪ t)

Tactic:
intro x

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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hs : IsOpen[inst✝³] s
ht : IsOpen[inst✝³] t
x : E
⊢ x ∈ s ∪ t → DifferentiableWithinAt 𝕜 f (s ∪ t) x
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

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
x : E
⊢ HasFDerivWithinAt f f' univ x ↔ Tendsto (fun x' ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) (𝓝 x) (𝓝 0)

Tactic:
hasFDerivWithinAt_iff_tendsto,

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
x : E
⊢ Tendsto (fun x' ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) (𝓝[univ] x) (𝓝 0) ↔
    Tendsto (fun x' ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - 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✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
z : F
⊢ (p.unshift z).shift = p

Tactic:
ext1 n

Goal state after:
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
z : F
n : ℕ
⊢ (p.unshift z).shift n = p n
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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : ↑r < p.radius
k : ℕ
⊢ Summable fun s ↦ ‖p (k + s.fst)‖₊ * r ^ s.fst

Tactic:
rcases ENNReal.lt_iff_exists_add_pos_lt.1 hr with ⟨r', h0, hr'⟩
  simpa only [mul_inv_cancel_right₀ (pow_pos h0 _).ne'] using
    ((NNReal.summable_sigma.1 (p.changeOriginSeries_summable_aux₁ hr')).1 k).mul_right (r' ^ k)⁻¹

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

Goal state before:
pp: 𝕜 : 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
h : 0 < p.radius
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < p.radius
rpos : 0 < ↑r
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
⊢ ∃ C r, ∃ (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n

Tactic:
refine ⟨C, r⁻¹, Cpos, by simp only [inv_pos, rpos], fun n => ?_⟩

Goal state after:
𝕜 : 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
h : 0 < p.radius
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < p.radius
rpos : 0 < ↑r
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
n : ℕ
⊢ ‖p n‖ ≤ C * (↑r)⁻¹ ^ n
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : 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
h : 0 < p.radius
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < p.radius
rpos : 0 < ↑r
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
n : ℕ
⊢ ‖p n‖ ≤ C * (↑r ^ n)⁻¹

Tactic:
← div_eq_mul_inv

Goal state after:
𝕜 : 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
h : 0 < p.radius
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < p.radius
rpos : 0 < ↑r
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
n : ℕ
⊢ ‖p n‖ ≤ C / ↑r ^ n
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G
⊢ f.uncurryLeft.curryLeft = f

Tactic:
by
  ext m x
  rw [ContinuousMultilinearMap.curryLeft_apply, ContinuousLinearMap.uncurryLeft_apply, tail_cons,
    cons_zero]

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
c : ℕ → 𝕜
inst✝ : Subsingleton E
⊢ ∀ (n : ℕ) (x : Fin n → E), (c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) x = (0 n) x

Tactic:
exact fun _ _ ↦ Subsingleton.allEq _ _

Goal state after:
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
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y : E
⊢ AnalyticOnNhd 𝕜 (fun z ↦ f (z - y)) (s + {y})

Tactic:
intro x

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
f : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
⊢ x ∈ s + {y} → AnalyticAt 𝕜 (fun z ↦ f (z - y)) x
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
s : Set E
hf : AnalyticOn 𝕜 f s
y : E
⊢ AnalyticOn 𝕜 (fun z ↦ f (z - y)) (s + {y})

Tactic:
intro x

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
f : E → F
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
⊢ x ∈ s + {y} → AnalyticWithinAt 𝕜 (fun z ↦ f (z - y)) (s + {y}) x
Module: Mathlib.Analysis.Analytic.CPolynomialDef

Goal state before:
pp: case hs
𝕜 : 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
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
⊢ (⋃ i, range (Sigma.mk ↑i)).Finite

Tactic:
exact finite_iUnion fun _ ↦ finite_range _

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

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
p : FormalMultilinearSeries 𝕜 E F
x : E
⊢ p.comp (id 𝕜 E x) = p

Tactic:
ext1 n

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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
⊢ p.comp (id 𝕜 E x) n = p n
Module: Mathlib.Analysis.Analytic.Composition

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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
⊢ (id 𝕜 F ((p 0) v0)).comp p = p

Tactic:
ext1 n

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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
⊢ (id 𝕜 F ((p 0) v0)).comp p n = p n
Module: Mathlib.Analysis.Analytic.Inverse

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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
⊢ p.removeZero.leftInv i x = p.leftInv i x

Tactic:
ext1 n

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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n : ℕ
⊢ p.removeZero.leftInv i x n = p.leftInv i x n
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ ↑rp < p.radius
hrq : rq < 1 ∧ ↑rq < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
Cp : ℝ≥0
hCp1 : Cp ≥ 1
hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp
r0 : ℝ≥0 := (4 * Cp)⁻¹
r0_pos : 0 < r0
r : ℝ≥0 := rp * rq * r0
r_pos : 0 < r
n : ℕ
c : Composition n
A : ‖q c.length‖₊ * rq ^ n ≤ Cq
B : (∏ i, ‖p (c.blocksFun i)‖₊) * rp ^ n ≤ Cp ^ n
⊢ Cq * Cp ^ n * (4 * Cp)⁻¹ ^ n = Cq / 4 ^ n

Tactic:
simp [field, mul_pow]

Goal state after: