mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
⊢ ∑ i, (∑ m, ⟪w m, v i⟫_ℝ • w m) ⊗ₜ[ℝ] ∑ n, ⟪w n, v i⟫_ℝ • w n = ∑ i, v i ⊗ₜ[ℝ] v i

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
⊢ canonicalCovariantTensor E = ∑ i, v i ⊗ₜ[ℝ] v i

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ ↑z.re + ↑y * I ∈ closedBall c r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: l u : ℝ
hul : l < u
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
⊢ ↑l + z * (↑u - ↑l) ∈ verticalClosedStrip l u

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c : ℂ
r a₁ a₂ b : ℝ
ha₁ : ↑a₁ + ↑b * I ∈ ball c r
ha₂ : ↑a₂ + ↑b * I ∈ ball c r
⊢ (fun x ↦ ↑x + ↑b * I) '' [[a₁, a₂]] ⊆ ball c r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
⊢ BddAbove (norm ∘ scale f l u '' verticalClosedStrip 0 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
w : ℂ
hw : w.im ∈ Icc (a - b) (a + b)
⊢ |(aff w).im| ≤ d * b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
z : ℂ
hz : z.re = 0
⊢ ↑l + z * (↑u - ↑l) ∈ re ⁻¹' {l}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
⊢ ∀ z ∈ re ⁻¹' {0}, ‖scale f l u z‖ ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c : ℂ
r a b₁ b₂ : ℝ
hb₁ : ↑a + ↑b₁ * I ∈ ball c r
hb₂ : ↑a + ↑b₂ * I ∈ ball c r
⊢ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]] ⊆ ball c r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ r - dist z c + dist z c ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
z : ℂ
hz : z.re = 1
⊢ ↑l + z * (↑u - ↑l) ∈ re ⁻¹' {u}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
⊢ ∃ δ < 0, ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
⊢ ∀ z ∈ re ⁻¹' {1}, ‖scale f l u z‖ ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ (fun y ↦ ↑w.re + ↑y * I) '' [[z.im, w.im]] ⊆ ball c r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
f : ℂ → E
⊢ z.wedgeIntegral w f + w.wedgeIntegral z f =
    (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
x₀ : ℂ
y : E
η : ℂ → E
hη : ∀ z ∈ s, HasDerivAt η (f z) z
⊢ η x₀ - η x₀ + y = y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
x₀ : ℂ
y : E
η : ℂ → E
hη : ∀ z ∈ s, HasDerivAt η (f z) z
⊢ ∀ x ∈ s, HasDerivAt (fun z ↦ η z - η x₀ + y) (f x) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
h : IsExactOn f s
x₀ : ℂ
y : E
⊢ ∃ g, g x₀ = y ∧ ∀ x ∈ s, HasDerivAt g (f x) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
U : Set ℂ
hf : DifferentiableOn ℂ f U
⊢ IsConservativeOn f U

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
⊢ ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ↑u - ↑l ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
hf : IsExactOn f U
⊢ DifferentiableOn ℂ f U

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
⊢ r - dist z c > 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ scale f l u '' re ⁻¹' {0} = f '' re ⁻¹' {l}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ sSupNormIm (scale f l u) 0 = sSupNormIm f l

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ ↑u - ↑l ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ scale f l u '' re ⁻¹' {1} = f '' re ⁻¹' {u}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ sSupNormIm (scale f l u) 1 = sSupNormIm f u

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
z : ℂ
⊢ interpStrip (scale f l u) ((z - ↑l) / (↑u - ↑l)) = interpStrip' f l u z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f (↑x + ↑c.im * I)
I₂ : E := I • ∫ (y : ℝ) in c.im..w.im, f (↑w.re + ↑y * I)
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f (↑x + ↑c.im * I)
I₄ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑z.re + ↑y * I)
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₆ : E := I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑c.im * I)
I₈ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑w.re + ↑y * I)
⊢ r - dist z c + dist z c ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ ≤ ‖(↑ε + ↑(sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(sSupNormIm f 1)) ^ z‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ (fun x ↦ ‖f z‖) ≤ᶠ[𝓝[>] 0] fun ε ↦ ‖(↑ε + ↑(sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(sSupNormIm f 1)) ^ z‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f (↑x + ↑c.im * I)
I₂ : E := I • ∫ (y : ℝ) in c.im..w.im, f (↑w.re + ↑y * I)
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f (↑x + ↑c.im * I)
I₄ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑z.re + ↑y * I)
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₆ : E := I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑c.im * I)
I₈ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑w.re + ↑y * I)
z_ball : ball z (r - dist z c) ⊆ ball c r
w_mem : w ∈ ball c r
a₁ a₂ b : ℝ
ha₁ : ↑a₁ + ↑b * I ∈ ball c r
ha₂ : ↑a₂ + ↑b * I ∈ ball c r
⊢ ContinuousOn (fun x ↦ ↑x + ↑b * I) [[a₁, a₂]]

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
⊢ init m 0 = m 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init m 0 = m 0
⊢ tail m (last n) = m (last n.succ)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init m 0 = m 0
hmtail : tail m (last n) = m (last n.succ)
⊢ ∂_{m 0} (∂^{tail m} f) = ∂_{m 0} (∂^{init (tail m)} (∂_{tail m (last n)} f))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f (↑x + ↑c.im * I)
I₂ : E := I • ∫ (y : ℝ) in c.im..w.im, f (↑w.re + ↑y * I)
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f (↑x + ↑c.im * I)
I₄ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑z.re + ↑y * I)
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₆ : E := I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑c.im * I)
I₈ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑w.re + ↑y * I)
z_ball : ball z (r - dist z c) ⊆ ball c r
w_mem : w ∈ ball c r
integrableHoriz :
  ∀ (a₁ a₂ b : ℝ),
    ↑a₁ + ↑b * I ∈ ball c r → ↑a₂ + ↑b * I ∈ ball c r → IntervalIntegrable (fun x ↦ f (↑x + ↑b * I)) volume a₁ a₂
a b₁ b₂ : ℝ
hb₁ : ↑a + ↑b₁ * I ∈ ball c r
hb₂ : ↑a + ↑b₂ * I ∈ ball c r
⊢ ContinuousOn (fun y ↦ ↑a + ↑y * I) [[b₁, b₂]]

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init m 0 = m 0
hmtail : tail m (last n) = m (last n.succ)
⊢ ∂_{m 0} (∂^{init (tail m)} (∂_{tail m (last n)} f)) = ∂^{init m} (∂_{m (last (n + 1))} f)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
n : ℕ
m : Fin (n + 1) → V
f : E
⊢ ∂^{m} f = ∂^{init m} (∂_{m (last n)} f)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
n : ℕ
y : V
f : E
⊢ ∂^{fun x ↦ y} f = ∂_{y}^[n] f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_5
E : Type u_6
inst✝³ : LineDeriv V E E
n : ℕ
m : Fin n → V
inst✝² : AddCommGroup V
inst✝¹ : AddCommGroup E
inst✝ : LineDerivAdd V E E
x y : E
⊢ ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
A : ℝ
hA₀ : A > 0
hA :
  ∀ᶠ (b_1 : ℝ) in atTop,
    ∀ (a_1 : ℂ), |a_1.re| = b_1 → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
this : Tendsto (fun R ↦ expR (δ * expR (d * R) + B * expR (c * R) + Real.log A)) atTop (𝓝 0)
⊢ ∀ᶠ (R : ℝ) in atTop, ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: R : Type u_4
V : Type u_5
E : Type u_6
inst✝² : LineDeriv V E E
n : ℕ
m : Fin n → V
inst✝¹ : SMul R E
inst✝ : LineDerivSMul R V E E
r : R
x : E
⊢ ∂^{m} (r • x) = r • ∂^{m} x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_5
E : Type u_6
inst✝² : LineDeriv V E E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousLineDeriv V E E
n : ℕ
m : Fin n → V
⊢ Continuous ∂^{m}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
R : Type u_4
V : Type u_5
E : Type u_6
F : Type u_7
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst✝¹⁴ : LineDeriv E V₁ V₂
inst✝¹³ : LineDeriv E V₂ V₃
inst✝¹² : AddCommGroup V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : AddCommGroup V₃
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
inst✝⁶ : Module R V₂
inst✝⁵ : Module R V₃
inst✝⁴ : LineDerivAdd E V₂ V₃
inst✝³ : LineDerivAdd E V₁ V₂
inst✝² : LineDerivSMul R E V₂ V₃
inst✝¹ : LineDerivLeftSMul R E V₁ V₂
inst✝ : LineDerivLeftSMul R E V₂ V₃
f : V₁
⊢ ∀ (m₁ m₂ n : E), ∂_{m₁ + m₂} (∂_{n} f) = ∂_{m₁} (∂_{n} f) + ∂_{m₂} (∂_{n} f)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
R : Type u_4
V : Type u_5
E : Type u_6
F : Type u_7
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst✝¹⁴ : LineDeriv E V₁ V₂
inst✝¹³ : LineDeriv E V₂ V₃
inst✝¹² : AddCommGroup V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : AddCommGroup V₃
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
inst✝⁶ : Module R V₂
inst✝⁵ : Module R V₃
inst✝⁴ : LineDerivAdd E V₂ V₃
inst✝³ : LineDerivAdd E V₁ V₂
inst✝² : LineDerivSMul R E V₂ V₃
inst✝¹ : LineDerivLeftSMul R E V₁ V₂
inst✝ : LineDerivLeftSMul R E V₂ V₃
f : V₁
⊢ ∀ (c : R) (m n : E), ∂_{c • m} (∂_{n} f) = c • ∂_{m} (∂_{n} f)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
R : Type u_4
V : Type u_5
E : Type u_6
F : Type u_7
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst✝¹⁴ : LineDeriv E V₁ V₂
inst✝¹³ : LineDeriv E V₂ V₃
inst✝¹² : AddCommGroup V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : AddCommGroup V₃
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
inst✝⁶ : Module R V₂
inst✝⁵ : Module R V₃
inst✝⁴ : LineDerivAdd E V₂ V₃
inst✝³ : LineDerivAdd E V₁ V₂
inst✝² : LineDerivSMul R E V₂ V₃
inst✝¹ : LineDerivLeftSMul R E V₁ V₂
inst✝ : LineDerivLeftSMul R E V₂ V₃
f : V₁
⊢ ∀ (m n₁ n₂ : E), ∂_{m} (∂_{n₁ + n₂} f) = ∂_{m} (∂_{n₁} f) + ∂_{m} (∂_{n₂} f)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
R : Type u_4
V : Type u_5
E : Type u_6
F : Type u_7
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst✝¹⁴ : LineDeriv E V₁ V₂
inst✝¹³ : LineDeriv E V₂ V₃
inst✝¹² : AddCommGroup V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : AddCommGroup V₃
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
inst✝⁶ : Module R V₂
inst✝⁵ : Module R V₃
inst✝⁴ : LineDerivAdd E V₂ V₃
inst✝³ : LineDerivAdd E V₁ V₂
inst✝² : LineDerivSMul R E V₂ V₃
inst✝¹ : LineDerivLeftSMul R E V₁ V₂
inst✝ : LineDerivLeftSMul R E V₂ V₃
f : V₁
⊢ ∀ (c : R) (m n : E), ∂_{m} (∂_{c • n} f) = c • ∂_{m} (∂_{n} f)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: ι : Type u_1
E : Type u_6
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst✝¹⁵ : LineDeriv E V₁ V₂
inst✝¹⁴ : LineDeriv E V₂ V₃
inst✝¹³ : AddCommGroup V₁
inst✝¹² : AddCommGroup V₂
inst✝¹¹ : AddCommGroup V₃
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : Module ℝ V₂
inst✝⁶ : Module ℝ V₃
inst✝⁵ : LineDerivAdd E V₁ V₂
inst✝⁴ : LineDerivAdd E V₂ V₃
inst✝³ : LineDerivSMul ℝ E V₂ V₃
inst✝² : LineDerivLeftSMul ℝ E V₁ V₂
inst✝¹ : LineDerivLeftSMul ℝ E V₂ V₃
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
f : V₁
⊢ (tensorLineDerivTwo ℝ f) (canonicalCovariantTensor E) = ∑ i, ∂_{v i} (∂_{v i} f)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: ι : Type u_1
E : Type u_6
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst✝²³ : LineDeriv E V₁ V₂
inst✝²² : LineDeriv E V₂ V₃
inst✝²¹ : AddCommGroup V₁
inst✝²⁰ : AddCommGroup V₂
inst✝¹⁹ : AddCommGroup V₃
inst✝¹⁸ : NormedAddCommGroup E
inst✝¹⁷ : InnerProductSpace ℝ E
inst✝¹⁶ : FiniteDimensional ℝ E
inst✝¹⁵ : Module ℝ V₁
inst✝¹⁴ : Module ℝ V₂
inst✝¹³ : Module ℝ V₃
inst✝¹² : TopologicalSpace V₁
inst✝¹¹ : TopologicalSpace V₂
inst✝¹⁰ : TopologicalSpace V₃
inst✝⁹ : IsTopologicalAddGroup V₃
inst✝⁸ : LineDerivAdd E V₁ V₂
inst✝⁷ : LineDerivSMul ℝ E V₁ V₂
inst✝⁶ : ContinuousLineDeriv E V₁ V₂
inst✝⁵ : LineDerivAdd E V₂ V₃
inst✝⁴ : LineDerivSMul ℝ E V₂ V₃
inst✝³ : ContinuousLineDeriv E V₂ V₃
inst✝² : LineDerivLeftSMul ℝ E V₁ V₂
inst✝¹ : LineDerivLeftSMul ℝ E V₂ V₃
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
f : V₁
⊢ (laplacianCLM ℝ E V₁) f = ∑ i, ∂_{v i} (∂_{v i} f)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ ∀ x ∈ Ioi 0,
    (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
      ‖↑(x + sSupNormIm f 0) ^ (1 - z) * ↑(x + sSupNormIm f 1) ^ z‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
A : ℝ
hA₀ : A > 0
hA :
  ∀ᶠ (b_1 : ℝ) in atTop,
    ∀ (a_1 : ℂ), |a_1.re| = b_1 → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
H : Tendsto (fun R ↦ δ + B * (expR ((d - c) * R))⁻¹) atTop (𝓝 (δ + B * 0))
⊢ Tendsto (fun R ↦ δ * expR (d * R) + B * expR (c * R) + Real.log A) atTop atBot

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ ‖f z‖ ≤ ‖interpStrip f z‖

Tactic:
by

Goal state after: