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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ X ^ n ∣ φ ↔ ∀ m < n, (coeff m) φ = 0

Tactic:
convert! @MvPowerSeries.X_pow_dvd_iff Unit R _ () n φ

Goal state after:
case e'_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (∀ m < n, (coeff m) φ = 0) ↔ ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
⊢ (coeff m) φ = (coeff m) (X s ^ n * fun m ↦ (coeff (m + single s n)) φ)

Tactic:
· rw [h, coeff_mul, Finset.sum_eq_zero]
      · rintro ⟨i, j⟩ hij
        rw [mem_antidiagonal] at hij
        rw [coeff_X_pow]
        split_ifs with hi
        · exfalso
          apply H
          rw [← hij, hi]
          ext
          rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]
        · exact zero_mul _
      · contrapose! H
        ext t
        by_cases hst : s = t
        · subst t
          simpa using! tsub_add_cancel_of_le H
        · simp [hst]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
g : MvPolynomial PUnit.{1} R := (MvPolynomial.uniqueAlgEquiv R PUnit.{1}).symm f
⊢ ↑f = ↑g

Tactic:
have : f = MvPolynomial.uniqueAlgEquiv R PUnit g := by simp only [g, AlgEquiv.apply_symm_apply]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
g : MvPolynomial PUnit.{1} R := (MvPolynomial.uniqueAlgEquiv R PUnit.{1}).symm f
this : f = (MvPolynomial.uniqueAlgEquiv R PUnit.{1}) g
⊢ ↑f = ↑g
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝⁵ : Field K
Γ₀ : Type u_2
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Algebra R K
inst✝¹ : UniformContinuousConstSMul R K
inst✝ : FaithfulSMul R K
⊢ Function.Injective ⇑(algebraMap R (hat K))

Tactic:
exact (FaithfulSMul.algebraMap_injective K (hat K)).comp (FaithfulSMul.algebraMap_injective R K)

Goal state after:
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Zero α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq ι
f✝ g✝ : ι →₀ α
i✝ : ι
a : α
f g : ι →₀ α
i : ι
⊢ i ∈ f.support ∪ g.support ↔ Icc (f i) (g i) ≠ 0

Tactic:
rw [mem_union, ← not_iff_not, not_or, notMem_support_iff, notMem_support_iff, not_ne_iff]
    exact Icc_eq_singleton_iff.symm

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s t : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
ht : IsLowerSet ↑t
x : σ →₀ ℕ
f g : MvPowerSeries σ R
hxs : x ∈ s
hxt : x ∈ t
i j : σ →₀ ℕ
hij : i + j = x
⊢ MvPolynomial.coeff (i, j).1 ((truncFinset R s) f) * MvPolynomial.coeff (i, j).2 ((truncFinset R t) g) =
    (coeff (i, j).1) f * (coeff (i, j).2) g

Tactic:
rw [coeff_truncFinset_of_mem _ (hs (show i ≤ x by simp [← hij]) hxs),
    coeff_truncFinset_of_mem _ (ht (show j ≤ x by simp [← hij]) hxt)]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : MonoidWithZero R
a : R
ha : IsNilpotent a
⊢ IsTopologicallyNilpotent a

Tactic:
obtain ⟨n, hn⟩ := ha
  apply tendsto_atTop_of_eventually_const (i₀ := n)
  intro i hi
  rw [← Nat.add_sub_of_le hi, pow_add, hn, zero_mul]

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
f : MvPowerSeries σ R
⊢ HasSum (fun d ↦ (monomial d) ((coeff d) f)) f

Tactic:
by
  rw [Pi.hasSum]
  intro d
  simpa using! hasSum_single d (fun d' h ↦ coeff_monomial_ne h.symm _)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n d : ℕ
⊢ ((trunc (n + 2)) X).coeff d = Polynomial.X.coeff d

Tactic:
rw [coeff_trunc, coeff_X]

Goal state after:
R : Type u_1
inst✝ : Semiring R
n d : ℕ
⊢ (if d < n + 2 then if d = 1 then 1 else 0 else 0) = Polynomial.X.coeff d
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
f : Polynomial R
⊢ eval₂ φ a ↑f = Polynomial.eval₂ φ a f

Tactic:
rw [← (MvPolynomial.uniqueAlgEquiv R Unit).apply_symm_apply f]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
φ : R →+* S
a : S
inst✝¹ : UniformSpace R
inst✝ : UniformSpace S
f : Polynomial R
⊢ eval₂ φ a ↑((MvPolynomial.uniqueAlgEquiv R Unit) ((MvPolynomial.uniqueAlgEquiv R Unit).symm f)) =
    Polynomial.eval₂ φ a ((MvPolynomial.uniqueAlgEquiv R Unit) ((MvPolynomial.uniqueAlgEquiv R Unit).symm f))
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
a : σ → MvPowerSeries τ S
x : σ → ℕ
inst✝ : Finite τ
ha : HasSubst a
i : σ
⊢ IsNilpotent (MvPolynomial.coeff 0 ((MvPowerSeries.truncTotal (x i)) (a i)))

Tactic:
← MvPolynomial.constantCoeff_eq,

Goal state after:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
a : σ → MvPowerSeries τ S
x : σ → ℕ
inst✝ : Finite τ
ha : HasSubst a
i : σ
⊢ IsNilpotent (MvPolynomial.constantCoeff ((MvPowerSeries.truncTotal (x i)) (a i)))
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
this✝ : UniformSpace R := ⊥
this : UniformSpace S := ⊥
⊢ ⇑(substAlgHom ha) = subst a

Tactic:
rw [substAlgHom_eq_aeval, coe_aeval ha.hasEval, subst_eq_eval₂]

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

Goal state before:
pp: case inl
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
⊢ 0 = f 0 / ↑0 ^ s

Tactic:
Nat.cast_zero,

Goal state after:
case inl
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
⊢ 0 = f 0 / 0 ^ s
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : n = 1
⊢ ∃ k, q ^ k = n

Tactic:
exact ⟨0, by simp [hn]⟩

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
f : MvPowerSeries σ R
inst✝ : Finite τ
x : σ → ℕ
k : ℕ
ha : HasSubst a
h : ∀ (i : σ), constantCoeff (a i) = 0
hx : ∀ (i : σ), k ≤ x i
i : σ
⊢ MvPolynomial.coeff 0 ((truncTotal (x i)) (a i)) = 0

Tactic:
← MvPolynomial.constantCoeff_eq,

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
f : MvPowerSeries σ R
inst✝ : Finite τ
x : σ → ℕ
k : ℕ
ha : HasSubst a
h : ∀ (i : σ), constantCoeff (a i) = 0
hx : ∀ (i : σ), k ≤ x i
i : σ
⊢ MvPolynomial.constantCoeff ((truncTotal (x i)) (a i)) = 0
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:
simp [egauge, iInf_lt_iff]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f φ : R⟦X⟧
hf : constantCoeff f = 0
hφ : constantCoeff φ = 0
⊢ f.order ≤ order (subst f φ)

Tactic:
simp_rw [order_eq_order]
  exact le_order_subst_right hf hφ

Goal state after:
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 : t ⊆ u
hv : t ⊆ v
i : ι
hi : i ∈ u \ t
⊢ i ∈ s

Tactic:
rw [Finset.mem_sdiff, Set.Finite.mem_toFinset, Set.notMem_compl_iff] at hi

Goal state after:
ι : 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 : t ⊆ u
hv : t ⊆ v
i : ι
hi : i ∈ u ∧ i ∈ s
⊢ i ∈ s
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 ι
hv : t ⊆ v
hu : ∀ i ∈ u \ t, i ∈ s
i : ι
hi : i ∈ v \ t
⊢ i ∈ s

Tactic:
rw [Finset.mem_sdiff, Set.Finite.mem_toFinset, Set.notMem_compl_iff] at hi

Goal state after:
ι : 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 ι
hv : t ⊆ v
hu : ∀ i ∈ u \ t, i ∈ s
i : ι
hi : i ∈ v ∧ i ∈ s
⊢ i ∈ s
Module: Mathlib.Analysis.Calculus.TangentCone.Defs

Goal state before:
pp: case refine_2
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
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)
⊢ ∀ᶠ (n : α) in l ⊓ 𝓟 {y | x + d y ∈ s}, d n ∈ (fun x_1 ↦ x + x_1) ⁻¹' s

Tactic:
· simp [eventually_inf_principal]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Semiring 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
s : Set E
x : E
inst✝¹ : T2Space E
inst✝ : Nontrivial E
h : UniqueDiffWithinAt 𝕜 s x
⊢ AccPt x (𝓟 s)

Tactic:
by_contra! h'

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Semiring 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
s : Set E
x : E
inst✝¹ : T2Space E
inst✝ : Nontrivial E
h : UniqueDiffWithinAt 𝕜 s x
h' : ¬AccPt x (𝓟 s)
⊢ False
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : (𝓝 0).HasBasis pE sE
hF : (𝓝 0).HasBasis pF sF
⊢ f =o[𝕜; l] g ↔
    ∀ (i : ιE),
      pE i → ∃ j, pF j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ ↑ε * egauge 𝕜 (sF j) (g x)

Tactic:
rw [isLittleOTVS_iff]
  refine (hE.forall_iff ?_).trans <| forall₂_congr fun _ _ ↦ hF.exists_iff ?_
  · rintro s t hsub ⟨V, hV₀, hV⟩
    exact ⟨V, hV₀, fun ε hε ↦ (hV ε hε).mono fun x ↦ le_trans <| egauge_anti _ hsub _⟩
  · refine fun s t hsub h ε hε ↦ (h ε hε).mono fun x hx ↦ hx.trans ?_
    simp only
    gcongr

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s t : Set 𝕜
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
⊢ (fun x ↦ (fderivWithin 𝕜 f₁ t x) 1) =ᶠ[𝓝[s] x] fun x ↦ (fderivWithin 𝕜 f t x) 1

