mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (fun x ↦ a + a - x) '' Ioi a = Iio a

Tactic:
convert! @image_const_sub_Ioi ℝ _ _ _

Goal state after:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (fun x ↦ a + a - x) '' Ioi a = Iio a ↔ ∀ (a b : ℝ), (fun x ↦ a - x) '' Ioi b = Iio (a - b)
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
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✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
hε : Continuous ⇑ε
⊢ ε.comp (substAlgHom ha) = aeval ⋯

Tactic:
by
  ext f
  simp only [AlgHom.coe_comp, substAlgHom_eq_aeval ha]
  exact DFunLike.congr_fun (comp_aeval ha.hasEval hε) f

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inl
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n ↦ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
⊢ ‖term f s 0‖ ≤ ‖↑C / ↑0 ^ (s + (1 - ↑x))‖

pp: case inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n ↦ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
hn : n > 0
⊢ ‖term f s n‖ ≤ ‖↑C / ↑n ^ (s + (1 - ↑x))‖

Tactic:
· simpa only [term_zero, norm_zero] using norm_nonneg _

Goal state after:
case inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n ↦ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
hn : n > 0
⊢ ‖term f s n‖ ≤ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
x : R
hq : 1 < q
k : ℕ
⊢ Function.extend (fun x ↦ q ^ x) (fun x_1 ↦ (PowerSeries.coeff x_1) (x • 1)) 0 (q ^ k) = (x • 1) (q ^ k)

Tactic:
simp [(Nat.pow_right_injective hq).extend_apply, one_apply, hq.ne']

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖
C' : ℝ := max C ((insert 0 (image (fun n ↦ ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : n < m
⊢ ‖f n‖ ≤ C' * ↑n ^ (x - 1)

Tactic:
have hn' : 0 < n := Nat.pos_of_ne_zero hn₀
    refine (div_le_iff₀ <| rpow_pos_of_pos (cast_pos.mpr hn') _).mp ?_
    refine (le_max' _ _ <| mem_insert_of_mem ?_).trans <| le_max_right ..
    exact mem_image.mpr ⟨n, mem_range.mpr hn, rfl⟩

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

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

Tactic:
have hc0 (i : ι) (hi : i ∈ I) : c i = 0 := by simpa [H] using hc_max hi

Goal state after:
case neg
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : ι → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
hr₀ : 0 < r
hIne : I.Nonempty
i₀ : ι
hi₀I : i₀ ∈ I
hc_max : IsMaxOn (fun x ↦ ‖c x‖ₑ) I i₀
H : c i₀ = 0 ∧ I ≠ univ
hc0 : ∀ i ∈ I, c i = 0
⊢ ∃ c₀, (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Tactic:
have A := H.hasDerivWithinAt.Ici_of_Ioi
    have B := (differentiableWithinAt_Ioi_iff_Ici.1 H).hasDerivWithinAt
    simpa using (uniqueDiffOn_Ici x).eq self_mem_Ici A B

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
x : E
s : Set E
inst✝ : T1Space E
y : E
⊢ DifferentiableWithinAt 𝕜 f (insert y s) x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
by
  simp only [DifferentiableWithinAt, hasFDerivWithinAt_insert]

Goal state after:
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: 𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
⊢ p.order = 0 ↔ p = 0 ∨ p 0 ≠ 0

Tactic:
simpa [order, Nat.sInf_eq_zero, FormalMultilinearSeries.ext_iff, eq_empty_iff_forall_notMem]
    using or_comm

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

Goal state before:
pp: case mp
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
h : ∀ (i : ℝ), 0 < i → ∃ j, 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ≥0
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 ↑r) (g x)
hr₀ : 0 < r
x : α
hx : egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 ↑r) (g x)
⊢ ‖f x‖ₑ ≤ ↑(‖c‖₊ / r) * ‖g x‖ₑ

Tactic:
calc
      ‖f x‖ₑ ≤ egauge 𝕜 (ball 0 1) (f x) := le_egauge_ball_one ..
      _ ≤ egauge 𝕜 (ball 0 r) (g x) := hx
      _ ≤ ‖c‖ₑ * ‖g x‖ₑ / ↑r :=
        egauge_ball_le_of_one_lt_norm hc <| .inl hr₀.ne'
      _ = (‖c‖₊ / r : ℝ≥0) * ‖g x‖ₑ := by
        simp [hr₀.ne', ENNReal.mul_div_right_comm, enorm_eq_nnnorm]

Goal state after:
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
x : E
k : ℕ
h : ↑‖x‖₊ < p.radius
⊢ ‖p.changeOrigin x k‖₊ ≤ ∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst

Tactic:
refine tsum_of_nnnorm_bounded ?_ fun l => p.nnnorm_changeOriginSeries_apply_le_tsum k l x
  have := p.changeOriginSeries_summable_aux₂ h k
  refine HasSum.sigma this.hasSum fun l => ?_
  exact ((NNReal.summable_sigma.1 this).1 l).hasSum

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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →ₗᵢ[𝕜] F
h : Nontrivial E
⊢ p.radius ≤ (p.compContinuousLinearMap u.toContinuousLinearMap).radius

Tactic:
· simpa [u.norm_toContinuousLinearMap]
      using div_le_radius_compContinuousLinearMap p u.toContinuousLinearMap

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
hn : n > 0
⊢ ‖c n‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖ ≤ ‖c n‖

Tactic:
exact (mul_le_of_le_one_right (norm_nonneg _)
    (ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos hn))

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' < r⁻¹
⊢ ↑r' ≤ (ofScalars E c).radius

Tactic:
NNReal.lt_inv_iff_mul_lt hr

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
⊢ ↑r' ≤ (ofScalars E c).radius
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
⊢ ↑r⁻¹ ≤ (ofScalars E c).radius

Tactic:
refine le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
  rw [coe_lt_coe, NNReal.lt_inv_iff_mul_lt hr] at hr'
  by_cases hrz : r' = 0
  · simp [hrz]
  apply FormalMultilinearSeries.le_radius_of_summable_norm
  refine Summable.of_norm_bounded_eventually (g := fun n ↦ ‖‖c n‖ * r' ^ n‖) ?_ ?_
  · refine summable_of_ratio_test_tendsto_lt_one hr' ?_ ?_
    · refine (hc.eventually_ne (NNReal.coe_ne_zero.mpr hr)).mp (Eventually.of_forall ?_)
      simp_all
    · simp_rw [norm_norm]
      exact tendsto_succ_norm_div_norm c hrz hc
  · filter_upwards [eventually_cofinite_ne 0] with n hn
    simp only [norm_mul, norm_norm, norm_pow, NNReal.norm_eq]
    gcongr
    exact ofScalars_norm_le E c n (Nat.pos_iff_ne_zero.mpr hn)

Goal state after:
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
n : ℕ
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
f : F [×c.length]→L[𝕜] G
v : Fin n → E
⊢ ‖f‖ * ∏ i, ‖p.applyComposition c v i‖ ≤ ‖f‖ * ∏ i, ‖p (c.blocksFun i)‖ * ∏ j, ‖(v ∘ ⇑(c.embedding i)) j‖

Tactic:
gcongr with i
      apply ContinuousMultilinearMap.le_opNorm

Goal state after:
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
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
c : Composition n
x✝ : c ∈ univ
h : ¬1 < c.length
⊢ 1 ≤ c.length

Tactic:
exact c.length_pos_of_pos hn

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

Goal state before:
pp: case a.a
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
a✝¹ : k ∈ Ico 2 (n + 1)
c : Composition k
a✝ : c ∈ {c | 1 < c.length}.toFinset
⊢ a ^ k * (r ^ c.length * ∏ j, p (c.blocksFun j)) = r ^ #univ * (a ^ k * ∏ x, p (c.blocksFun x))

Tactic:
card_fin

Goal state after:
case a.a
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
a✝¹ : k ∈ Ico 2 (n + 1)
c : Composition k
a✝ : c ∈ {c | 1 < c.length}.toFinset
⊢ a ^ k * (r ^ c.length * ∏ j, p (c.blocksFun j)) = r ^ c.length * (a ^ k * ∏ x, p (c.blocksFun 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
⊢ ∃ t ∈ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r] y,
    ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun y ↦ f (x + y)) y, (fun n y ↦ p.partialSum n y) n y) ∈ u

Tactic:
have : Metric.eball (0 : E) r' ∈ 𝓝 y := IsOpen.mem_nhds Metric.isOpen_eball yr'

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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
this : Metric.eball 0 ↑r' ∈ 𝓝 y
⊢ ∃ t ∈ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r] y,
    ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun y ↦ f (x + y)) y, (fun n y ↦ p.partialSum n y) n y) ∈ u
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
ys : x + y ∈ insert x s
yr : ‖y‖ < r ∧ edist y 0 < t
⊢ y ∈ eball 0 t

Tactic:
simp only [mem_eball, yr]

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

Goal state before:
pp: n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i ↦ (⟨a, b⟩.snd i).blocks) = ofFn fun i ↦ (⟨a', b'⟩.snd i).blocks
⊢ ⟨a, b⟩ = ⟨a', b'⟩

