mathlib-initiative/mathlib-tactics huggingface dataset:
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
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
e : F ≃L[𝕜] E
⊢ UniqueDiffOn 𝕜 (⇑e ⁻¹' s) ↔ UniqueDiffOn 𝕜 s

Tactic:
← e.image_symm_eq_preimage,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
e : F ≃L[𝕜] E
⊢ UniqueDiffOn 𝕜 (⇑e.symm '' s) ↔ UniqueDiffOn 𝕜 s
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: case hbc
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ∏ i_1 ∈ {i}ᶜ, ‖(Function.update (fun x ↦ g) i dg i_1) (v i_1)‖ ≤ ‖g‖ ^ (Fintype.card ι - 1) * ∏ i ∈ {i}ᶜ, ‖v i‖

Tactic:
rw [← Finset.card_singleton i, ← Finset.card_compl, ← Finset.prod_const,
        ← Finset.prod_mul_distrib]

Goal state after:
case hbc
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ∏ i_1 ∈ {i}ᶜ, ‖(Function.update (fun x ↦ g) i dg i_1) (v i_1)‖ ≤ ∏ x ∈ {i}ᶜ, ‖g‖ * ‖v x‖
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
n : ℕ
ihn : iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t
⊢ iteratedFDerivWithin 𝕜 (n + 1) f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 (n + 1) f t

Tactic:
have : fderivWithin 𝕜 _ t =ᶠ[𝓝[s] x] fderivWithin 𝕜 _ t := ihn.fderivWithin' ht

Goal state after:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
n : ℕ
ihn : iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t
this : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f₁ t) t =ᶠ[𝓝[s] x] fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t
⊢ iteratedFDerivWithin 𝕜 (n + 1) f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 (n + 1) f t
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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
x₁ : E
⊢ (∀ᶠ (x : E) in 𝓝[s] x₁, f₁ x = f x) → x₁ ∈ s → ftaylorSeriesWithin 𝕜 f₁ s x₁ = ftaylorSeriesWithin 𝕜 f s x₁

Tactic:
h₁x₁

Goal state after:
𝕜 : 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 f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
x₁ : E
h₁x₁ : ∀ᶠ (x : E) in 𝓝[s] x₁, f₁ x = f x
⊢ x₁ ∈ s → ftaylorSeriesWithin 𝕜 f₁ s x₁ = ftaylorSeriesWithin 𝕜 f s x₁
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
y : E
n : ℕ
ihn : ∀ {x : E}, s =ᶠ[𝓝[{y}ᶜ] x] t → iteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 n f t
x : E
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ iteratedFDerivWithin 𝕜 (n + 1) f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 (n + 1) f t

Tactic:
refine (eventually_nhds_nhdsWithin.2 h).mono fun y hy => ?_

Goal state after:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
y✝ : E
n : ℕ
ihn : ∀ {x : E}, s =ᶠ[𝓝[{y✝}ᶜ] x] t → iteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 n f t
x : E
h : s =ᶠ[𝓝[{y✝}ᶜ] x] t
y : E
hy : ∀ᶠ (x : E) in 𝓝[{y✝}ᶜ] y, s x = t x
⊢ iteratedFDerivWithin 𝕜 (n + 1) f s y = iteratedFDerivWithin 𝕜 (n + 1) f t y
Module: Mathlib.Analysis.Calculus.FDeriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
s : Set 𝔸
x : 𝔸
n : ℕ
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun x ↦ x ^ n) s x = ∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i

Tactic:
rw [fderivWithin_fun_pow' hxs n differentiableAt_fun_id.differentiableWithinAt,
    fderivWithin_fun_id hxs]

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
m : ℕ
hm : ¬1 + m = Fintype.card ι
⊢ ((f.toFormalMultilinearSeries.changeOriginSeries 1 m) fun x_1 ↦ x) = 0

Tactic:
rw [f.changeOriginSeries_support hm, _root_.zero_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
u : Finset ι
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
x : ι → 𝔸'
⊢ HasStrictFDerivAt (fun x ↦ (Multiset.map x u.val).prod)
    (Multiset.map (fun i ↦ (Multiset.map x (u.erase i).val).prod •> proj i) u.val).sum x

Tactic:
exact hasStrictFDerivAt_multiset_prod

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivAt c c' x
hd : HasDerivAt d d' x
hx : d x ≠ 0
⊢ HasDerivAt (fun y ↦ c y / d y) ((c' * d x - c x * d') / d x ^ 2) x

Tactic:
rw [← hasDerivWithinAt_univ] at *
  exact hc.div hd hx

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
k : ℕ
⊢ (deriv^[k] fun x ↦ x ^ m) = fun x ↦ (∏ i ∈ Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)

Tactic:
induction k with
  | zero =>
    simp only [one_mul, Int.ofNat_zero, id, sub_zero, Finset.prod_range_zero, Function.iterate_zero]
  | succ k ihk =>
    simp only [Function.iterate_succ_apply', ihk, deriv_const_mul_field', deriv_zpow',
      Finset.prod_range_succ, Int.natCast_succ, ← sub_sub, Int.cast_sub, Int.cast_natCast,
      mul_assoc]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.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
s : Set E
f : E → F
n : ℕ∞ω
inst✝ : Subsingleton F
⊢ ContDiffOn 𝕜 n (fun x ↦ 0) s

Tactic:
exact contDiffOn_const

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

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
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
⊢ HasFTaylorSeriesUpToOn n (fun y ↦ (f y, g y)) (fun y k ↦ (p y k).prod (q y k)) s

Tactic:
set L := fun m => ContinuousMultilinearMap.prodL 𝕜 (fun _ : Fin m => E) F G

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
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) → (E [×m]→L[𝕜] F) × (E [×m]→L[𝕜] G) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] F × G :=
  fun m ↦ ContinuousMultilinearMap.prodL 𝕜 (fun x ↦ E) F G
⊢ HasFTaylorSeriesUpToOn n (fun y ↦ (f y, g y)) (fun y k ↦ (p y k).prod (q y k)) s
Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft

Goal state before:
pp: case refine_2
𝕜 : 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 : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
h' : E →L[𝕜] G
lE : Filter (E × E)
lF : Filter (F × F)
hf_emb : Topology.IsEmbedding ⇑f'
htendsto : Tendsto (Prod.map g g) lE lF
hh : HasFDerivAtFilter h h' lE
hf : HasFDerivAtFilter f f' lF
hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h
ho :
  (fun x ↦
      match x with
      | (x, y) => g x - g y - g' (x - y)) =O[𝕜;
    lE] fun x ↦
    match x with
    | (x, y) => f' (g x - g y) - h' (x - y)
⊢ ((fun p ↦ p.1 - p.2) ∘ Prod.map g g) =O[𝕜; lE] fun p ↦ p.1 - p.2

Tactic:
· refine hf.isThetaTVS_sub hf_emb.isInducing |>.symm.isBigOTVS.comp_tendsto htendsto |>.trans ?_
    refine hh.isBigOTVS_sub.congr' (hcomp.mono ?_) .rfl
    simp +contextual

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

Goal state before:
pp: case zero_eq
𝕜 : 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
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
⊢ ∀ x ∈ s, (ftaylorSeriesWithin 𝕜 f s x 0).curry0 = f x

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
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
⊢ ∀ (m : ℕ),
    ↑m < n →
      ∀ x ∈ s,
        HasFDerivWithinAt (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

pp: case 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
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m) s

Tactic:
· intro x _
    simp only [ftaylorSeriesWithin, ContinuousMultilinearMap.curry0_apply,
      iteratedFDerivWithin_zero_apply]

Goal state after:
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
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
⊢ ∀ (m : ℕ),
    ↑m < n →
      ∀ x ∈ s,
        HasFDerivWithinAt (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

case 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
n : ℕ∞ω
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m) s
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

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
f : E → F
x : E
n : ℕ∞ω
⊢ ContDiffWithinAt 𝕜 n f {x}ᶜ x ↔ ContDiffAt 𝕜 n f x

Tactic:
compl_eq_univ_sdiff,

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
⊢ ContDiffWithinAt 𝕜 n f (univ \ {x}) x ↔ ContDiffAt 𝕜 n f x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

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
h : ContDiff 𝕜 ω f
⊢ AnalyticOnNhd 𝕜 f s

Tactic:
rw [← contDiffOn_univ] at h

Goal state after:
𝕜 : 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
h : ContDiffOn 𝕜 ω f univ
⊢ AnalyticOnNhd 𝕜 f s
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

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
f : E → F
n : ℕ∞
⊢ ContDiff 𝕜 (↑n) f → HasFTaylorSeriesUpTo (↑n) f (ftaylorSeries 𝕜 f)

Tactic:
rw [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ]
    exact fun h ↦ ContDiffOn.ftaylorSeriesWithin h uniqueDiffOn_univ

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_2
inst✝² : Ring 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ (if h : Nonempty (Algebra ℚ 𝔸) then (expSeries ℚ 𝔸).sum 0 else 1) = 1

Tactic:
split_ifs

Goal state after:
case pos
𝔸 : Type u_2
inst✝² : Ring 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
h✝ : Nonempty (Algebra ℚ 𝔸)
⊢ (expSeries ℚ 𝔸).sum 0 = 1

case neg
𝔸 : Type u_2
inst✝² : Ring 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
h✝ : ¬Nonempty (Algebra ℚ 𝔸)
⊢ 1 = 1
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : DivisionRing 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ ((expSeries 𝕂 𝔸 n) fun x_1 ↦ x) = x ^ n * (↑n !)⁻¹

Tactic:
← (Nat.cast_commute n ! (x ^ n)).inv_left₀.eq,

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : DivisionRing 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ ((expSeries 𝕂 𝔸 n) fun x_1 ↦ x) = (↑n !)⁻¹ * x ^ n
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

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
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
i : Fin c.length
e : E
v : Fin m → E
j : Fin c.length
hij : j ≠ i
⊢ update c.partSize i (c.partSize i + 1) j = c.partSize j

Tactic:
by simp [hij]

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

Goal state before:
pp: case mpr
s : Set ℝ
a : ℝ
h : ∃ᶠ (a_1 : ℝ) in 𝓝 0, a + a_1 ∈ Ioi a ∩ s
⊢ ∃ᶠ (t : ℝ) in 𝓝[>] 0, a + t • 1 ∈ s

Tactic:
simpa [nhdsWithin, frequently_inf_principal] using h

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : ℕ∞ω
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f ↦ f ∘SL ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f ↦ ↑e.symm ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
⊢ ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) ↑e

Tactic:
have h₁ : ContDiff 𝕜 n O₁ := contDiff_id.clm_comp contDiff_const

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : ℕ∞ω
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f ↦ f ∘SL ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f ↦ ↑e.symm ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
⊢ ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) ↑e
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

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
L : E →L[𝕜] F
r ε δ : ℝ
h : ε ≤ δ
⊢ A f L r ε ⊆ A f L r δ

Tactic:
rintro x ⟨r', r'r, hr'⟩

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε δ : ℝ
h : ε ≤ δ
x : E
r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r
⊢ x ∈ A f L r δ
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
s : Set E
inst✝ : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : u ∈ 𝓝 0
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
c : ℝ
hc₀ : 0 < c
hcr : c < r⁻¹
y : E
hy : y ∈ s
hx : gauge s ((fun x ↦ c • x) y) < r⁻¹
hrc : r < c⁻¹
⊢ (fun x ↦ c • x) y ∈ u

Tactic:
rcases hr c⁻¹ (hrc.le.trans (le_abs_self _)) hy with ⟨z, hz, rfl⟩

Goal state after:
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
s : Set E
inst✝ : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : u ∈ 𝓝 0
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
c : ℝ
hc₀ : 0 < c
hcr : c < r⁻¹
hrc : r < c⁻¹
z : E
hz : z ∈ u
hy : (fun x ↦ c⁻¹ • x) z ∈ s
hx : gauge s ((fun x ↦ c • x) ((fun x ↦ c⁻¹ • x) z)) < r⁻¹
⊢ (fun x ↦ c • x) ((fun x ↦ c⁻¹ • x) z) ∈ u
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁸ : Field R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R V
inst✝² : SeparatingDual R V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ (fun z ↦ z + ((G y)⁻¹ * G z) • (x - y)) ((fun z ↦ z + G z • (y - x)) z) = z

Tactic:
simp only [RingHom.id_apply, smul_eq_mul,
        -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `map_smulₛₗ` into `map_smulₛₗ _`
        map_add, map_smulₛₗ _, map_sub, Gx, mul_sub, mul_one, add_sub_cancel]
      rw [mul_comm (G z), ← mul_assoc, inv_mul_cancel₀ Gy]
      simp only [smul_sub, one_mul]
      abel

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

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
L : F
r ε δ : ℝ
h : ε ≤ δ
⊢ A f L r ε ⊆ A f L r δ

Tactic:
rintro x ⟨r', r'r, hr'⟩

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
L : F
r ε δ : ℝ
h : ε ≤ δ
x r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
⊢ x ∈ A f L r δ
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : ¬CompleteSpace E
⊢ HasSum (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

Tactic:
simp [integral, hE, hasSum_zero]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
inst✝ : PseudoMetrizableSpace ε
μ : Measure ℝ
a b : ℝ
hf : AEStronglyMeasurable f (μ.restrict (Ι a b))
⊢ Integrable (fun t ↦ ‖f t‖ₑ) (μ.restrict (Ι a b)) ↔ Integrable f (μ.restrict (Ι a b))

Tactic:
integrable_enorm_iff hf

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b ↦ ∫ (x : ℝ) in b₁..b₂, {x | x ≤ b}.indicator f x ∂μ
x t : ℝ
⊢ t ∈ Ι b₁ b₂ → ‖if t ≤ x then f t else 0‖ ≤ ‖f t‖

Tactic:
split_ifs

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b ↦ ∫ (x : ℝ) in b₁..b₂, {x | x ≤ b}.indicator f x ∂μ
x t : ℝ
h✝ : t ≤ x
⊢ t ∈ Ι b₁ b₂ → ‖f t‖ ≤ ‖f t‖

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b ↦ ∫ (x : ℝ) in b₁..b₂, {x | x ≤ b}.indicator f x ∂μ
x t : ℝ
h✝ : ¬t ≤ x
⊢ t ∈ Ι b₁ b₂ → ‖0‖ ≤ ‖f t‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
⊢ ‖if a ≤ b then 1 else -1‖ * ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖

Tactic:
split_ifs

Goal state after:
case pos
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
h✝ : a ≤ b
⊢ ‖1‖ * ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖

case neg
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
h✝ : ¬a ≤ b
⊢ ‖-1‖ * ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ ∈ {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}

Tactic:
split_ifs

Goal state after:
case pos
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
h✝ : a ≤ b
⊢ 1 • ∫ (x : ℝ) in Ι a b, f x ∂μ ∈ {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}

case neg
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
h✝ : ¬a ≤ b
⊢ -1 • ∫ (x : ℝ) in Ι a b, f x ∂μ ∈ {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}