Tactic:
exact h.fderivWithin' ht |>.fun_comp (fun a ↦ a 1)

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
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousSMul 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
α : Type u_4
l : Filter α
c : α → 𝕜
d : α → E
v : E
dlim : Tendsto d l (𝓝 0)
dtop : ∀ᶠ (n : α) in l, x + d n ∈ s
cdlim : Tendsto (fun n ↦ c n • d n) l (𝓝 v)
⊢ Tendsto (fun n ↦ c n • (f (x + d n) - f x)) l (𝓝 (f' v))

Tactic:
by
  have tendsto_arg : Tendsto (fun n => x + d n) l (𝓝[s] x) := by
    rw [tendsto_nhdsWithin_iff]
    exact ⟨by simpa using tendsto_const_nhds.add dlim, dtop⟩
  have := calc
    (fun n ↦ c n • (f (x + d n) - f x) - f' (c n • d n)) =o[𝕜; l] fun n ↦ c n • d n := by
      simpa [smul_sub] using h.isLittleOTVS.comp_tendsto tendsto_arg |>.smul_left c
    _ =O[𝕜; l] (1 : α → 𝕜) := cdlim.isBigOTVS_one _
  rw [isLittleOTVS_one] at this
  simpa using this.add <| ((map_continuous f').tendsto v).comp cdlim

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 t : Set E
ht : t ∈ 𝓝 x
⊢ fderivWithin 𝕜 f (s ∩ t) x = fderivWithin 𝕜 f s x

Tactic:
by
  classical
  simp [fderivWithin, hasFDerivWithinAt_inter ht, DifferentiableWithinAt]

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

Goal state before:
pp: 𝕜 : 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 𝕜 E F
f : F →L[𝕜] G
r : ℝ≥0
hr : ↑r < p.radius
⊢ (fun n ↦ ‖f.compFormalMultilinearSeries p n‖ * ↑r ^ n) =O[atTop] fun x ↦ 1

Tactic:
apply (IsBigO.trans_isLittleO _ (p.isLittleO_one_of_lt_radius hr)).isBigO

Goal state after:
𝕜 : 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 𝕜 E F
f : F →L[𝕜] G
r : ℝ≥0
hr : ↑r < p.radius
⊢ (fun n ↦ ‖f.compFormalMultilinearSeries p n‖ * ↑r ^ n) =O[atTop] fun n ↦ ‖p n‖ * ↑r ^ n
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
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := fun y ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
y : E × E
hy' : ‖y - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F := fun n ↦ ((p n) fun x_1 ↦ y.1 - x) - (p n) fun x_1 ↦ y.2 - x
hA : HasSum (fun n ↦ A (n + 2)) (f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2)
B : ℕ → ℝ := fun n ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * ((↑n + 2) * a ^ n)
n : ℕ
⊢ ‖A (n + 2)‖ ≤ ‖p (n + 2)‖ * ↑(n + 2) * ‖y - (x, x)‖ ^ (n + 1) * ‖y.1 - y.2‖

Tactic:
simpa only [Fintype.card_fin, pi_norm_const, Prod.norm_def, Pi.sub_def,
            Prod.fst_sub, Prod.snd_sub, sub_sub_sub_cancel_right] using!
            (p <| n + 2).norm_image_sub_le (fun _ => y.1 - x) fun _ => y.2 - x

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

Goal state before:
pp: m M N : ℕ
i : (n : ℕ) × (Fin n → ℕ)
⊢ i ∈ compPartialSumSource m M N ↔ (m ≤ i.fst ∧ i.fst < M) ∧ ∀ (a : Fin i.fst), 1 ≤ i.snd a ∧ i.snd a < N

Tactic:
by
  simp only [compPartialSumSource, Finset.mem_Ico, Fintype.mem_piFinset, Finset.mem_sigma]

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)) = ∏ j, r * (a ^ c.blocksFun j * p (c.blocksFun j))

Tactic:
rw [prod_mul_distrib, prod_mul_distrib, prod_pow_eq_pow_sum, Composition.sum_blocksFun,
        prod_const, 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.Composition

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

Tactic:
· simp only [heq_eq_eq, ofFn_inj] at H ⊢
    ext1 i
    ext1
    exact congrFun H i

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_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
⊢ AnalyticWithinAt 𝕜 (f ^ n) s z

Tactic:
by_cases hn : 0 ≤ n

Goal state after:
case pos
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : 0 ≤ n
⊢ AnalyticWithinAt 𝕜 (f ^ n) s z

case neg
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ AnalyticWithinAt 𝕜 (f ^ n) s z
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_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
⊢ AnalyticAt 𝕜 (f ^ n) z

Tactic:
by_cases hn : 0 ≤ n

Goal state after:
case pos
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : 0 ≤ n
⊢ AnalyticAt 𝕜 (f ^ n) z

case neg
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ AnalyticAt 𝕜 (f ^ n) z
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: case inl
𝕜 : 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
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, AntilipschitzWith C ⇑f'
⊢ ∀ᶠ (x_1 : F) in 𝓝[≠] f x, x_1 ≠ f x

pp: case inr
𝕜 : 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
s : Set E
c : F
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, AntilipschitzWith C ⇑f'
hc : f x ≠ c
⊢ ∀ᶠ (x : F) in 𝓝[≠] f x, x ≠ c

Tactic:
· exact eventually_mem_nhdsWithin

Goal state after:
case inr
𝕜 : 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
s : Set E
c : F
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, AntilipschitzWith C ⇑f'
hc : f x ≠ c
⊢ ∀ᶠ (x : F) in 𝓝[≠] f x, x ≠ c
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑x.1, ↑x.2) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ {x | (↑x.1, ↑x.2) ∈ t}
x y : Completion α
hxy : dist x y < ε
⊢ ∀ (a b : α), ε ≤ dist ↑a ↑b ∨ (↑a, ↑b) ∈ t

Tactic:
intro x y
        rw [Completion.dist_eq]
        by_cases! h : ε ≤ dist x y
        · exact Or.inl h
        · have Z := hε h
          simp only [Set.mem_ofPred_eq] at Z
          exact Or.inr Z

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

Goal state before:
pp: case fderivWithin
𝕜 : 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 : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n) f p s ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun x ↦ p x (n + 1)) s
⊢ ∀ (m : ℕ), ↑m < ↑n + 1 → ∀ x ∈ s, HasFDerivWithinAt (fun x ↦ p x m) (p x m.succ).curryLeft s x

pp: case mpr.cont
𝕜 : 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 : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n) f p s ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun x ↦ p x (n + 1)) s
⊢ ∀ (m : ℕ), ↑m ≤ ↑n + 1 → ContinuousOn (fun x ↦ p x m) s

Tactic:
· intro m hm
      by_cases h' : m < n
      · exact h.1.fderivWithin m (mod_cast h')
      · have : m = n := Nat.eq_of_lt_succ_of_not_lt (mod_cast hm) h'
        rw [this]
        exact h.2.1

Goal state after:
case mpr.cont
𝕜 : 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 : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n) f p s ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun x ↦ p x (n + 1)) s
⊢ ∀ (m : ℕ), ↑m ≤ ↑n + 1 → ContinuousOn (fun x ↦ p x m) s
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case mp
𝕜 : 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 : ℕ
⊢ HasFTaylorSeriesUpToOn (↑(n + 1)) f p s →
    (∀ 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

Tactic:
intro H
    refine ⟨H.zero_eq, H.fderivWithin 0 (Nat.cast_lt.2 (Nat.succ_pos n)), ?_⟩
    exact H.shift_of_succ

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

Goal state before:
pp: 𝕜 : 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 (n + 1) f s x =
    (⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 f s y) s)
      x

Tactic:
by
  ext m; simp [iteratedFDerivWithin_succ_apply_right hs hx]

Goal state after: