mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℝ
hx : 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:
repeat rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]

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
x : ℝ
hx : x ∈ Ioi 0
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * (x + sSupNormIm f 1) ^ z.re

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 : ℝ
hx : x ∈ Ioi 0
⊢ z.re ≠ 0

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 : ℝ
hx : x ∈ Ioi 0
⊢ (1 - z).re ≠ 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
x : ℝ
hx : x ∈ Ioi 0
⊢ (1 - z).re ≠ 0

Tactic:
· simpa [sub_eq_zero] using (ne_comm.mpr (ne_of_lt hz.2))

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
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

Tactic:
· simpa [sub_eq_zero] using (ne_comm.mpr (ne_of_lt hz.2))

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

Goal state before:
pp: z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l * (u - l) / normSq (↑u - ↑l) ≤ z.re * (u - l) / normSq (↑u - ↑l) ∧
    z.re * (u - l) / normSq (↑u - ↑l) ≤ 1 + l * (u - l) / normSq (↑u - ↑l)

Tactic:
norm_cast

Goal state after:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l * (u - l) / normSq ↑(u - l) ≤ z.re * (u - l) / normSq ↑(u - l) ∧
    z.re * (u - l) / normSq ↑(u - l) ≤ 1 + l * (u - l) / normSq ↑(u - l)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: l u : ℝ
hul : l < u
z : ℂ
⊢ ↑u - ↑l ≠ 0

Tactic:
norm_cast

Goal state after:
l u : ℝ
hul : l < u
z : ℂ
⊢ ¬u - l = 0
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: l u : ℝ
hul : l < u
z : ℂ
⊢ (z / (↑u - ↑l)).re - (↑l / (↑u - ↑l)).re = (z.re - l) / (u - l)

Tactic:
norm_cast

Goal state after:
l u : ℝ
hul : l < u
z : ℂ
⊢ (z / ↑(u - l)).re - l / (u - l) = (z.re - l) / (u - l)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: l u : ℝ
hul : l < u
z : ℂ
⊢ u - l ≠ 0

Tactic:
norm_cast

Goal state after:
l u : ℝ
hul : l < u
z : ℂ
⊢ ¬u - l = 0
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ HarmonicAt (f₁ - f₂) x

Tactic:
constructor
  · exact h₁.1.sub h₂.1
  · filter_upwards [h₁.1.laplacian_sub_nhds h₂.1, h₁.2, h₂.2]
    simp_all

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

Goal state before:
pp: case e_a
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ ↑(((fderiv ℝ (fderiv ℝ f) x) I) 1) = ↑(((fderiv ℝ (fderiv ℝ f) x) 1) I)

Tactic:
norm_cast

Goal state after:
case e_a
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ ((fderiv ℝ (fderiv ℝ f) x) I) 1 = ((fderiv ℝ (fderiv ℝ f) x) 1) I
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: x : ℂ
a : ℤ
⊢ (∃ n, ↑n = x + ↑a) ↔ ∃ n, ↑n = x

Tactic:
exact ⟨(Exists.elim · fun n hn ↦ ⟨n - a, by simp [hn]⟩),
    (Exists.elim · fun n hn ↦ ⟨n + a, by simp [hn]⟩)⟩

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

Goal state before:
pp: case neg.inr.refine_2.inr.right
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : ∀ x ∈ Ioo c 0, ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ μ (Ioo c 0) < ⊤

Tactic:
refine (measure_mono Set.Ioo_subset_Icc_self).trans_lt ?_

Goal state after:
case neg.inr.refine_2.inr.right
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
this : ∀ x ∈ Ioo c 0, ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖
⊢ μ (Icc c 0) < ⊤
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: 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₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
z : ℂ
hz : ‖z - ↑x₀‖ < x₀
⊢ z ∈ {z | 0 < z.re}

Tactic:
mem_ofPred_eq

Goal state after:
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₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
z : ℂ
hz : ‖z - ↑x₀‖ < x₀
⊢ 0 < z.re
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: case pos.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : ↑[[a, b]]), meromorphicOrderAt f ↑u ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : ↑[[a, b]]), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin [[a, b]]] (∏ᶠ (u : ℝ), (fun x ↦ x - u) ^ (divisor f [[a, b]]) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    (∑ᶠ (u : ℝ), fun x ↦ ↑((divisor f [[a, b]]) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
⊢ ∀ (i : ℝ), IntervalIntegrable (fun x ↦ ↑((divisor f [[a, b]]) i) * log ‖x - i‖) volume a b

Tactic:
intro i

Goal state after:
case pos.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : ↑[[a, b]]), meromorphicOrderAt f ↑u ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : ↑[[a, b]]), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin [[a, b]]] (∏ᶠ (u : ℝ), (fun x ↦ x - u) ^ (divisor f [[a, b]]) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    (∑ᶠ (u : ℝ), fun x ↦ ↑((divisor f [[a, b]]) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
i : ℝ
⊢ IntervalIntegrable (fun x ↦ ↑((divisor f [[a, b]]) i) * log ‖x - i‖) volume a b
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z✝ : ℂ
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‖
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : z ∈ {z | 0 < z.re}
⊢ expR (ε * z.re) * ‖f z‖ ≤ ‖f z‖

Tactic:
refine mul_le_of_le_one_left (norm_nonneg _) (Real.exp_le_one_iff.2 ?_)

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z✝ : ℂ
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‖
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : z ∈ {z | 0 < z.re}
⊢ ε * z.re ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: case pos.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : ↑(sphere c |R|)), meromorphicOrderAt f ↑u ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : ↑(sphere c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (sphere c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (sphere c |R|)) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    (∑ᶠ (u : ℂ), fun x ↦ ↑((divisor f (sphere c |R|)) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
⊢ ∀ (i : ℂ), CircleIntegrable (fun x ↦ ↑((divisor f (sphere c |R|)) i) * log ‖x - i‖) c R

Tactic:
intro i

Goal state after:
case pos.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : ↑(sphere c |R|)), meromorphicOrderAt f ↑u ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : ↑(sphere c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (sphere c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (sphere c |R|)) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    (∑ᶠ (u : ℂ), fun x ↦ ↑((divisor f (sphere c |R|)) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
i : ℂ
⊢ CircleIntegrable (fun x ↦ ↑((divisor f (sphere c |R|)) i) * log ‖x - i‖) c R
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case neg
r : ℝ
hr : ¬r = 0
⊢ 2 * ↑(sin r) = 2 * ↑r * ↑(sin r / r)

Tactic:
norm_cast

Goal state after:
case neg
r : ℝ
hr : ¬r = 0
⊢ 2 * sin r = 2 * r * (sin r / r)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hint
a✝ b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ 1 + ↑a ^ 2 ∈ slitPlane

Tactic:
norm_cast

Goal state after:
case hint
a✝ b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ ↑(1 + a ^ 2) ∈ slitPlane
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b t : ℝ
ht : t ≠ -1
⊢ ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s

Tactic:
intro x s

Goal state after:
a b t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s

Tactic:
norm_cast

Goal state after:
a b t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ ↑((1 + x ^ 2) ^ s) = ↑(1 + x ^ 2) ^ ↑s
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:
norm_cast

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 + 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)
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:
norm_cast

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 + 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)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case inl.refine_1
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * ↑n + 1

Tactic:
norm_cast

Goal state after:
case inl.refine_1
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 1
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case inl.refine_2
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * ↑n + 2

Tactic:
norm_cast

Goal state after:
case inl.refine_2
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 2
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case inr.refine_1
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * ↑n + 2

Tactic:
norm_cast

Goal state after:
case inr.refine_1
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 2
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case inr.refine_2
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * ↑n + 3

Tactic:
norm_cast

Goal state after:
case inr.refine_2
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 3
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: P : ℂ[X]
z w : ℂ
⊢ 0 ≤ P.derivRootWeight z w

Tactic:
simp only [derivRootWeight, Pi.single, Function.update_apply]

Goal state after:
P : ℂ[X]
z w : ℂ
⊢ 0 ≤ if eval z P = 0 then if w = z then 1 else 0 w else ↑(rootMultiplicity w P) / ‖z - w‖ ^ 2
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ log ‖circleMap 0 r θ - ρ‖ ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|

Tactic:
calc log ‖circleMap 0 r θ - ρ‖
      _ ≤ |log (2 * R)| + 0 + 0 := by
        grw [← le_abs_self, norm_sub_le, hρ, two_mul, norm_circleMap_zero, abs_of_pos hr, hrR]
        simp
      _ ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖| := by
        gcongr <;> positivity

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
this : ∑ x ∈ s, weight x • (z - x) = 0
⊢ z = (∑ i ∈ s, weight i)⁻¹ • ∑ i ∈ s, weight i • z

Tactic:
← Finset.sum_smul,

Goal state after:
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
this : ∑ x ∈ s, weight x • (z - x) = 0
⊢ z = (∑ i ∈ s, weight i)⁻¹ • (∑ i ∈ s, weight i) • z
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3

Tactic:
by
  have := @integral_sin_pow_odd_mul_cos_pow a b 1 0
  norm_num at this; exact this

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

Goal state before:
pp: w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
⊢ circleAverage (Complex.re ∘ herglotzRieszKernel c w * fun x ↦ log ‖x - ρ‖) c R = log ‖w - ρ‖

Tactic:
simp only [← circleAverage_map_add_const, Pi.mul_apply, Function.comp_apply, add_zero]
  conv =>
    left; arg 1
    intro z
    rw [(by ring : (z + 0 + c) - ρ = z - (ρ - c))]
    arg 1; arg 1
    rw [add_zero, herglotzRieszKernel_add_const c w z]
  have : (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) =
    (Complex.re ∘ herglotzRieszKernel 0 (w - c)) • (log ‖· - (ρ - c)‖) := by rfl
  rw [this, circleAverage_re_herglotzRieszKernel_mul_log₀ (by simp_all)
    (by simp_all [mem_ball_iff_norm.1 hw])]
  simp

Goal state after:
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
⊢ Monotone f

Tactic:
by
  rw [← monotoneOn_univ, ← @Iic_union_Ici _ _ a]
  exact MonotoneOn.union_right h₁ h₂ isGreatest_Iic isLeast_Ici

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : ¬im I = 1
⊢ ↑√(re a) = (map ℂ 𝕜) ((map 𝕜 ℂ) a).sqrt

Tactic:
have : (I : 𝕜) = 0 := by grind [I_eq_zero_or_im_I_eq_one]

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : ¬im I = 1
this : I = 0
⊢ ↑√(re a) = (map ℂ 𝕜) ((map 𝕜 ℂ) a).sqrt
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : ℝ
⊢ re (sqrt ↑a) = √a

Tactic:
by
  aesop (add simp [sqrt, Complex.re_sqrt_ofReal])

Goal state after:
Module: Mathlib.Topology.UrysohnsBounded

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
hx : x ∈ t
⊢ (BoundedContinuousFunction.const X a + (b - a) • f) x = Function.const X b x

Tactic:
by
    simp [hft hx]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Disc

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
a✝ : Nontrivial R
⊢ ↑(Fintype.card n) = 2

Tactic:
norm_cast

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

Goal state before:
pp: case pos
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
⊢ ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r) ≤
    ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)

pp: case neg
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∉ closedBall c |R|
⊢ ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r) ≤
    ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
· by_cases h2 : u ∈ closedBall c |r|
        · --In the smaller ball: the divisors agree and we bound the log factor
          simp only [(h₁f.mono (closedBall_subset_closedBall r_lt_R.le)), h2,
            AnalyticOnNhd.divisor_apply, h₁f, h1]
          by_cases! h3 : u = c --Need to use the divisor is 0 at c rather than comparing the logs
          · rw [h3, (h₁f c (by simp)).analyticOrderAt_eq_zero.mpr h₂f]
            simp
          simp +singlePass only [← log_abs]
          gcongr 2
          · simp
          · have : ‖c - u‖ ≠ 0 := by simpa [sub_eq_zero] using h3.symm
            simpa [field, abs_div, r_pos.trans r_lt_R, dist_eq_norm'] using h2
        · --In the larger ball but not the smaller so LHS is 0 and RHS nonnegative
          simp only [h2, not_false_eq_true, Function.locallyFinsuppWithin.apply_eq_zero_of_notMem,
            Int.cast_zero, zero_mul]
          refine mul_nonneg (mod_cast h₁f.divisor_nonneg ..) ?_
          apply log_abs _ ▸ log_nonneg
          simp only [mem_closedBall, dist_eq_norm', not_le] at h1 h2
          have : ‖c - u‖ ≠ 0 := (r_pos.trans h2).ne'
          simpa [field]

Goal state after:
case neg
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∉ closedBall c |R|
⊢ ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r) ≤
    ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ denom (-g) z = -denom g z

Tactic:
by
  simp [denom]; ring

Goal state after:
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
⊢ (¬∃ y, (scalar (Fin 2)) y = ↑g * m * (↑g)⁻¹) ∧ m.discr = 0 ↔ (¬∃ y, (scalar (Fin 2)) y = m) ∧ m.discr = 0

Tactic:
← Matrix.coe_units_inv,

Goal state after:
R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ (¬∃ y, (scalar (Fin 2)) y = ↑g * m * ↑g⁻¹) ∧ m.discr = 0 ↔ (¬∃ y, (scalar (Fin 2)) y = m) ∧ m.discr = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case neg
g : GL (Fin 2) ℝ
h : (↑g).det < 0
hadd : (↑g).trace = 0
hc : ¬↑g 1 0 = 0
⊢ ∃ z, g • z = z

Tactic:
use ⟨⟨-g 1 1 / g 1 0, √(-g.val.det) / |g 1 0|⟩, by simp [*]⟩

Goal state after:
case h
g : GL (Fin 2) ℝ
h : (↑g).det < 0
hadd : (↑g).trace = 0
hc : ¬↑g 1 0 = 0
⊢ g • { coe := { re := -↑g 1 1 / ↑g 1 0, im := √(-(↑g).det) / |↑g 1 0| }, coe_im_pos := ⋯ } =
    { coe := { re := -↑g 1 1 / ↑g 1 0, im := √(-(↑g).det) / |↑g 1 0| }, coe_im_pos := ⋯ }
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case refine_1.succ
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n✝ : ℕ
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
n : ℕ
hn : 1 ≤ n
IH : ((Matrix.scalar (Fin 2)) a + m) ^ n = (Matrix.scalar (Fin 2)) (a ^ n) + (↑n * a ^ (n - 1)) • m
⊢ ((Matrix.scalar (Fin 2)) a + m) ^ (n + 1) = (Matrix.scalar (Fin 2)) (a ^ (n + 1)) + (↑(n + 1) * a ^ (n + 1 - 1)) • m

Tactic:
simp only [pow_succ, IH, add_mul, Nat.add_sub_cancel, mul_add, ← map_mul, add_assoc]

Goal state after:
case refine_1.succ
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n✝ : ℕ
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
n : ℕ
hn : 1 ≤ n
IH : ((Matrix.scalar (Fin 2)) a + m) ^ n = (Matrix.scalar (Fin 2)) (a ^ n) + (↑n * a ^ (n - 1)) • m
⊢ (Matrix.scalar (Fin 2)) (a ^ n * a) +
      ((↑n * a ^ (n - 1)) • m * (Matrix.scalar (Fin 2)) a +
        ((Matrix.scalar (Fin 2)) (a ^ n) * m + (↑n * a ^ (n - 1)) • m * m)) =
    (Matrix.scalar (Fin 2)) (a ^ n * a) + (↑(n + 1) * a ^ n) • m
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGL ⟨!![a, b; c, d], ⋯⟩) ↑z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ ↑c ≠ 0

Tactic:
norm_cast

Goal state after: