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

Goal state before:
pp: case neg.inr.refine_2.inr
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntervalIntegrable (fun x ↦ ‖↑x ^ r‖) μ c 0

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hc.le]

Goal state after:
case neg.inr.refine_2.inr
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntegrableOn (fun x ↦ ‖↑x ^ r‖) (Ioc c 0) μ
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
z : ℂ
hz : z ∈ sphere 0 |R|
hzR : ‖z‖ = R
⊢ ↑((z + w) / (z - w)).re = z / (z - w) - ↑‖w‖ / ↑R * z / (↑‖w‖ / ↑R * z - ↑R * cexp (↑w.arg * I))

Tactic:
rw [← norm_mul_exp_arg_mul_I w, ← norm_mul_exp_arg_mul_I z, hzR,
        ← circleAverage_re_smul_on_ball_zero_aux, norm_mul_exp_arg_mul_I w]

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
z : ℂ
hz : z ∈ sphere 0 |R|
hzR : ‖z‖ = R
⊢ ↑R * cexp (↑z.arg * I) / (↑R * cexp (↑z.arg * I) - w) -
      ↑‖w‖ * cexp (↑z.arg * I) / (↑‖w‖ * cexp (↑z.arg * I) - ↑R * cexp (↑w.arg * I)) =
    ↑R * cexp (↑z.arg * I) / (↑R * cexp (↑z.arg * I) - w) -
      ↑‖w‖ / ↑R * (↑R * cexp (↑z.arg * I)) / (↑‖w‖ / ↑R * (↑R * cexp (↑z.arg * I)) - ↑R * cexp (↑w.arg * I))
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

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

Tactic:
posLog_abs

Goal state after:
case h₂
α : Type u_1
s : Finset α
f : α → ℝ
hs : s.Nonempty
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (f t_max) ≤ ∑ t ∈ s, log⁺ (f t)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: 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
⊢ ↑r + 1 = ↑(r + 1)

Tactic:
push_cast; rfl

Goal state after:
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
⊢ (r + 1)⁻¹ * (b ^ (r + 1) - a ^ (r + 1)) = ((↑(r + 1))⁻¹ * (↑b ^ ↑(r + 1) - ↑a ^ ↑(r + 1))).re

Tactic:
← Complex.ofReal_inv,

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
⊢ (r + 1)⁻¹ * (b ^ (r + 1) - a ^ (r + 1)) = (↑(r + 1)⁻¹ * (↑b ^ ↑(r + 1) - ↑a ^ ↑(r + 1))).re
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

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

Tactic:
calc ∫ x in 0..(2 * π), log (4 * sin (x / 2) ^ 2) / 2
  _ = ∫ (x : ℝ) in 0..π, log (4 * sin x ^ 2) := by
    have {x : ℝ} : x / 2 = 2⁻¹ * x := by ring
    rw [intervalIntegral.integral_div, this, inv_mul_integral_comp_div
      (f := fun x ↦ log (4 * sin x ^ 2))]
    simp
  _ = ∫ (x : ℝ) in 0..π, log 4 + 2 * log (sin x) := 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]
  _ = (∫ (x : ℝ) in 0..π, log 4) + 2 * ∫ (x : ℝ) in 0..π, log (sin x) := by
    rw [integral_add _root_.intervalIntegrable_const
      (by apply intervalIntegrable_log_sin.const_mul 2), intervalIntegral.integral_const_mul]
  _ = 0 := by
    simp only [intervalIntegral.integral_const, sub_zero, smul_eq_mul, integral_log_sin_zero_pi,
      (by norm_num : (4 : ℝ) = 2 * 2), log_mul two_ne_zero two_ne_zero]
    ring

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

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ 2 - 2 * cos x = 2 - 2 * cos (2 * (x / 2))

Tactic:
rw [← mul_div_assoc]
      simp

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

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
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
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ ∀ᶠ (x : ℂ) in cobounded ℂ ⊓ 𝓟 {z | 0 < z.re},
    ‖expR x.re ^ n * expR (B * ‖x‖ ^ c)‖ ≤ ‖expR ((↑n + max B 0) * ‖x‖ ^ max c 1)‖

Tactic:
filter_upwards [(eventually_cobounded_le_norm 1).filter_mono inf_le_left] with z hz

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
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
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : 1 ≤ ‖z‖
⊢ ‖expR z.re ^ n * expR (B * ‖z‖ ^ c)‖ ≤ ‖expR ((↑n + max B 0) * ‖z‖ ^ max c 1)‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hderiv
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y ↦ 1 + y ^ 2) (2 * ↑x) ↑x
g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
⊢ 0 < (1 + ↑x ^ 2).re

Tactic:
exact mod_cast add_pos_of_pos_of_nonneg zero_lt_one (sq_nonneg x)

Goal state after:
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 (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|) ≤ log ‖circleMap 0 r θ - ρ‖

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:
· have h_log_lower_bound :
          log ‖circleMap 0 r θ - ρ‖ ≥ log (sqrt (r₀ / R)) + log ‖circleMap 0 R θ - ρ‖ := by
        rw [← log_mul (by positivity) (by positivity)]
        gcongr
      grind

Goal state after:
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 θ - ρ‖|
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: p : ℂ[X]
⊢ (∃ x, C x = p) ∨ IsOpenQuotientMap fun x ↦ eval x p

Tactic:
refine or_iff_not_imp_left.mpr fun h ↦ ?_

Goal state after:
p : ℂ[X]
h : ¬∃ x, C x = p
⊢ IsOpenQuotientMap fun x ↦ eval x p
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: case inr
p : ℂ[X]
h : ¬∃ x, C x = p
hp : IsOpenMap fun x ↦ eval x p
⊢ IsOpenQuotientMap fun x ↦ eval x p

Tactic:
· exact ⟨IsAlgClosed.eval_surjective <| natDegree_eq_zero.not.mpr h, p.continuous_aeval, hp⟩

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

Goal state before:
pp: 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

Tactic:
split_ifs

Goal state after:
case pos
P : ℂ[X]
z w : ℂ
h✝¹ : eval z P = 0
h✝ : w = z
⊢ 0 ≤ 1

case neg
P : ℂ[X]
z w : ℂ
h✝¹ : eval z P = 0
h✝ : ¬w = z
⊢ 0 ≤ 0 w

case neg
P : ℂ[X]
z w : ℂ
h✝ : ¬eval z P = 0
⊢ 0 ≤ ↑(rootMultiplicity w P) / ‖z - w‖ ^ 2
Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < q.degree
⊢ False

Tactic:
← degree_map_eq_of_injective (algebraMap ℤ ℂ).injective_int

Goal state after:
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
⊢ False
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ :=
  fun θ ↦ (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
n : ℕ
hn : (R + ‖w‖) / 2 ≤ r n
h_bound : ∀ {θ : ℝ}, ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ ∨ ‖circleMap 0 R θ - ρ‖ = 0
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x

Tactic:
apply measure_mono_null (t := {θ | ‖circleMap 0 R θ - ρ‖ = 0}) (by grind)

Goal state after:
ρ 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 : ℕ
hn : (R + ‖w‖) / 2 ≤ r n
h_bound : ∀ {θ : ℝ}, ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ ∨ ‖circleMap 0 R θ - ρ‖ = 0
⊢ volume {θ | ‖circleMap 0 R θ - ρ‖ = 0} = 0
Module: Mathlib.Analysis.Complex.Positivity

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ ↑(z - c).re
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * ↑(z - c).re ^ n = f z
hz' : z - c = ↑(z - c).re
n : ℕ
⊢ 0 ≤ ↑(↑n.factorial)⁻¹ * iteratedDeriv n f c * ↑((z - c).re ^ n)

Tactic:
eq_re_of_ofReal_le (h n),

Goal state after:
f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ ↑(z - c).re
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * ↑(z - c).re ^ n = f z
hz' : z - c = ↑(z - c).re
n : ℕ
⊢ 0 ≤ ↑(↑n.factorial)⁻¹ * ↑(iteratedDeriv n f c).re * ↑((z - c).re ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: x✝ : ℝ
h : -(π / 2) < x✝ ∧ x✝ ≤ π / 2
⊢ cos x✝ * cos x✝ = cos x✝ ^ 2

Tactic:
pow_two

Goal state after:
x✝ : ℝ
h : -(π / 2) < x✝ ∧ x✝ ≤ π / 2
⊢ cos x✝ * cos x✝ = cos x✝ * cos x✝
Module: Mathlib.Order.Monotone.Odd

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : AddCommGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x < y
⊢ f (-y) < f (-x)

Tactic:
exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_lt_neg hxy)

Goal state after:
Module: Mathlib.Order.Interval.Set.IsoIoo

Goal state before:
pp: case refine_2.refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ StrictMonoOn (fun x ↦ x / (1 + |x|)) (Ici 0)

Tactic:
rintro x (hx : 0 ≤ x) y (hy : 0 ≤ y) hxy

Goal state after:
case refine_2.refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
x : k
hx : 0 ≤ x
y : k
hy : 0 ≤ y
hxy : x < y
⊢ (fun x ↦ x / (1 + |x|)) x < (fun x ↦ x / (1 + |x|)) y
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 : ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)

Tactic:
rwa [← finsum_mul, ← le_div_iff₀] at this
    simpa using log_pos hrR

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

Goal state before:
pp: case h₂f.h.h.inl
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‖
z : ℂ
hz : z ∈ sphere c |R|
this : ‖f z‖ ≤ M
h : f z = 0
⊢ Real.log ‖f z‖ ≤ Real.log M

Tactic:
simpa [h] using log_nonneg hM

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

Goal state before:
pp: 𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
⊢ ↑(closedBall y r) ≃ₜ ↑(closedBall 0 1)

Tactic:
by
    symm
    apply (DilationEquiv.smulTorsor y (k := (r : 𝕜)) <| by exact_mod_cast hr.ne').toHomeomorph.sets
    ext x
    simp only [mem_closedBall, dist_zero_right, DilationEquiv.coe_toHomeomorph, Set.mem_preimage,
      DilationEquiv.smulTorsor_apply, vadd_eq_add, dist_add_self_left, norm_smul,
      RCLike.norm_ofReal, abs_of_nonneg hr.le]
    exact (mul_le_iff_le_one_right hr).symm

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
hz : z.im ≠ 0
⊢ denom g z ≠ 0

Tactic:
by
  refine linear_ne_zero_of_im hz fun H ↦ g.det.ne_zero ?_
  simp [Matrix.det_fin_two, H]

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

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

Tactic:
split_ifs

Goal state after:
case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ((starRingEnd ℂ) z) = (starRingEnd ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z)

case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ Complex.conjCAE ((starRingEnd ℂ) z) = (starRingEnd ℂ) (Complex.conjCAE z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
y : ℝ
⊢ (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) ↑y = ↑y

Tactic:
split_ifs

Goal state after:
case pos
g : GL (Fin 2) ℝ
y : ℝ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ↑y = ↑y

case neg
g : GL (Fin 2) ℝ
y : ℝ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ Complex.conjCAE ↑y = ↑y
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

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

Tactic:
split_ifs

Goal state after:
case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z) = z

case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ Complex.conjCAE (Complex.conjCAE z) = z
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ ((if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z).im ≠ 0 ↔ z.im ≠ 0

Tactic:
split_ifs

Goal state after:
case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ ((ContinuousAlgEquiv.refl ℝ ℂ) z).im ≠ 0 ↔ z.im ≠ 0

case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ (Complex.conjCAE z).im ≠ 0 ↔ z.im ≠ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

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

Tactic:
split_ifs

Goal state after:
case pos
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : 0 < ↑(GeneralLinearGroup.det g)
h✝ : 0 < ↑(GeneralLinearGroup.det h)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z) =
    (ContinuousAlgEquiv.refl ℝ ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z)

case neg
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : 0 < ↑(GeneralLinearGroup.det g)
h✝ : ¬0 < ↑(GeneralLinearGroup.det h)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) (Complex.conjCAE z) = Complex.conjCAE ((ContinuousAlgEquiv.refl ℝ ℂ) z)

case pos
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : ¬0 < ↑(GeneralLinearGroup.det g)
h✝ : 0 < ↑(GeneralLinearGroup.det h)
⊢ Complex.conjCAE ((ContinuousAlgEquiv.refl ℝ ℂ) z) = (ContinuousAlgEquiv.refl ℝ ℂ) (Complex.conjCAE z)

case neg
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : ¬0 < ↑(GeneralLinearGroup.det g)
h✝ : ¬0 < ↑(GeneralLinearGroup.det h)
⊢ Complex.conjCAE (Complex.conjCAE z) = Complex.conjCAE (Complex.conjCAE z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

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

Tactic:
split_ifs

Goal state after:
case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ ‖(ContinuousAlgEquiv.refl ℝ ℂ) z‖ = ‖z‖

case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ ‖Complex.conjCAE z‖ = ‖z‖
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: case refine_1
g : GL (Fin 2) ℝ
⊢ Continuous ⇑(if 0 < ↑(Matrix.GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else conjCAE)

Tactic:
split_ifs

Goal state after:
case pos
g : GL (Fin 2) ℝ
h✝ : 0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ Continuous ⇑(ContinuousAlgEquiv.refl ℝ ℂ)

case neg
g : GL (Fin 2) ℝ
h✝ : ¬0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ Continuous ⇑conjCAE
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]
      simp only [scalar_apply, ← smul_eq_mul_diagonal, ← mul_smul,
        ← smul_eq_diagonal_mul, smul_mul, ← sq, hmsq, smul_zero, add_zero, ← add_smul,
        Nat.cast_add_one, add_mul, one_mul]
      rw [(by lia : n = n - 1 + 1), pow_succ, (by lia : n - 1 + 1 = n)]
      ring_nf

Goal state after:
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
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
⊢ (∃ x, x ≠ 0 ∧ g = upperRightHom x) ∨ ∃ x, x ≠ 0 ∧ g = -upperRightHom x

Tactic:
apply (sq_eq_one_iff.mp this).imp <;> intro hg11

Goal state after:
case mp.f
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 : ↑g 1 1 ^ 2 = 1
hg11 : ↑g 1 1 = 1
⊢ ∃ x, x ≠ 0 ∧ g = upperRightHom x

case mp.g
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 : ↑g 1 1 ^ 2 = 1
hg11 : ↑g 1 1 = -1
⊢ ∃ x, x ≠ 0 ∧ g = -upperRightHom x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure

Goal state before:
pp: s : Set ℍ
⊢ Measure.map UpperHalfPlane.coe (Measure.comap UpperHalfPlane.coe volume) =
    volume.restrict (Set.range UpperHalfPlane.coe)

Tactic:
measurableEmbedding_coe.map_comap

Goal state after:
s : Set ℍ
⊢ volume.restrict (Set.range UpperHalfPlane.coe) = volume.restrict (Set.range UpperHalfPlane.coe)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case left
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ Tendsto id (𝓝 z) (𝓝 ↑(↑ofComplex z))

Tactic:
simpa [ofComplex_apply_of_im_pos hz] using! tendsto_id

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.inr.inl.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hyb : (g - dg) y < b
xu : X
hyxu : (g - dg) y < f xu
right✝ : f xu ≤ b
hc : c < g y
h✝ : a ∉ range ⇑f
⊢ ∃ x₁ x₂, (g - dg) y ∈ Icc (f x₁) (f x₂)

Tactic:
have hay : a < (g - dg) y := by
        calc
          a = c - (b - c) := by rw [← hsub, sub_sub_cancel]
          _ < g y - (b - c) := sub_lt_sub_right hc _
          _ ≤ g y - dg y := sub_le_sub_left (dgmem _).2 _
      rcases ha.exists_between hay with ⟨_, ⟨x, rfl⟩, _, hxy⟩
      exact ⟨x, xu, hxy.le, hyxu.le⟩

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

Goal state before:
pp: z w : ℍ
⊢ dist ↑z ↑w / (2 * √(z.im * w.im)) / cosh (dist z w / 2) = dist ↑z ↑w / dist (↑z) ((starRingEnd ℂ) ↑w)

Tactic:
cosh_half_dist,

Goal state after:
z w : ℍ
⊢ dist ↑z ↑w / (2 * √(z.im * w.im)) / (dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))) =
    dist ↑z ↑w / dist (↑z) ((starRingEnd ℂ) ↑w)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ dist ↑z ↑w / (2 * √(z.im * w.im)) + cosh (dist z w / 2) =
    (dist ↑z ↑w + dist (↑z) ((starRingEnd ℂ) ↑w)) / (2 * √(z.im * w.im))

Tactic:
cosh_half_dist,

Goal state after:
z w : ℍ
⊢ dist ↑z ↑w / (2 * √(z.im * w.im)) + dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im)) =
    (dist ↑z ↑w + dist (↑z) ((starRingEnd ℂ) ↑w)) / (2 * √(z.im * w.im))