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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
φ : R →+* S
a : S
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformSpace S
inst✝⁶ : IsUniformAddGroup R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous ⇑φ
ha : HasEval a
ε : R⟦X⟧ → S
hε : Continuous ε
h : ∀ (p : Polynomial R), ε ↑p = Polynomial.eval₂ φ a p
⊢ ε = eval₂ φ a

Tactic:
refine MvPowerSeries.eval₂_unique hφ (hasEval ha) hε (fun p ↦ ?_)
  rw [MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, h, ← MvPolynomial.eval₂_uniqueAlgEquiv]

Goal state after:
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
ha : HasSubst a
e : σ →₀ ℕ
r : R
⊢ (substAlgHom ha) ((monomial e) r) = (algebraMap R (MvPowerSeries τ S)) r * e.prod fun s n ↦ a s ^ n

Tactic:
substAlgHom_monomial

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
ha : HasSubst a
e : σ →₀ ℕ
r : R
⊢ ((algebraMap R (MvPowerSeries τ S)) r * e.prod fun s n ↦ a s ^ n) =
    (algebraMap R (MvPowerSeries τ S)) r * e.prod fun s n ↦ a s ^ n
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

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

Tactic:
intro (a, b)

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
⊢ ∀ x ∈ n.divisorsAntidiagonal,
    Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 x.1 *
        Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 x.2 =
      0

Tactic:
intro (a, b)

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
⊢ (a, b) ∈ n.divisorsAntidiagonal →
    Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 *
        Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 =
      0
Module: Mathlib.NumberTheory.LSeries.Basic

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

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

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 : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : 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:
simp only [Finset.mem_antidiagonal] at hx

Goal state after:
σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ a✝ : σ → MvPowerSeries τ S
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : IsUniformAddGroup T✝
inst✝⁹ : IsTopologicalRing T✝
inst✝⁸ : IsLinearTopology T✝ T✝
inst✝⁷ : Algebra R✝ T✝
ε : MvPowerSeries τ S →ₐ[R✝] T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ (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.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NNNorm 𝕜
E : Type u_2
inst✝ : SMul 𝕜 E
s : Set E
x : E
r : ℝ≥0∞
⊢ egauge 𝕜 s x < r ↔ ∃ c, x ∈ c • s ∧ ‖c‖ₑ < r

Tactic:
by
  simp [egauge, iInf_lt_iff]

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 := ⊥
f : ℕ → R
⊢ f ∈ Set.range DFunLike.coe → f ∈ {f | f 0 = 0}

Tactic:
by rintro ⟨f, rfl⟩; simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x : E
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
hc : x ∈ 0 • s
⊢ x = 0

Tactic:
zero_smul_set_subset,

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x : E
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
hc : x ∈ 0
⊢ x = 0
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, Finsupp.degree d = n
e : σ →₀ ℕ
⊢ (coeff e) ((rescale (Function.const σ r)) f) = (coeff e) (r ^ n • f)

Tactic:
simp only [MvPowerSeries.coeff_rescale, map_smul, Finsupp.prod, Function.const_apply,
    Finset.prod_pow_eq_pow_sum, smul_eq_mul]

Goal state after:
σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, Finsupp.degree d = n
e : σ →₀ ℕ
⊢ (r ^ ∑ i ∈ e.support, e i) * (coeff e) f = r ^ n * (coeff e) f
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : ∀ i ∈ u \ t, i ∈ s
hv : ∀ i ∈ v \ t, i ∈ s
i : ι
w : Finset ι
hi : i ∉ w
hw' : (∀ i ∈ w, i ∈ s) → ∀ k ≤ n, (∏ x ∈ w, f x) k = 1 k
hw : ∀ i_1 ∈ insert i w, i_1 ∈ s
k : ℕ
hk : k ≤ n
j : ℕ × ℕ
hj : j ∈ k.divisorsAntidiagonal
h1 : (f i) j.1 = 1 j.1
h2 : (∏ x ∈ w, f x) j.2 = 1 j.2
⊢ (f i) j.1 * (∏ x ∈ w, f x) j.2 = 1 j.1 * 1 j.2

Tactic:
rw [h1, h2]

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

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

Tactic:
simp only [HasFDerivWithinAt, this]

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
    exact hasFDerivWithinAt_congr_set h

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

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

Tactic:
by_cases H : DifferentiableWithinAt ℝ f (Ioi x) x
  · 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
  · rw [derivWithin_zero_of_not_differentiableWithinAt H,
      derivWithin_zero_of_not_differentiableWithinAt]
    rwa [differentiableWithinAt_Ioi_iff_Ici] at H

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
f : α → E
inst✝ : ContinuousSMul 𝕜 E
hf : Tendsto f l (𝓝 0)
U : Set E
hU : U ∈ 𝓝 0
ε : ℝ≥0
hε : ε ≠ 0
c : 𝕜
hc₀ : 0 < ‖c‖
hcε : ‖c‖ < ↑ε
⊢ c ≠ 0

Tactic:
simpa using! hc₀

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‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ : ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑ε_1 * egauge 𝕜 (ball 0 ↑δ) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x)
⊢ ↑‖f x‖₊ / ↑ε ≤ ↑‖g x‖₊

Tactic:
calc
      (‖f x‖₊ / ε : ℝ≥0∞) ≤ egauge 𝕜 (ball 0 ε) (f x) := div_le_egauge_ball 𝕜 _ _
      _ ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x) := hx
      _ ≤ (δ / ‖c‖₊) * (‖c‖₊ * ‖g x‖₊ / δ) := by
        gcongr
        exacts [ENNReal.coe_div_le, egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hδ₀)]
      _ = (δ / δ) * (‖c‖₊ / ‖c‖₊) * ‖g x‖₊ := by simp only [div_eq_mul_inv]; ring
      _ ≤ 1 * 1 * ‖g x‖₊ := by gcongr <;> exact ENNReal.div_self_le_one
      _ = ‖g x‖₊ := by simp

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
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
x y : E
⊢ ‖((p.changeOriginSeriesTerm k l s hs) fun x_1 ↦ x) fun x ↦ y‖₊ ≤ ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ k

Tactic:
by
  rw [← p.nnnorm_changeOriginSeriesTerm k l s hs, ← Fin.prod_const, ← Fin.prod_const]
  apply ContinuousMultilinearMap.le_of_opNNNorm_le
  apply ContinuousMultilinearMap.le_opNNNorm

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

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
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k m : ℕ
hm : n ≤ k + m
⊢ p.changeOriginSeries k m = 0

Tactic:
changeOriginSeries

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
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k m : ℕ
hm : n ≤ k + m
⊢ ∑ s, p.changeOriginSeriesTerm k m ↑s ⋯ = 0
Module: Mathlib.Analysis.Analytic.CPolynomialDef

Goal state before:
pp: case ht
𝕜 : 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
s : (k : ℕ) × (l : ℕ) × { s // s.card = l }
hs : n ≤ s.fst + s.snd.fst
⊢ f s = 0

Tactic:
dsimp only [f]

Goal state after:
case ht
𝕜 : 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
s : (k : ℕ) × (l : ℕ) × { s // s.card = l }
hs : n ≤ s.fst + s.snd.fst
⊢ (((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y) = 0
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 t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : Metric.eball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (min r r')
y : E
hy : x + y ∈ insert x t
h'y : y ∈ Metric.eball 0 (min r r')
⊢ HasSum (fun n ↦ (p n) fun x ↦ y) (f (x + y))

Tactic:
apply Z.hasSum ?_ h'y

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 t : Set E
x : E
hst : s ∈ 𝓝[t] x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0∞
r'_pos : r' > 0
hr' : Metric.eball x r' ∩ t ⊆ s
Z : HasFPowerSeriesWithinOnBall f p s x (min r r')
y : E
hy : x + y ∈ insert x t
h'y : y ∈ Metric.eball 0 (min r r')
⊢ x + y ∈ insert x s
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
z : E
s : Set E
hU : s ∈ 𝓝 z
h : AnalyticOn 𝕜 f s
⊢ AnalyticAt 𝕜 f z

Tactic:
obtain ⟨p, hp⟩ := h z (mem_of_mem_nhds hU)
  exact ⟨p, hasFPowerSeriesWithinAt_iff_of_nhds f p hU |>.mp hp⟩

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

Tactic:
induction n using Nat.strong_induction_on with | _ n IH
   =>  _ 

Goal state after:
case h
𝕜 : 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 : ℕ
IH : ∀ m < n, p.removeZero.leftInv i x m = p.leftInv i x m
⊢ p.removeZero.leftInv i x n = p.leftInv i x 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
n : ℕ
⊢ p.removeZero.rightInv i x n = p.rightInv i x n

Tactic:
induction n using Nat.strong_induction_on with | _ n IH
   =>  _ 

Goal state after:
case h
𝕜 : 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 : ℕ
IH : ∀ m < n, p.removeZero.rightInv i x m = p.rightInv i x m
⊢ p.removeZero.rightInv i x n = p.rightInv 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
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
m M N n : ℕ
f : Fin n → ℕ
hi : (m ≤ ⟨n, f⟩.fst ∧ ⟨n, f⟩.fst < M) ∧ ∀ (a : Fin ⟨n, f⟩.fst), 1 ≤ ⟨n, f⟩.snd a ∧ ⟨n, f⟩.snd a < N
j : Fin n
hi' : f j ∈ ofFn fun a ↦ f a
⊢ 0 < f j

Tactic:
exact (hi.2 j).1

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

Goal state before:
pp: case hi
α : Type u_6
inst✝ : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
⊢ ∀ (a : (n : ℕ) × (Fin n → ℕ)) (ha : a ∈ compPartialSumSource m M N),
    compChangeOfVariables m M N a ha ∈ compPartialSumTarget m M N

Tactic:
rintro ⟨k, blocks_fun⟩ H

Goal state after:
case hi
α : Type u_6
inst✝ : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
⊢ compChangeOfVariables m M N ⟨k, blocks_fun⟩ H ∈ compPartialSumTarget m M N
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case i_inj
α : Type u_6
inst✝ : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
blocks_fun' : Fin k → ℕ
H' : ⟨k, blocks_fun'⟩ ∈ compPartialSumSource m M N
heq : compChangeOfVariables m M N ⟨k, blocks_fun⟩ H = compChangeOfVariables m M N ⟨k, blocks_fun'⟩ H'
⊢ blocks_fun = blocks_fun'

Tactic:
funext i

Goal state after:
case i_inj
α : Type u_6
inst✝ : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
blocks_fun' : Fin k → ℕ
H' : ⟨k, blocks_fun'⟩ ∈ compPartialSumSource m M N
heq : compChangeOfVariables m M N ⟨k, blocks_fun⟩ H = compChangeOfVariables m M N ⟨k, blocks_fun'⟩ H'
i : Fin k
⊢ blocks_fun i = blocks_fun' i
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
M N : ℕ
z : E
⊢ ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource 0 M N),
    ((q e.fst) fun i ↦ (p (e.snd i)) fun _j ↦ z) =
      (q.compAlongComposition p (compChangeOfVariables 0 M N e he).snd) fun _j ↦ z

Tactic:
rintro ⟨k, blocks_fun⟩ H

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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 0 M N
⊢ ((q ⟨k, blocks_fun⟩.fst) fun i ↦ (p (⟨k, blocks_fun⟩.snd i)) fun _j ↦ z) =
    (q.compAlongComposition p (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd) fun _j ↦ z
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
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
hfg : ∃ ε > 0, ∀ ⦃y : E⦄, dist y x < ε → y ∈ insert x s → f y = g y
⊢ HasFPowerSeriesWithinAt f p s x

Tactic:
rcases hfg with ⟨e, e0, hfg⟩

Goal state after:
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
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
⊢ HasFPowerSeriesWithinAt f p s x
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)
⊢ (a.sigmaCompositionAux b ⟨↑i, ⋯⟩).blocksFun ⟨↑j, ⋯⟩ = a.blocksFun ((b.embedding i) j)

Tactic:
unfold sigmaCompositionAux

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 := ⋯ }.blocksFun ⟨↑j, ⋯⟩ =
    a.blocksFun ((b.embedding i) j)
Module: Mathlib.Analysis.Calculus.FDeriv.Linear

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 →L[𝕜] F
x : E
s : Set E
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : T2Space F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (⇑f) s x = f

Tactic:
rw [DifferentiableAt.fderivWithin f.differentiableAt hxs]
  exact f.fderiv

Goal state after: