mathlib-initiative/mathlib-tactics huggingface dataset:
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|))
⊢ Tendsto (fun R ↦ δ * expR (d * R) + B * expR (c * R) + Real.log A) atTop atBot

Tactic:
suffices H : Tendsto (fun R => δ + B * (expR ((d - c) * R))⁻¹) atTop (𝓝 (δ + B * 0)) by
      rw [mul_zero, add_zero] at H
      refine Tendsto.atBot_add ?_ tendsto_const_nhds
      simpa only [id, (· ∘ ·), add_mul, mul_assoc, ← div_eq_inv_mul, ← Real.exp_sub, ← sub_mul,
        sub_sub_cancel]
        using H.neg_mul_atTop δ₀ <| Real.tendsto_exp_atTop.comp <| tendsto_id.const_mul_atTop hd₀

Goal state after:
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|))
⊢ Tendsto (fun R ↦ δ + B * (expR ((d - c) * R))⁻¹) atTop (𝓝 (δ + B * 0))
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ (a - b)⁻¹ • ∫ (x : ℝ) in Ioc b a, f x = -(b - a)⁻¹ • ∫ (x : ℝ) in Ioc b a, f x ∂volume

Tactic:
← inv_neg,

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ (a - b)⁻¹ • ∫ (x : ℝ) in Ioc b a, f x = (-(b - a))⁻¹ • ∫ (x : ℝ) in Ioc b a, f x ∂volume
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 (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
⊢ cexp z ∈ Ioi 0 ×ℂ Ioi 0

Tactic:
by
    rw [mem_reProdIm, exp_re, exp_im, mem_Ioi, mem_Ioi]
    have : 0 < Real.cos z.im := Real.cos_pos_of_mem_Ioo ⟨by linarith [hz.1, hz.2], hz.2⟩
    have : 0 < Real.sin z.im :=
      Real.sin_pos_of_mem_Ioo ⟨hz.1, hz.2.trans (half_lt_self Real.pi_pos)⟩
    constructor <;> positivity

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

Goal state before:
pp: R : ℝ
w : ℂ
g : ℂ → ℝ
hg : CircleIntegrable g 0 R
hw : w ∈ ball 0 R
h₁ : CircleIntegrable (fun ζ ↦ ↑(g ζ)) 0 R
h₂ : CircleIntegrable (fun ζ ↦ herglotzRieszKernel 0 w ζ • ↑(g ζ)) 0 R
⊢ circleAverage (⇑reCLM ∘ fun ζ ↦ herglotzRieszKernel 0 w ζ • ↑(g ζ)) 0 R =
    circleAverage (re ∘ herglotzRieszKernel 0 w • g) 0 R

Tactic:
by
        simp [Function.comp_def, Complex.mul_re, Pi.mul_def]

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

Goal state before:
pp: ⊢ Tendsto (deriv fun x ↦ x * log x) (𝓝[>] 0) atBot

Tactic:
by
  have : (deriv (fun x ↦ x * log x)) =ᶠ[𝓝[>] 0] (fun x ↦ log x + 1) := by
    apply eventuallyEq_nhdsWithin_of_eqOn
    intro x hx
    rw [Set.mem_Ioi] at hx
    exact deriv_mul_log hx.ne'
  simp only [tendsto_congr' this, tendsto_atBot_add_const_right, tendsto_log_nhdsGT_zero]

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

Goal state before:
pp: case inr.inr
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
⊢ Real.circleAverage (fun z ↦ ((z + w) / (z - w)).re • f z) 0 R = f w

Tactic:
let W := R * exp (w.arg * I)

Goal state after:
case inr.inr
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)
⊢ Real.circleAverage (fun z ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case pos
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'
hfc : ContinuousOn (fun x ↦ f ↑x) (Ici 0)
h₀ : ∀ (x : ℝ), 0 ≤ x → f ↑x = 0
y : ℝ
hy : 0 ≤ y
⊢ ‖f ↑y‖ ≤ ‖f ↑0‖

Tactic:
rw [h₀ y hy, h₀ 0 le_rfl]

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

Goal state before:
pp: case pos
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'
hfc : ContinuousOn (fun x ↦ f ↑x) (Ici 0)
h₀ : ∀ (x : ℝ), 0 ≤ x → f ↑x = 0
⊢ ∃ x, 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x‖

pp: case neg
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'
hfc : ContinuousOn (fun x ↦ f ↑x) (Ici 0)
h₀ : ∃ x, 0 ≤ x ∧ f ↑x ≠ 0
⊢ ∃ x, 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x‖

Tactic:
· refine ⟨0, le_rfl, fun y hy => ?_⟩; rw [h₀ y hy, h₀ 0 le_rfl]

Goal state after:
case neg
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'
hfc : ContinuousOn (fun x ↦ f ↑x) (Ici 0)
h₀ : ∃ x, 0 ≤ x ∧ f ↑x ≠ 0
⊢ ∃ x, 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x‖
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun t ↦ ‖↑t ^ r‖) volume 0 c

Tactic:
rw [intervalIntegrable_iff]

Goal state after:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn (fun t ↦ ‖↑t ^ r‖) (Ι 0 c) volume
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
hg : CircleIntegrable f 0 R
hw : w ∈ ball 0 R
hR : 0 < R
d : ℝ
hd : d > 0
hsub : ball w d ⊆ ball 0 R
hdist : ∀ x ∈ ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap 0 R θ - x‖
hgm : AEStronglyMeasurable (fun θ ↦ f (circleMap 0 R θ)) (volume.restrict (uIoc 0 (2 * π)))
x : ℂ
⊢ AEStronglyMeasurable (fun θ ↦ (circleMap 0 R θ + x) / (circleMap 0 R θ - x)) (volume.restrict (uIoc 0 (2 * π)))

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

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

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

Tactic:
by
    apply integral_congr_codiscreteWithin
    apply codiscreteWithin_mono (by tauto : Ι 0 π ⊆ Set.univ)
    have : AnalyticOnNhd ℝ (4 * sin · ^ 2) Set.univ := fun _ _ ↦ by fun_prop
    have := this.preimage_zero_mem_codiscrete (x := π / 2)
    simp only [sin_pi_div_two, one_pow, mul_one, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
      Set.preimage_compl, forall_const] at this
    filter_upwards [this] with a ha
    simp only [Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff, mul_eq_zero,
      OfNat.ofNat_ne_zero, ne_eq, not_false_eq_true, pow_eq_zero_iff, false_or] at ha
    rw [log_mul (by simp) (by simp_all), log_pow, Nat.cast_ofNat]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
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 : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
H : ∀ (n : ℕ), ‖g n z‖ ≤ C
⊢ f z = 0

Tactic:
contrapose! H

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
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 : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
H : f z ≠ 0
⊢ ∃ n, C < ‖g n z‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : x ∈ closedBall 0 |1|
⊢ x ≠ a

Tactic:
by_contra!

Goal state after:
a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : x ∈ closedBall 0 |1|
this : x = a
⊢ False
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z ↦ ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
z : ℂ
hz : z ∈ sphere z₀ r
⊢ ε / 2 ≤ ‖f z - v‖

Tactic:
linarith [hf z hz, show ‖v - f z₀‖ < ε / 2 from mem_ball_iff_norm.1 hv,
      norm_sub_sub_norm_sub_le_norm_sub (f z) v (f z₀)]

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 : f ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id
this : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Tactic:
← EventuallyEq.eq_of_nhds (qdiff.hasStrictFDerivAt_equiv diff_ne).eventually_left_inverse

Goal state after:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * ↑π * I / ↑h)) z
diff_ne : q * (2 * ↑π * I / ↑h) ≠ 0
hol_z :
  DifferentiableAt ℂ f
    (HasStrictFDerivAt.localInverse (𝕢 h)
      ((ContinuousLinearEquiv.unitsEquivAut ℂ) (Units.mk0 (q * (2 * ↑π * I / ↑h)) diff_ne)) z ⋯ (𝕢 h z))
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.JensenFormula

Goal state before:
pp: case h_bound
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x

pp: case bound_integrable
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ IntervalIntegrable bound volume 0 (2 * π)

pp: case h_lim
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᵐ (x : ℝ),
    x ∈ uIoc 0 (2 * π) →
      Tendsto (fun n ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) atTop
        (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R x)))

Tactic:
· -- Pointwise boundedness outside a null set
    filter_upwards [hr_tendsto.eventually (le_mem_nhds (by linarith : (R + ‖w‖) / 2 < R))] with n hn
    have h_bound {θ : ℝ} :
        ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ ∨ ‖circleMap 0 R θ - ρ‖ = 0 := by
      refine Classical.or_iff_not_imp_right.mpr fun h ↦ ?_
      apply norm_herglotzLogIntegrand_circleMap_le hR hρ (by positivity) (by linarith) hn
        (hr_lt n).le
      simpa using! h
    apply measure_mono_null (t := {θ | ‖circleMap 0 R θ - ρ‖ = 0}) (by grind)
    simpa [sub_eq_zero] using!
      (countable_singleton ρ).preimage_circleMap 0 (hR.ne') |>.measure_zero _

Goal state after:
case bound_integrable
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ IntervalIntegrable bound volume 0 (2 * π)

case h_lim
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᵐ (x : ℝ),
    x ∈ uIoc 0 (2 * π) →
      Tendsto (fun n ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) atTop
        (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R x)))
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
⊢ sqrt (-I) = ↑√2⁻¹ * (1 + I) * -I

Tactic:
by
  rw [sqrt_eq_ite]
  split_ifs with h
  · simp_rw [RingEquiv.symm_apply_eq, map_mul]
    simp [h, mul_assoc, add_comm, Complex.sqrt_neg_I, neg_mul, mul_add, add_mul, mul_sub,
      mul_comm Complex.I, ← sub_eq_add_neg]
  grind [I_eq_zero_or_im_I_eq_one]

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

Goal state before:
pp: 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|
this : (∑ᶠ (a : ℂ), ↑((divisor f (closedBall c |r|)) a)) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)
⊢ 0 < Real.log (R / r)

Tactic:
simpa using log_pos hrR

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: 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
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
⊢ Disjoint (Iic (-‖f‖ / 3)) (Ici (‖f‖ / 3))

Tactic:
rwa [Iic_disjoint_Ici, not_le]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ (smulAux' g z).im = |↑(GeneralLinearGroup.det g)| * z.im / Complex.normSq (denom g z)

Tactic:
simp only [smulAux', σ]

Goal state after:
g : GL (Fin 2) ℝ
z : ℂ
⊢ ((if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
        (num g z / denom g z)).im =
    |↑(GeneralLinearGroup.det g)| * z.im / Complex.normSq (denom g z)
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: 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‖
n : ℕ
⊢ ‖f - (g n).compContinuous e‖ / 3 = 1 / 3 * ‖f - (g n).compContinuous e‖

Tactic:
one_div,

Goal state after:
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‖
n : ℕ
⊢ ‖f - (g n).compContinuous e‖ / 3 = 3⁻¹ * ‖f - (g n).compContinuous e‖
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
c : ℝ := ↑g 1 0
d : ℝ := ↑g 1 1
⊢ (c * z.im) ^ 2 + (c * z.re + d) ^ 2 = Complex.normSq (denom g ↑z)

Tactic:
by simp [denom, Complex.normSq]; ring

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

Goal state before:
pp: τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : ‖r - ‖↑τ‖‖ < ε
hr' : r < 0
⊢ False

Tactic:
Real.norm_eq_abs,

Goal state after:
τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : |r - ‖↑τ‖| < ε
hr' : r < 0
⊢ False
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((evalRingHom 0).mapMatrix ((Matrix.comp m m n n R[X]) ((cornerAddX M k).map ⇑f.polyToMatrix))).det =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det

Tactic:
← compRingEquiv_apply,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((evalRingHom 0).mapMatrix ((compRingEquiv m n R[X]) ((cornerAddX M k).map ⇑f.polyToMatrix))).det =
    ((compRingEquiv m n R) (M.map ⇑f)).det
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp m m n n R) (f.mapMatrix M)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (f.mapMatrix (M * auxMat M k))).det

Tactic:
← compRingEquiv_apply,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((compRingEquiv m n R) (f.mapMatrix M)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((compRingEquiv m n R) (f.mapMatrix (M * auxMat M k))).det
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
ih :
  ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
    (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det
⊢ (f (M k k)).det *
        ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
            (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det -
      (f (M k k)).det *
        ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
            (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    0

Tactic:
sub_self

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
ih :
  ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
    (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det
⊢ 0 = 0
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
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:
cases fintypeOrInfinite ιA

Goal state after:
case inl.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
val✝ : Fintype ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

case inl.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✝¹ : Fintype ιS
val✝ : Infinite ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ |sinh x| = sinh |x|

Tactic:
cases le_total x 0 <;> simp [abs_of_nonneg, abs_of_nonpos, *]

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ Epi f

Tactic:
rw [← CategoryTheory.ofHom_epi_iff_surjective] at hf

Goal state after:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Epi (↾⇑(ConcreteCategory.hom f))
⊢ Epi f