mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case coe.a
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z
hr : r < 1
⊢ False

Tactic:
have := hfF.self_of_nhds

Goal state after:
case coe.a
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z
hr : r < 1
this : f x - f x = (x - x) ^ r • F x
⊢ False
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
⊢ DifferentiableAt 𝕜 (fun x_1 ↦ (x_1 - x) ^ r) x

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
⊢ DifferentiableAt 𝕜 F x

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
⊢ DifferentiableAt 𝕜 (fun x_1 ↦ x_1 - x) x

Tactic:
by fun_prop

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

Goal state before:
pp: case a
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
⊢ 0 + 0 = 0

Tactic:
add_zero

Goal state after:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
⊢ 0 = 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CharZero 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
horder : analyticOrderAt f z₀ = ↑n + 1
⊢ analyticOrderAt (deriv f) z₀ = ↑n

Tactic:
have ⟨g, hg, hg₀, hfg⟩ := (AnalyticAt.analyticOrderAt_eq_natCast hf).1 horder
  have hz₀ : f z₀ = 0 := by
    simpa [sub_self, zero_pow, zero_smul] using Filter.Eventually.self_of_nhds hfg
  simpa [hz₀, sub_zero, horder] using hf.analyticOrderAt_deriv_add_one

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
hf : AnalyticAt 𝕜 f 0
n : ℕ
this : AnalyticAt 𝕜 (fun z ↦ ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0) 0
i : ℕ
hi : i < n
⊢ AnalyticAt 𝕜 f 0

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
n : ℕ
⊢ AnalyticAt 𝕜 ((fun x ↦ x - z₀) ^ n) z₀

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : analyticOrderAt f (g z₀) = ⊤
⊢ AnalyticAt 𝕜 (fun x ↦ g x - g z₀) z₀

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
hs : analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ↑s
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
⊢ AnalyticAt 𝕜 (fun x ↦ g x - g z₀) z₀

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
G : 𝕜 → 𝕜
hGa : AnalyticAt 𝕜 G z₀
hGne : G z₀ ≠ 0
hgG : ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z - g z₀ = (z - z₀) ^ s • G z
⊢ AnalyticAt 𝕜 (fun z ↦ G z ^ r • F (g z)) z₀

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
x✝ : MeromorphicAt g x
⊢ MeromorphicAt (f + g) x

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
x✝ : MeromorphicAt g x
⊢ MeromorphicAt (f - g) x

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hg : MeromorphicAt g x
x✝ : MeromorphicAt f x
⊢ MeromorphicAt (f - g) x

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) x
this : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt (fun z ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ContinuousAt (fun z ↦ (z - x) ^ n • f z) y
h'y : ¬y = x
⊢ ContinuousAt (fun z ↦ (z - x) ^ n) y

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z₀ : 𝕜
h₁ : AnalyticAt 𝕜 g z₀
h₂ : z₀ ∈ {x}ᶜ
⊢ DifferentiableAt 𝕜 (fun x_1 ↦ x_1 - x) z₀

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
z₀ : 𝕜
h₁ : AnalyticAt 𝕜 g z₀
h₂ : z₀ ∈ {x}ᶜ
⊢ DifferentiableAt 𝕜 g z₀

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt 𝕜' (fun z ↦ (z - g x) ^ r • f z) (g x)
hg' : ¬analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : ↑n = analyticOrderAt (fun x_1 ↦ g x_1 - g x) x
⊢ MeromorphicAt (f ∘ g) x

Tactic:
obtain ⟨h, han, hne, heq⟩ := (hg.fun_sub analyticAt_const).analyticOrderAt_eq_natCast.mp hn.symm

Goal state after:
case neg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : 𝕜
f : 𝕜' → F
g : 𝕜 → 𝕜'
hg : AnalyticAt 𝕜 g x
r : ℕ
hr : AnalyticAt 𝕜' (fun z ↦ (z - g x) ^ r • f z) (g x)
hg' : ¬analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
n : ℕ
hn : ↑n = analyticOrderAt (fun x_1 ↦ g x_1 - g x) x
h : 𝕜 → 𝕜'
han : AnalyticAt 𝕜 h x
hne : h x ≠ 0
heq : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ n • h z
⊢ MeromorphicAt (f ∘ g) x
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
⊢ MeromorphicAt f (g x) → MeromorphicAt (f ∘ g) x

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicAt (f ∘ fun x ↦ x + c) (x + c - c)
⊢ AnalyticAt 𝕜 (fun z ↦ z - c) (x + c)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicAt f (x + c)
⊢ AnalyticAt 𝕜 (fun z ↦ z + c) x

Tactic:
by fun_prop

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

Goal state before:
pp: case convert_7
a : ℂ
this : binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
⊢ AnalyticOn ℂ (fun x ↦ (1 + x) ^ a) (Metric.eball 0 1)

pp: case convert_8
a : ℂ
this : binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
⊢ 1 ≤ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !).radius

Tactic:
· -- TODO: use `fun_prop` for this subgoal
      apply AnalyticOn.cpow (analyticOn_const.add analyticOn_id) analyticOn_const
      intro z hz
      apply Complex.mem_slitPlane_of_norm_lt_one
      rw [← ENNReal.ofReal_one, Metric.eball_ofReal] at hz
      simpa using hz

Goal state after:
case convert_8
a : ℂ
this : binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
⊢ 1 ≤ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !).radius
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ DifferentiableAt ℂ (HAdd.hAdd 1) z

Tactic:
by fun_prop

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

Goal state before:
pp: case h's
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ s ∩ Metric.eball x r ⊆ Metric.eball x r

Tactic:
· exact inter_subset_right

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

Goal state before:
pp: case h's
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ s ∩ Metric.eball x r ⊆ Metric.eball x r

Tactic:
· exact inter_subset_right

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDeriv 𝕜 n f x) (v ∘ ⇑σ) = (iteratedFDeriv 𝕜 n f x) v

Tactic:
← iteratedFDerivWithin_univ

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
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDerivWithin 𝕜 n f univ x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f univ x) v
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
σ : Perm (Fin n)
⊢ ContinuousMultilinearMap.domDomCongr σ (iteratedFDeriv 𝕜 n f x) = iteratedFDeriv 𝕜 n f x

Tactic:
← iteratedFDerivWithin_univ

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
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
σ : Perm (Fin n)
⊢ ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f univ x) = iteratedFDerivWithin 𝕜 n f univ x
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDeriv 𝕜 n f x) (v ∘ ⇑σ) = (iteratedFDeriv 𝕜 n f x) v

Tactic:
← iteratedFDerivWithin_univ

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
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDerivWithin 𝕜 n f univ x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f univ x) v
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
σ : Perm (Fin n)
⊢ ContinuousMultilinearMap.domDomCongr σ (iteratedFDeriv 𝕜 n f x) = iteratedFDeriv 𝕜 n f x

Tactic:
← iteratedFDerivWithin_univ

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
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
σ : Perm (Fin n)
⊢ ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f univ x) = iteratedFDerivWithin 𝕜 n f univ x
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
hK1 hK2 : 0 < 1
hA : AntilipschitzWith 1 ⇑(Equiv.refl X)
hL : LipschitzWith 1 ⇑(Equiv.refl X)
⊢ mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D = D

Tactic:
ext <;> simp only [mapBilipschitz, Equiv.refl_apply, Set.image_id', div_one, one_mul]

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

Goal state before:
pp: case inl
u v : ℕ → EReal
hb : ⊥ ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + ⊥
⊢ (linearGrowthSup fun x ↦ v x + ⊥) ≤ linearGrowthSup v

Tactic:
simp only [add_bot, ← Pi.bot_def, linearGrowthSup_bot, bot_le]

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

Goal state before:
pp: ⊢ linearGrowthSup (log ∘ 0) = linearGrowthSup ⊥

Tactic:
congr 1

Goal state after:
⊢ log ∘ 0 = ⊥
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: case inr
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun x ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
h't : t ∈ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
⊢ t ⊆ closedBall x δ

Tactic:
exact ht.trans (closedBall_subset_closedBall (min_le_right _ _))

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
⊢ ⨍ (x : α), f x ∂μ = (μ.real univ)⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
average_eq',

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
⊢ ∫ (x : α), f x ∂(μ univ)⁻¹ • μ = (μ.real univ)⁻¹ • ∫ (x : α), f x ∂μ
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
x : α
⊢ Continuous (HMul.hMul 20)

Tactic:
by fun_prop

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    (μ.real s / (μ.real s + μ.real t)) • ⨍ (x : α) in s, f x ∂μ +
      (μ.real t / (μ.real s + μ.real t)) • ⨍ (x : α) in t, f x ∂μ

Tactic:
by
  have := Fact.mk hsμ.lt_top; have := Fact.mk htμ.lt_top
  rw [restrict_union₀ hd ht, average_add_measure hfs hft, measureReal_restrict_apply_univ,
    measureReal_restrict_apply_univ]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
u : Set α
hu : MeasurableSet u
huμ : (μ.restrict (s ∪ t)) u < ∞
⊢ ∫⁻ (x : α) in u, f x ∂μ.restrict (s ∪ t) = ∫⁻ (x : α) in u, g x ∂μ.restrict (s ∪ t)

Tactic:
rw [Measure.restrict_restrict hu]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
u : Set α
hu : MeasurableSet u
huμ : (μ.restrict (s ∪ t)) u < ∞
⊢ ∫⁻ (x : α) in u ∩ (s ∪ t), f x ∂μ = ∫⁻ (x : α) in u ∩ (s ∪ t), g x ∂μ