mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case refine_1
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 t) volume
I : 0 < min 1 t
⊢ False

Tactic:
have H' : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 (min 1 t)) :=
    H.mono (Set.Ioo_subset_Ioo le_rfl (min_le_right _ _)) le_rfl

Goal state after:
case refine_1
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
⊢ False
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
⊢ Real.circleAverage (fun z ↦ (z / (z - w) - q • z / (q • z - W)) • f z) 0 R =
    Real.circleAverage (fun z ↦ (z / (z - w)) • f z) 0 R - Real.circleAverage (fun z ↦ (q • z / (q • z - W)) • f z) 0 R

Tactic:
[

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
⊢ Real.circleAverage (fun z ↦ (z / (z - w) - q • z / (q • z - W)) • f z) 0 R =
    Real.circleAverage (fun z ↦ (z / (z - w)) • f z) 0 R - Real.circleAverage (fun z ↦ (q • z / (q • z - W)) • f z) 0 R
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
⊢ Real.circleAverage (fun z ↦ (z / (z - w) - q • z / (q • z - W)) • f z) 0 R =
    Real.circleAverage (fun z ↦ (z / (z - w)) • f z) 0 R - Real.circleAverage (fun z ↦ (q • z / (q • z - W)) • f z) 0 R

Tactic:
by
      simp_rw [sub_smul]
      have h₁ : ∀ z ∈ sphere 0 R, z - w ≠ 0 := by aesop (add simp sub_eq_zero)
      have h₃ : ContinuousOn f (sphere 0 R) :=
        hf.2.mono <| sphere_subset_closedBall.trans_eq (closure_ball 0 hR.ne').symm
      rw [circleAverage_fun_sub]
      all_goals
        apply ContinuousOn.circleIntegrable hR.le
        fun_prop (disch := aesop)

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

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
hmax : ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x₀‖
h : ‖f ↑x₀‖ ≤ C
⊢ ∀ {z : ℂ}, 0 ≤ z.re → ‖f z‖ ≤ C

Tactic:
simpa only [max_eq_left h] using hle _ hmax

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
⊢ Real.circleAverage (poissonKernel c w • f) c R = f w

Tactic:
[

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
⊢ Real.circleAverage (poissonKernel c w • f) c R = f w
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case inr
a b : ℝ
r : ℂ
h : -1 < r.re
this✝ : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x ↦ Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Ioc 0 (-c)) volume
x : ℝ
hx : x ∈ Ioc 0 (-c)
this : -x ≤ 0
⊢ Complex.exp (↑π * Complex.I * r) * ↑x ^ r = ↑(-x) ^ r

Tactic:
Complex.ofReal_cpow_of_nonpos this,

Goal state after:
case inr
a b : ℝ
r : ℂ
h : -1 < r.re
this✝ : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x ↦ Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Ioc 0 (-c)) volume
x : ℝ
hx : x ∈ Ioc 0 (-c)
this : -x ≤ 0
⊢ Complex.exp (↑π * Complex.I * r) * ↑x ^ r = (-↑(-x)) ^ r * Complex.exp (↑π * Complex.I * r)
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (∑ t ∈ s, |f t|) ≤ log⁺ (∑ t ∈ s, |f t_max|)

Tactic:
apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp [mul_nonneg])
    apply Finset.sum_le_sum (fun i ih ↦ ht_max.2 i ih)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: case e'_3
x y : ℝ
⊢ log⁺ (x + y) = log⁺ (∑ t, ![x, y] t)

Tactic:
simp [add_assoc]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: case e'_4
x y : ℝ
⊢ log 2 + log⁺ x + log⁺ y = log ↑Finset.univ.card + ∑ t, log⁺ (![x, y] t)

Tactic:
simp [add_assoc]

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

Goal state before:
pp: case e'_2
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ∫ (x : ℝ) in a..b, x ^ r = (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re

Tactic:
[

Goal state after:
case e'_2
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ∫ (x : ℝ) in a..b, x ^ r = (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

Goal state before:
pp: | (∫ (x : ℝ) in 0..π / 2, log (sin x)) + ∫ (x : ℝ) in π / 2..π, log (sin x) = 2 * ∫ (x : ℝ) in 0..π / 2, log (sin x)

Tactic:
left; right; arg 1
    intro x
    rw [← sin_pi_sub]

Goal state after:
x : ℝ
| log (sin (π - x))
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case e'_3
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = ((↑b ^ ↑(r + 1) - ↑a ^ ↑(r + 1)) / ↑(r + 1)).re

Tactic:
[

Goal state after:
case e'_3
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = ((↑b ^ ↑(r + 1) - ↑a ^ ↑(r + 1)) / ↑(r + 1)).re
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z ↦ cexp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ Tendsto (fun x ↦ g ↑x) atTop (𝓝 0)

Tactic:
[

Goal state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z ↦ cexp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ Tendsto (fun x ↦ g ↑x) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (fun x ↦ log⁺ ‖f x‖) volume a b

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (fun x ↦ log⁺ ‖f x‖) volume a b
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: r : ℝ
⊢ ∫ (t : ℝ) in -r..r, Complex.exp (↑t * Complex.I) =
    (Complex.exp (Complex.I * ↑r) - Complex.exp (Complex.I * -↑r)) / Complex.I

Tactic:
[

Goal state after:
r : ℝ
⊢ ∫ (t : ℝ) in -r..r, Complex.exp (↑t * Complex.I) =
    (Complex.exp (Complex.I * ↑r) - Complex.exp (Complex.I * -↑r)) / Complex.I
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case inl
b : ℝ
h : b < 0
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
conv => arg 1; arg 1; intro t; rw [← log_neg_eq_log]

Goal state after:
case inl
b : ℝ
h : b < 0
⊢ ∫ (t : ℝ) in 0..b, log (-t) = b * log b - b
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
ha : 1 < a
hb : 1 < b
this : ∫ (t : ℝ) in a..b, deriv (fun t ↦ (log t)⁻¹) t = (log b)⁻¹ - (log a)⁻¹
⊢ ∫ (t : ℝ) in a..b, t⁻¹ / log t ^ 2 = (log a)⁻¹ - (log b)⁻¹

Tactic:
[

Goal state after:
a b : ℝ
ha : 1 < a
hb : 1 < b
this : ∫ (t : ℝ) in a..b, deriv (fun t ↦ (log t)⁻¹) t = (log b)⁻¹ - (log a)⁻¹
⊢ ∫ (t : ℝ) in a..b, t⁻¹ / log t ^ 2 = (log a)⁻¹ - (log b)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖) c R

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖) c R
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case e'_3
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ↑((1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))) =
    (1 + ↑b ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))

Tactic:
[

Goal state after:
case e'_3
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ↑((1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))) =
    (1 + ↑b ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
x : ℝ
x✝ : x ∈ [[a, b]]
⊢ HasDerivAt (-cos) (sin x) x

Tactic:
by
    simpa only [neg_neg] using! (hasDerivAt_cos x).neg

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * ↑π * I / ↑h)) z
diff_ne : q * (2 * ↑π * I / ↑h) ≠ 0
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * ↑π * I / ↑h)) z qdiff diff_ne
diff_L : DifferentiableAt ℂ L q
hL : 𝕢 h ∘ L =ᶠ[𝓝 q] id
hF : cuspFunction h f ∘ 𝕢 h ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id
this : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Tactic:
this

Goal state after:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * ↑π * I / ↑h)) z
diff_ne : q * (2 * ↑π * I / ↑h) ≠ 0
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * ↑π * I / ↑h)) z qdiff diff_ne
diff_L : DifferentiableAt ℂ L q
hL : 𝕢 h ∘ L =ᶠ[𝓝 q] id
hF : f ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id
this : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: case h
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).re = c₀
h₁U : IsOpen U
h₂U : IsConnected U
cc : ℂ
hcc : ∀ x ∈ U, f x = cc
⊢ ∀ x ∈ U, f x = ↑c₀ + ↑cc.im * I

Tactic:
[

Goal state after:
case h
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).re = c₀
h₁U : IsOpen U
h₂U : IsConnected U
cc : ℂ
hcc : ∀ x ∈ U, f x = cc
⊢ ∀ x ∈ U, f x = ↑c₀ + ↑cc.im * I
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: case h
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
cc : ℂ
hcc : ∀ x ∈ U, f x = cc
⊢ ∀ x ∈ U, f x = ↑cc.re + ↑c₀ * I

Tactic:
[

Goal state after:
case h
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
cc : ℂ
hcc : ∀ x ∈ U, f x = cc
⊢ ∀ x ∈ U, f x = ↑cc.re + ↑c₀ * I
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case refine_3
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)

pp: case refine_1
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
⊢ IntervalIntegrable (fun x ↦ -↑(n + 1) * sin x * cos x ^ n) MeasureTheory.volume a b

pp: case refine_2
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
⊢ IntervalIntegrable cos MeasureTheory.volume a b

Tactic:
· calc
      (∫ x in a..b, cos x ^ (n + 2)) = ∫ x in a..b, cos x ^ (n + 1) * cos x := by
        simp only [_root_.pow_succ]
      _ = C + (n + 1) * ∫ x in a..b, sin x ^ 2 * cos x ^ n := by simp [C, H, h, sq, -neg_add_rev]
      _ = C + (n + 1) * ∫ x in a..b, cos x ^ n - cos x ^ (n + 2) := by
        simp [sin_sq, sub_mul, ← pow_add, add_comm]
      _ = (C + (n + 1) * ∫ x in a..b, cos x ^ n) - (n + 1) * ∫ x in a..b, cos x ^ (n + 2) := by
        rw [integral_sub, mul_sub, add_sub_assoc] <;>
          apply Continuous.intervalIntegrable <;> fun_prop

Goal state after:
case refine_1
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
⊢ IntervalIntegrable (fun x ↦ -↑(n + 1) * sin x * cos x ^ n) MeasureTheory.volume a b

case refine_2
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
⊢ IntervalIntegrable cos MeasureTheory.volume a b
Module: Mathlib.Analysis.Complex.TaylorSeries

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (Metric.eball c r)
z : ℂ
hz : z ∈ Metric.eball c r
r' : NNReal
hzr' : edist c z < ↑r'
hr' : ↑r' < r
⊢ HasSum (fun n ↦ (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Tactic:
rw [← Metric.mem_eball', Metric.eball_coe] at hzr'

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (Metric.eball c r)
z : ℂ
hz : z ∈ Metric.eball c r
r' : NNReal
hzr' : z ∈ Metric.ball c ↑r'
hr' : ↑r' < r
⊢ HasSum (fun n ↦ (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
z : ℂ
| herglotzRieszKernel c w (z + c)

Tactic:
herglotzRieszKernel_add_const c w z

Goal state after:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
z : ℂ
| herglotzRieszKernel 0 (w - c) z
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
u : ℂ
hu : u ∈ h.toFinset
⊢ circleAverage (fun x ↦ ↑(D u) * log ‖x - u‖) c R = ↑(D u) * log R

Tactic:
[

Goal state after:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
u : ℂ
hu : u ∈ h.toFinset
⊢ circleAverage (fun x ↦ ↑(D u) * log ‖x - u‖) c R = ↑(D u) * log R
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∑ᶠ (i : ℂ), (↑((divisor f CB) i) * log R - ↑((divisor f CB) i) * log ‖c - i‖) + log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * (log R - log ‖c - u‖) + log ‖meromorphicTrailingCoeffAt f c‖

Tactic:
[

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∑ᶠ (i : ℂ), (↑((divisor f CB) i) * log R - ↑((divisor f CB) i) * log ‖c - i‖) + log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * (log R - log ‖c - u‖) + log ‖meromorphicTrailingCoeffAt f c‖
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : im I = 1
⊢ (complexRingEquiv h).symm ((complexRingEquiv h) I).sqrt = ↑√2⁻¹ * (1 - I) * I

Tactic:
[

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : im I = 1
⊢ (complexRingEquiv h).symm ((complexRingEquiv h) I).sqrt = ↑√2⁻¹ * (1 - I) * I
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : im I = 1
⊢ (complexRingEquiv h).symm ((complexRingEquiv h) (-I)).sqrt = ↑√2⁻¹ * (1 + I) * -I

Tactic:
[

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : im I = 1
⊢ (complexRingEquiv h).symm ((complexRingEquiv h) (-I)).sqrt = ↑√2⁻¹ * (1 + I) * -I
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

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

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ (↑g * m * (↑g)⁻¹).IsParabolic ↔ m.IsParabolic
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case h.«0»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
j : Fin 2
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨0, ⋯⟩) j = m ((fun i ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case h.«0».«0»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = m ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case h.«0».«1»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = m ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case h.«1»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
j : Fin 2
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨1, ⋯⟩) j = m ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case h.«1».«0»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = m ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case h.«1».«1»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = m ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case inl.inr
g g' : GL (Fin 2) ℝ
z : ℂ
h : (↑g).det < 0
h' : 0 < (↑g').det
⊢ (if 0 < ↑(GeneralLinearGroup.det g) * ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ
      else Complex.conjCAE)
      z =
    (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
      ((if 0 < ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z)

pp: case inr.inl
g g' : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g).det
h' : (↑g').det < 0
⊢ (if 0 < ↑(GeneralLinearGroup.det g) * ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ
      else Complex.conjCAE)
      z =
    (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
      ((if 0 < ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z)

pp: case inr.inr
g g' : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g).det
h' : 0 < (↑g').det
⊢ (if 0 < ↑(GeneralLinearGroup.det g) * ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ
      else Complex.conjCAE)
      z =
    (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
      ((if 0 < ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z)

Tactic:
· simp [(mul_neg_of_neg_of_pos h h').not_gt, h.not_gt, h']

Goal state after:
case inr.inl
g g' : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g).det
h' : (↑g').det < 0
⊢ (if 0 < ↑(GeneralLinearGroup.det g) * ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ
      else Complex.conjCAE)
      z =
    (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
      ((if 0 < ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z)

case inr.inr
g g' : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g).det
h' : 0 < (↑g').det
⊢ (if 0 < ↑(GeneralLinearGroup.det g) * ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ
      else Complex.conjCAE)
      z =
    (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
      ((if 0 < ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z)