Tactic:
dsimp at H

Goal state after:
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i ↦ (b i).blocks) = ofFn fun i ↦ (b' i).blocks
⊢ ⟨a, b⟩ = ⟨a', b'⟩
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
⊢ b.blocks[↑i] = b.blocksFun i

Tactic:
blocksFun,

Goal state after:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
⊢ b.blocks[↑i] = b.blocks.get i
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
j : Fin (b.blocksFun i)
⊢ { blocks := (a.blocks.splitWrtComposition b)[↑⟨↑i, ⋯⟩], blocks_pos := ⋯, blocks_sum := ⋯ }.blocksFun ⟨↑j, ⋯⟩ =
    a.blocksFun ((b.embedding i) j)

Tactic:
blocksFun,

Goal state after:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
j : Fin (b.blocksFun i)
⊢ { blocks := (a.blocks.splitWrtComposition b)[↑⟨↑i, ⋯⟩], blocks_pos := ⋯, blocks_sum := ⋯ }.blocks.get ⟨↑j, ⋯⟩ =
    a.blocksFun ((b.embedding i) j)
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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ Metric.eball 0 q.radius
y : E
hy : Tendsto (fun a ↦ q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x ↦ 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : f (x + y) - f x ∈ Metric.eball 0 q.radius
u : Set G
hu : u ∈ 𝓝 (g (f (x + y)))
u_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
v : Set G
vu : v ⊆ u
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
hv : g (f (x + y)) ∈ v
⊢ ∃ a₀ b₀, ∀ (a b : ℕ), a₀ ≤ a → b₀ ≤ b → q.partialSum a (p.partialSum b y - (p 0) fun x ↦ 0) ∈ v

Tactic:
simpa using hy (v_open.mem_nhds hv)

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

Goal state before:
pp: case hbc
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : ↑r' < (pi p).radius
C : ℝ
hC : ∀ (n : ℕ), ‖pi p n‖ * ↑r' ^ n ≤ C
n : ℕ
⊢ ‖p i n‖ ≤ ‖ContinuousMultilinearMap.pi fun i ↦ p i n‖

Tactic:
ContinuousMultilinearMap.opNorm_pi

Goal state after:
case hbc
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : ↑r' < (pi p).radius
C : ℝ
hC : ∀ (n : ℕ), ‖pi p n‖ * ↑r' ^ n ≤ C
n : ℕ
⊢ ‖p i n‖ ≤ ‖fun i ↦ p i n‖
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
hr : 0 < r
i : ι
⊢ r ≤ (p i).radius

Tactic:
exact (hf i).r_le

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_7
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
hf : AnalyticAt 𝕜 f z
n : ℕ
⊢ AnalyticAt 𝕜 (f ^ n) z

Tactic:
rw [← analyticWithinAt_univ] at hf ⊢
  exact hf.pow n

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
s : Set E
p : FormalMultilinearSeries 𝕜' E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
exact ⟨p.restrictScalars 𝕜, hp.restrictScalars⟩

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜' E F
hp : HasFPowerSeriesAt f p x
⊢ AnalyticAt 𝕜 f x

Tactic:
exact ⟨p.restrictScalars 𝕜, hp.restrictScalars⟩

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

Goal state before:
pp: case hasSum
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
y : A
hy : ‖y‖ < 1
⊢ HasSum (fun n ↦ y ^ n) (∑' (n : ℕ), y ^ n)

Tactic:
exact (summable_geometric_of_norm_lt_one hy).hasSum

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

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 g : E → F
x : E
hg : DifferentiableAt 𝕜 g x
⊢ DifferentiableAt 𝕜 (f - g) x ↔ DifferentiableAt 𝕜 f x

Tactic:
simp only [sub_eq_add_neg, differentiableAt_neg_iff, hg, add_iff_left]

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

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
x a : E
⊢ DifferentiableAt 𝕜 (fun x ↦ f (a + x)) x ↔ DifferentiableAt 𝕜 f (a + x)

Tactic:
simp [DifferentiableAt, hasFDerivAt_comp_add_left]

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

Goal state before:
pp: case hcd
𝕜 : 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
s : Set E
f' : E →L[𝕜] F
x : E
h : HasFDerivWithinAt f f' s x
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ Tendsto (fun n ↦ c n • (f (x + d n) - f x)) l (𝓝 (f' y))

Tactic:
exact h.lim hd₀ hds hcd

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
x : E
G : Type u_4
inst✝³ : GroupWithZero G
inst✝² : DistribMulAction G E
inst✝¹ : ContinuousConstSMul G E
inst✝ : SMulCommClass G 𝕜 E
c : G
hc : c ≠ 0
h : UniqueDiffWithinAt 𝕜 (c • s) (c • x)
⊢ UniqueDiffWithinAt 𝕜 s x

Tactic:
by simpa [hc] using h.smul (inv_ne_zero hc)

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ (∀ x ∈ s, (p x 0).curry0 = f x) ∧
      (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x) ∧
        HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s →
    HasFTaylorSeriesUpToOn (↑(n + 1)) f p s

Tactic:
rintro ⟨Hzero_eq, Hfderiv_zero, Htaylor⟩
    constructor
    · exact Hzero_eq
    · intro m (hm : (m : ℕ∞ω) < n.succ) x (hx : x ∈ s)
      rcases m with - | m
      · exact Hfderiv_zero x hx
      · have A : (m : ℕ∞ω) < n := by
          rw [Nat.cast_lt] at hm ⊢
          exact Nat.lt_of_succ_lt_succ hm
        have :
          HasFDerivWithinAt (𝕜 := 𝕜) (continuousMultilinearCurryRightEquiv' 𝕜 m E F ∘ (p · m.succ))
            ((p x).shift m.succ).curryLeft s x := Htaylor.fderivWithin _ A x hx
        rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff'
            (f' := ((p x).shift m.succ).curryLeft)] at this
        convert! this
        ext y v
        change
          (p x (Nat.succ (Nat.succ m))) (cons y v) =
            (p x m.succ.succ) (snoc (cons y (init v)) (v (last _)))
        rw [← cons_snoc_eq_snoc_cons, snoc_init_self]
    · intro m (hm : (m : ℕ∞ω) ≤ n.succ)
      rcases m with - | m
      · have : DifferentiableOn 𝕜 (fun x => p x 0) s := fun x hx =>
          (Hfderiv_zero x hx).differentiableWithinAt
        exact this.continuousOn
      · refine (continuousMultilinearCurryRightEquiv' 𝕜 m E F).comp_continuousOn_iff.mp ?_
        refine Htaylor.cont _ ?_
        rw [Nat.cast_le] at hm ⊢
        exact Nat.lt_succ_iff.mp hm

Goal state after: