mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
x : ℂ
hx : x ∈ η₀.toFinset
⊢ x ∈ ball 0 R

Tactic:
by_contra

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
x : ℂ
hx : x ∈ η₀.toFinset
this : x ∉ ball 0 R
⊢ False
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
z : ℂ
hR : 0 < R
⊢ meromorphicOrderAt (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) z ≠ ⊤

Tactic:
by
  apply meromorphicOrderAt_finprod_ne_top
    (fun _ ↦ MeromorphicAt.zpow (meromorphic_canonicalFactor _ _ _) _)
  intro c
  rw [meromorphicOrderAt_zpow (meromorphic_canonicalFactor R c z)]
  lift meromorphicOrderAt (canonicalFactor R c) z to ℤ using
    (meromorphicOrderAt_canonicalFactor_ne_top c hR) with ℓ
  simp [← WithTop.coe_mul]

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

Goal state before:
pp: case right
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ (f I).im = I.im ∨ (f I).im = -I.im

Tactic:
apply @LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re f.toLinearIsometry

Goal state after:
case right
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ ∀ (z : ℂ), (f.toLinearIsometry z).re = z.re
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: a : Circle
i j : Fin 2
⊢ ![(↑a).re * (![1, I] j).re - (↑a).im * (![1, I] j).im, (↑a).re * (![1, I] j).im + (↑a).im * (![1, I] j).re] i =
    Matrix.vecCons (![(↑a).re, -(↑a).im] j) (fun i ↦ ![(↑a).im, (↑a).re] j) i

Tactic:
fin_cases i <;> fin_cases j <;> simp

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
g : ℂ → E
D : CanonicalDecomp f g R
⊢ 0 ∈ closedBall 0 R

Tactic:
simp [hR.le]

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hf' : ∃ g_1, AnalyticAt 𝕜 g_1 (g x) ∧ g_1 (g x) ≠ 0 ∧ f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ r • g_1 z
hr : meromorphicOrderAt f (g x) = ↑r
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x)

Tactic:
hr

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
hf' : ∃ g_1, AnalyticAt 𝕜 g_1 (g x) ∧ g_1 (g x) ≠ 0 ∧ f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ r • g_1 z
hr : meromorphicOrderAt f (g x) = ↑r
⊢ meromorphicOrderAt (f ∘ g) x = ↑r * ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x)
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
η₀ : ∀ x ∈ t₁, ‖w - x‖ ^ (-divisor f S₀R) x ≠ 0
x : ℂ
hx : x ∈ t₂
⊢ ‖canonicalFactor R x w‖ ≠ 0

Tactic:
rw [norm_ne_zero_iff]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
η₀ : ∀ x ∈ t₁, ‖w - x‖ ^ (-divisor f S₀R) x ≠ 0
x : ℂ
hx : x ∈ t₂
⊢ canonicalFactor R x w ≠ 0
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
this :
  ∀ 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‖
⊢ Tendsto (fun x ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 (‖↑(sSupNormIm f 0) ^ (1 - z)‖ * ‖↑(sSupNormIm f 1) ^ z‖))

Tactic:
norm_cpow_eq_rpow_re_of_nonneg (sSupNormIm_nonneg _ _) _,

Goal state after:
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
this :
  ∀ 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‖
⊢ Tendsto (fun x ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 (sSupNormIm f 0 ^ (1 - z).re * ‖↑(sSupNormIm f 1) ^ z‖))

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
this :
  ∀ 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‖
⊢ (1 - z).re ≠ 0
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ 0 ≤ sSupNormIm f 0

Tactic:
exact sSupNormIm_nonneg f _

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
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
this : (fun w ↦ ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) - f z) =o[𝓝 z] fun w ↦ w - z
⊢ (fun w ↦ (∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) - (w - z).im • f z) =o[𝓝 z] fun w ↦ w - z

Tactic:
calc
      _ = fun w ↦ (∫ y in z.im..w.im, f (w.re + y * I)) - (∫ _ in z.im..w.im, f z) := by simp
      _ =ᶠ[𝓝 z] fun w ↦ ∫ y in z.im..w.im, f (w.re + y * I) - f z := ?_
      _ =o[𝓝 z] fun w ↦ w - z := this
    refine eventually_nhds_iff_ball.mpr ⟨r - dist z c, by simpa using hz, fun w hw ↦ ?_⟩
    exact (intervalIntegral.integral_sub
      ((f_cont.mono (mem_ball_of_map_im_aux₂ hw)).comp (by fun_prop)
        (mapsTo_image _ _)).intervalIntegrable intervalIntegrable_const).symm

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: case neg
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
hR : ¬R = 0
H : ContinuousOn (circleAverage (⇑g ∘ f) c) (Set.Ioc 0 |R|)
r : ℝ
⊢ r ∈ Set.Ioo 0 |R| → circleAverage (⇑g ∘ f) c r = (fun x ↦ g (f c)) r

Tactic:
hr

Goal state after:
case neg
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
hR : ¬R = 0
H : ContinuousOn (circleAverage (⇑g ∘ f) c) (Set.Ioc 0 |R|)
r : ℝ
hr : r ∈ Set.Ioo 0 |R|
⊢ circleAverage (⇑g ∘ f) c r = (fun x ↦ g (f c)) r
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ circleAverage (f₁ - f₂) c R = circleAverage f₁ c R - circleAverage f₂ c R

Tactic:
by
  rw [circleAverage, circleAverage, circleAverage, ← smul_sub]
  congr
  apply intervalIntegral.integral_sub hf₁ hf₂

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: case h₂f
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
r : ℝ
⊢ r ∈ Set.Ioo ‖w - c‖ R → circleAverage (re ∘ herglotzRieszKernel c w • f) c r = (fun x ↦ f w) r

Tactic:
hr

Goal state after:
case h₂f
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
r : ℝ
hr : r ∈ Set.Ioo ‖w - c‖ R
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c r = (fun x ↦ f w) r
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 t) volume
I : 0 < min 1 t
H' : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 (min 1 t)) volume
x : ℝ
hx : x ∈ Ioo 0 (min 1 t)
⊢ x⁻¹ ≤ x ^ s

Tactic:
rwa [← Real.rpow_neg_one x, Real.rpow_le_rpow_left_iff_of_base_lt_one hx.1]

Goal state after:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 t) volume
I : 0 < min 1 t
H' : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 (min 1 t)) volume
x : ℝ
hx : x ∈ Ioo 0 (min 1 t)
⊢ x < 1
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hderiv.refine_2
a b : ℝ
r : ℂ
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hr : r = -1
⊢ r + 1 = 0

Tactic:
hr

Goal state after:
case hderiv.refine_2
a b : ℝ
r : ℂ
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hr : r = -1
⊢ -1 + 1 = 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
z : ℂ
hz : ‖z‖ = 1
this : z ≠ 0
⊢ ‖z⁻¹ * (z - a)‖ = ‖1 - z⁻¹ * a‖

Tactic:
field_simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b c : ℝ
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, (c ^ 2 + x ^ 2)⁻¹ = ∫ (x : ℝ) in a..b, (c ^ 2)⁻¹ * (1 + (x / c) ^ 2)⁻¹

Tactic:
field_simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b c : ℝ
hc : c ≠ 0
⊢ c * ((c ^ 2)⁻¹ * (arctan (b / c) - arctan (a / c))) = c⁻¹ * (arctan (b / c) - arctan (a / c))

Tactic:
field_simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case neg
a b c : ℝ
hc : ¬c = 0
⊢ c * (c⁻¹ * (arctan (b / c) - arctan (a / c))) = arctan (b / c) - arctan (a / c)

Tactic:
field_simp

Goal state after:
Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SeminormedRing β
l : Filter α
f g : α → β
hf : l.BoundedAtFilter f
hg : l.BoundedAtFilter g
⊢ l.BoundedAtFilter (f * g)

Tactic:
refine (hf.mul hg).trans ?_

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : SeminormedRing β
l : Filter α
f g : α → β
hf : l.BoundedAtFilter f
hg : l.BoundedAtFilter g
⊢ (fun x ↦ 1 x * 1 x) =O[l] 1
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, sin x ^ n

Tactic:
field_simp

Goal state after:
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * (↑n + 2) =
    sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ (sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π) / ↑(2 * k + 1 + 2) +
      ↑(2 * k + 1 + 1) / ↑(2 * k + 1 + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) =
    ↑(2 * k + 2) / ↑(2 * k + 3) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)

Tactic:
field_simp

Goal state after:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π +
      ↑(2 * k + 1 + 1) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) =
    ↑(2 * k + 1 + 1) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / ↑(2 * k + 2) +
      ↑(2 * k + 1) / ↑(2 * k + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    ↑(2 * k + 1) / ↑(2 * k + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)

Tactic:
field_simp

Goal state after:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π + ↑(2 * k + 1) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    ↑(2 * k + 1) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, cos x ^ n

Tactic:
field_simp

Goal state after:
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) * (↑n + 2) =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n
Module: Mathlib.Analysis.Complex.Positivity

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ f c ≤ f z

Tactic:
have h' (n : ℕ) : 0 ≤ iteratedDeriv n (f · - f c) c := by
    cases n with
    | zero => simp only [iteratedDeriv_zero, sub_self, le_refl]
    | succ n =>
      specialize h (n + 1) n.succ_ne_zero
      rw [iteratedDeriv_succ'] at h ⊢
      rwa [funext fun x ↦ deriv_sub_const (f := f) (x := x) (f c)]
  exact sub_nonneg.mp <| nonneg_of_iteratedDeriv_nonneg (hf.sub_const _) h' hz

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
m n : ℕ
⊢ ∫ (x : ℝ) in a..b, (1 - 2⁻¹ - cos (2 * x) / 2) ^ m * (2⁻¹ + cos (2 * x) / 2) ^ n =
    ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n

Tactic:
field_simp

Goal state after:
a b : ℝ
m n : ℕ
⊢ ∫ (x : ℝ) in a..b, ((2 - 1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n =
    ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case e'_3
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x ↦ cos (2 * x) ^ 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
h4 : ∀ (d : ℝ), 2 * (2 * d) = 4 * d
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ 1 * ((1 + cos (2 * x)) / 2) ^ 1

Tactic:
simp [h1, h2.intervalIntegrable, integral_comp_mul_left fun x => cos x ^ 2, h3, h4]

Goal state after:
case e'_3
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x ↦ cos (2 * x) ^ 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
h4 : ∀ (d : ℝ), 2 * (2 * d) = 4 * d
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    (b - a - 2⁻¹ * ((sin (4 * b) / 2 - sin (4 * a) / 2 + 2 * b - 2 * a) / 2)) / 4
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case hw
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
⊢ ‖w‖ + (R - ‖w‖) / (↑n + 2) < R

Tactic:
field_simp

Goal state after:
case hw
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
⊢ ‖w‖ * (↑n + 2) + (R - ‖w‖) < R * (↑n + 2)
Module: Mathlib.Analysis.Complex.SummableUniformlyOn

Goal state before:
pp: case refine_1
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
t : Finset ι
r : ℂ
⊢ r ∈ s → DifferentiableWithinAt ℂ (fun x2 ↦ ∑ i ∈ t, f i x2) s r

Tactic:
hr

Goal state after:
case refine_1
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
t : Finset ι
r : ℂ
hr : r ∈ s
⊢ DifferentiableWithinAt ℂ (fun x2 ↦ ∑ i ∈ t, f i x2) s r
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Preorder R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ (↑g * m * (↑g)⁻¹).IsHyperbolic ↔ m.IsHyperbolic

Tactic:
simp [IsHyperbolic]

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = (Complex.I * ↑√(-(↑g).discr)) ^ 2
h : ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0))
⊢ z.im ≤ 0

Tactic:
rw [← coe_im, h]

Goal state after:
g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = (Complex.I * ↑√(-(↑g).discr)) ^ 2
h : ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0))
⊢ ((-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0))).im ≤ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
⊢ |(↑(↑N * -n) +ᵥ z).re| ≤ ↑N

Tactic:
have h : (N * (-n : ℝ) +ᵥ z).re = -N * Int.floor (z.re / N) + z.re := by
    simp only [n, mul_neg, vadd_re, neg_mul]

Goal state after:
case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
h : (↑N * -↑n +ᵥ z).re = -↑N * ↑⌊z.re / ↑N⌋ + z.re
⊢ |(↑(↑N * -n) +ᵥ z).re| ≤ ↑N
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
hge : (atTop.limUnder g).compContinuous e = f
⊢ ‖atTop.limUnder g‖ ≤ ‖f‖

Tactic:
← dist_zero_left,

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
hge : (atTop.limUnder g).compContinuous e = f
⊢ dist 0 (atTop.limUnder g) ≤ ‖f‖
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mp
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
⊢ ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 ≠ 0 → (∃ x, x ≠ 0 ∧ g = upperRightHom x) ∨ ∃ x, x ≠ 0 ∧ g = -upperRightHom x

Tactic:
rintro ⟨hg00, hg01⟩

Goal state after:
case mp
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
⊢ (∃ x, x ≠ 0 ∧ g = upperRightHom x) ∨ ∃ x, x ≠ 0 ∧ g = -upperRightHom x
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑(det g) = ↑g 1 1 ^ 2
⊢ ↑g 1 1 ^ 2 = 1

Tactic:
simp only [Units.ext_iff, Units.val_one, Units.val_neg, this] at h_det

Goal state after:
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑(det g) = ↑g 1 1 ^ 2
h_det : ↑g 1 1 ^ 2 = 1 ∨ ↑g 1 1 ^ 2 = -1
⊢ ↑g 1 1 ^ 2 = 1
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝ : Infinite ιS
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

pp: case inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝ : Fintype ιS
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
· rw [Algebra.norm_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis bS),
      det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis (bS.smulTower bA))]

Goal state after:
case inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝ : Fintype ιS
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)