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

Goal state before:
pp: case inr.succ
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (0, 1) ∉ {(1, 0)}

Tactic:
· decide

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : σ → R
⊢ (MvPowerSeries.monomial e) (e.prod fun s n ↦ r s ^ n) = (e.prod fun s n ↦ r s ^ n) • (MvPowerSeries.monomial e) 1

Tactic:
← map_smul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : σ → R
⊢ (MvPowerSeries.monomial e) (e.prod fun s n ↦ r s ^ n) = (MvPowerSeries.monomial e) ((e.prod fun s n ↦ r s ^ n) • 1)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_4
R : Type u_5
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (MvPowerSeries.monomial e) (r ^ e.sum fun x n ↦ n) = (e.prod fun s n ↦ r ^ n) • (MvPowerSeries.monomial e) 1

Tactic:
← map_smul,

Goal state after:
σ : Type u_4
R : Type u_5
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (MvPowerSeries.monomial e) (r ^ e.sum fun x n ↦ n) = (MvPowerSeries.monomial e) ((e.prod fun s n ↦ r ^ n) • 1)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f : MvPowerSeries σ R
⊢ weightedOrder w (-f) = weightedOrder w f

Tactic:
by_contra! h

Goal state after:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f : MvPowerSeries σ R
h : weightedOrder w (-f) ≠ weightedOrder w f
⊢ False
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℕ∞
⊢ Tendsto f l (𝓝 ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, ↑n < f a

Tactic:
by
  simp_rw [nhds_top_order, lt_top_iff_ne_top, tendsto_iInf, tendsto_principal, ENat.forall_ne_top,
    mem_Ioi]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff d) f ≠ 0
⊢ f.order ≤ ↑((weight fun x ↦ 1) d)

Tactic:
exact weightedOrder_le _ h

Goal state after:
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: key : ∀ (a : ℕ∞), ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 * x2) (a, ⊤)
a b : ℕ
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a, ↑b)

Tactic:
simp [ContinuousAt, nhds_prod_eq, tendsto_pure_nhds]

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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p < weightedOrder w f
d : σ →₀ ℕ
hd : ¬(weight w) d = p
⊢ 0 = (coeff d) 0

Tactic:
rw [map_zero]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
u : Filter ι
g : MvPowerSeries σ R
⊢ Tendsto f u (𝓝 g) ↔ ∀ (d : σ →₀ ℕ), Tendsto (fun i ↦ (coeff d) (f i)) u (𝓝 ((coeff d) g))

Tactic:
rw [nhds_pi, tendsto_pi]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
u : Filter ι
g : MvPowerSeries σ R
⊢ (∀ (i : σ →₀ ℕ), Tendsto (fun x ↦ f x i) u (𝓝 (g i))) ↔
    ∀ (d : σ →₀ ℕ), Tendsto (fun i ↦ (coeff d) (f i)) u (𝓝 ((coeff d) g))
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
hf : constantCoeff f = 0
⊢ Tendsto (fun n ↦ f ^ n) atTop (𝓝 0)

Tactic:
by
  apply isTopologicallyNilpotent_of_constantCoeff_isNilpotent
  rw [hf]
  exact IsNilpotent.zero

Goal state after:
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
hR'S : uR' • S ⊆ S
A : AddSubgroup M := AddSubgroup.closure S
r : R
i : M
hi : i ∈ A
x : M
hx : x ∈ S
⊢ r • x ∈ A

Tactic:
exact AddSubgroup.subset_closure <| hRS <| Set.smul_mem_smul trivial hx

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
this : (φ + ψ).order = φ.order
⊢ φ.order ≤ φ.order ∧ φ.order ≤ ψ.order

Tactic:
exact ⟨le_rfl, le_of_lt H⟩

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

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
⊢ ∀ x ∈ antidiagonal m, (coeff x.1) ↑((trunc n) f) * (coeff x.2) g = (coeff x.1) f * (coeff x.2) g

Tactic:
intro _ hab

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
x✝ : ℕ × ℕ
hab : x✝ ∈ antidiagonal m
⊢ (coeff x✝.1) ↑((trunc n) f) * (coeff x✝.2) g = (coeff x✝.1) f * (coeff x✝.2) g
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_2
inst✝ : Ring R
φ : R⟦X⟧
⊢ (-φ).order = φ.order

Tactic:
by_contra! h

Goal state after:
R : Type u_2
inst✝ : Ring R
φ : R⟦X⟧
h : (-φ).order ≠ φ.order
⊢ False
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : Nontrivial R
⊢ ∏' (i : ℕ), (1 - X ^ (i + 1)) ≠ 0

Tactic:
by_contra! h

Goal state after:
R : Type u_2
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : Nontrivial R
h : ∏' (i : ℕ), (1 - X ^ (i + 1)) = 0
⊢ False
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ X ^ (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder = X ^ (f * g).order.toNat * (f * g).divXPowOrder

Tactic:
rw [order_mul, ENat.toNat_add (order_eq_top.not.mpr h.1) (order_eq_top.not.mpr h.2)]

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

Goal state before:
pp: case zero
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
hn : g_min 0 = true
⊢ g 0 = true

Tactic:
gn

Goal state after:
case zero
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
hn : g_min 0 = true
⊢ true = true
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inr
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term δ s n = if n = 1 then 1 else 0

Tactic:
· rcases eq_or_ne n 1 with hn' | hn' <;>
    simp [hn, hn', delta]

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

Goal state before:
pp: case refine_2
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
n : ℕ
hn : 1 ≤ n
⊢ ‖↑n ^ (-(s + (1 - ↑x)))‖ = ↑n ^ (-s.re + x - 1)

Tactic:
simp only [norm_natCast_cpow_of_pos hn, add_re, sub_re, neg_re, ofReal_re, one_re]

Goal state after:
case refine_2
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
n : ℕ
hn : 1 ≤ n
⊢ ↑n ^ (-(s.re + (1 - x))) = ↑n ^ (-s.re + x - 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
hq : 1 < q
f : PowerSeries R
k : ℕ
⊢ ((ofPowerSeries q) f) (q ^ k) = (PowerSeries.coeff k) f

Tactic:
by
  rw [ofPowerSeries_apply hq, (Nat.pow_right_injective hq).extend_apply]

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

Goal state before:
pp: f : ℕ → ℂ
m : ℝ
h : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ m
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n ≠ 0
⊢ ‖f n‖ ≤ m * ↑n ^ (1 - 1)

Tactic:
by simp [h n hn]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
this✝ : UniformSpace R := ⊥
this : Set.range DFunLike.coe = {f | f 0 = 0}
⊢ IsClosed (Set.range DFunLike.coe)

Tactic:
rw [ArithmeticFunction.range_coe]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
this✝ : UniformSpace R := ⊥
this : Set.range DFunLike.coe = {f | f 0 = 0}
⊢ IsClosed {f | f 0 = 0}
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, (f i) n = 1 n
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
⊢ ∀ (i : ℕ), ∀ᶠ (a : Finset ι × Finset ι) in atTop ×ˢ atTop, ((∏ b ∈ a.1, f b) i, (∏ b ∈ a.2, f b) i) ∈ SetRel.id

Tactic:
prod_atTop_atTop_eq,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, (f i) n = 1 n
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
⊢ ∀ (i : ℕ), ∀ᶠ (a : Finset ι × Finset ι) in atTop, ((∏ b ∈ a.1, f b) i, (∏ b ∈ a.2, f b) i) ∈ SetRel.id
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
n✝ : σ →₀ ℕ
⊢ ((coeff n✝) fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) 0) = (coeff n✝) 0

Tactic:
simp [map_zero, coeff_apply]

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

Goal state before:
pp: R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
h : ClusterPt y (map₂ (fun x1 x2 ↦ x1 • x2) ⊤ (𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0))
⊢ ∃ α l,
    ∃ (_ : l.NeBot), ∃ c d, Tendsto d l (𝓝 0) ∧ (∀ᶠ (n : α) in l, x + d n ∈ s) ∧ Tendsto (fun n ↦ c n • d n) l (𝓝 y)

Tactic:
← map_prod_eq_map₂,

Goal state after:
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
h : ClusterPt y (map (fun p ↦ p.1 • p.2) (⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0))
⊢ ∃ α l,
    ∃ (_ : l.NeBot), ∃ c d, Tendsto d l (𝓝 0) ∧ (∀ᶠ (n : α) in l, x + d n ∈ s) ∧ Tendsto (fun n ↦ c n • d n) l (𝓝 y)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
hP' : IsUnit ((coeff 1) P)
this : Invertible ((coeff 1) P) := hP'.invertible
⊢ subst P (P.substInvOfIsUnit hP') = X

Tactic:
rw [P.substInvOfIsUnit_eq_substInv hP', P.subst_substInv_left hP]

Goal state after:
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 : E
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : ContinuousAdd E
h : s ∈ 𝓝 x
⊢ tangentConeAt 𝕜 (univ ∩ s) x = univ

Tactic:
tangentConeAt_inter_nhds h,

Goal state after:
𝕜 : 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 : E
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : ContinuousAdd E
h : s ∈ 𝓝 x
⊢ tangentConeAt 𝕜 univ x = univ
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' : F
x : 𝕜
inst✝ : PartialOrder 𝕜
⊢ HasDerivWithinAt f f' (Iio x) x ↔ HasDerivWithinAt f f' (Iic x) x

Tactic:
by
  rw [← Iic_sdiff_right, hasDerivWithinAt_sdiff_singleton]

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x y : 𝕜
⊢ (fderiv 𝕜 f x) y = deriv f x * y

Tactic:
simp [mul_comm]

Goal state after:
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
hf : HasFDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (a : E) in 𝓝 0, ‖f (x₀ + a) - f x₀‖ ≤ C * ‖x₀ + a - x₀‖
ε : ℝ
ε0 : 0 < ε
y : E
hy : ‖f (x₀ + y) - f x₀ - f' y‖ ≤ ε * ‖y‖
hyC : ‖f (x₀ + y) - f x₀‖ ≤ C * ‖y‖
⊢ ‖f' y‖ ≤ (C + ε) * ‖y‖

Tactic:
calc
    ‖f' y‖ ≤ ‖f (x₀ + y) - f x₀‖ + ‖f (x₀ + y) - f x₀ - f' y‖ := norm_le_insert _ _
    _ ≤ C * ‖y‖ + ε * ‖y‖ := add_le_add hyC hy
    _ = (C + ε) * ‖y‖ := (add_mul _ _ _).symm

Goal state after:
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✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ ↑C * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
x : α
hx : ‖f x‖ ≤ ↑C * ‖g x‖
⊢ ‖c‖ₑ * ‖f x‖ₑ / ↑r ≤ ‖c‖ₑ * (↑C * ‖g x‖ₑ) / ↑r

Tactic:
by
        gcongr
        simp only [enorm_eq_nnnorm, ← coe_nnnorm] at hx ⊢
        exact mod_cast hx

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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : y ∈ Metric.eball x r
⊢ AnalyticAt 𝕜 f y

Tactic:
← analyticWithinAt_univ

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
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : y ∈ Metric.eball x r
⊢ AnalyticWithinAt 𝕜 f univ y
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
x : E
hf : AnalyticAt 𝕜 f x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
← analyticWithinAt_univ

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
x : E
hf : AnalyticWithinAt 𝕜 f univ x
⊢ AnalyticWithinAt 𝕜 f s x
Module: Mathlib.Analysis.Analytic.Composition

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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : b.blocks[i] = k
j : Fin b.length := ⟨↑i, ⋯⟩
A : 1 < b.blocksFun j
v : Fin n → E
⊢ (p.compAlongComposition (id 𝕜 E x) b) v = 0 v

Tactic:
rw [compAlongComposition_apply, _root_.zero_apply]

Goal state after:
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
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : b.blocks[i] = k
j : Fin b.length := ⟨↑i, ⋯⟩
A : 1 < b.blocksFun j
v : Fin n → E
⊢ (p b.length) ((id 𝕜 E x).applyComposition b v) = 0
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case mpr
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
⊢ (∃ g, EqOn f g (insert x s ∩ eball x r) ∧ HasFPowerSeriesOnBall g p x r) → HasFPowerSeriesWithinOnBall f p s x r

Tactic:
intro ⟨g, hfg, hg⟩
    refine ⟨hg.r_le, hg.r_pos, ?_⟩
    intro y ys lt
    rw [hfg]
    · exact hg.hasSum lt
    · refine ⟨ys, ?_⟩
      simpa only [mem_eball, edist_eq_enorm_sub, add_sub_cancel_left, sub_zero] using lt

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
g : F → G
f : E → F
x : E
hg : AnalyticAt 𝕜 g (f x)
hf : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (g ∘ f) x

Tactic:
← analyticWithinAt_univ

Goal state after:
𝕜 : 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
g : F → G
f : E → F
x : E
hg : AnalyticWithinAt 𝕜 g Set.univ (f x)
hf : AnalyticWithinAt 𝕜 f Set.univ x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) Set.univ x
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
g : F → G
f : E → F
x : E
s : Set E
hg : AnalyticAt 𝕜 g (f x)
hf : AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
← analyticWithinAt_univ

Goal state after:
𝕜 : 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
g : F → G
f : E → F
x : E
s : Set E
hg : AnalyticWithinAt 𝕜 g Set.univ (f x)
hf : AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case zero.succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
⊢ (take (take (i + 1) b.blocks).sum a.blocks).sum = (take (i + 1) (List.map sum (a.blocks.splitWrtComposition b))).sum

Tactic:
have C : 0 < blocksFun b ⟨i, A⟩ := Composition.blocks_pos' _ _ _

Goal state after:
case zero.succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun ⟨i, A⟩
⊢ (take (take (i + 1) b.blocks).sum a.blocks).sum = (take (i + 1) (List.map sum (a.blocks.splitWrtComposition b))).sum
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
hi : i < b.length
j : ℕ
IHj :
  j < b.blocksFun ⟨i, hi⟩ →
    a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j
hj : j + 1 < b.blocksFun ⟨i, hi⟩
A : j < b.blocksFun ⟨i, hi⟩
B : j < (a.sigmaCompositionAux b ⟨i, ⋯⟩).length
C : b.sizeUpTo i + j < b.sizeUpTo (i + 1)
D : b.sizeUpTo i + j < a.length
this : b.sizeUpTo i + j.succ = (b.sizeUpTo i + j).succ
⊢ (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j + a.blocks[b.sizeUpTo i + j] =
    (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo (j + 1)

Tactic:
sizeUpTo_succ _ B

Goal state after:
case succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
hi : i < b.length
j : ℕ
IHj :
  j < b.blocksFun ⟨i, hi⟩ →
    a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j
hj : j + 1 < b.blocksFun ⟨i, hi⟩
A : j < b.blocksFun ⟨i, hi⟩
B : j < (a.sigmaCompositionAux b ⟨i, ⋯⟩).length
C : b.sizeUpTo i + j < b.sizeUpTo (i + 1)
D : b.sizeUpTo i + j < a.length
this : b.sizeUpTo i + j.succ = (b.sizeUpTo i + j).succ
⊢ (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j + a.blocks[b.sizeUpTo i + j] =
    (a.gather b).sizeUpTo i + ((a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j + (a.sigmaCompositionAux b ⟨i, ⋯⟩).blocks[j])
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
h : AnalyticWithinAt 𝕜 (fun x x_1 ↦ f x_1 x) s e
i : ι
⊢ AnalyticWithinAt 𝕜 (f i) s e

Tactic:
exact ((ContinuousLinearMap.proj (R := 𝕜) i).analyticAt _).comp_analyticWithinAt h

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
ι : 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
hf : ∀ (i : ι), AnalyticAt 𝕜 (f i) e
⊢ AnalyticAt 𝕜 (fun x x_1 ↦ f x_1 x) e

Tactic:
← analyticWithinAt_univ

Goal state after:
𝕜 : 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
hf : ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) Set.univ e
⊢ AnalyticWithinAt 𝕜 (fun x x_1 ↦ f x_1 x) Set.univ e