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

Goal state before:
pp: case inr
a b r : ℝ
h✝ : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ¬↑r = ↑(-1) ∧ 0 ∉ [[a, b]]

Tactic:
Complex.ofReal_inj

Goal state after:
case inr
a b r : ℝ
h✝ : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ¬r = -1 ∧ 0 ∉ [[a, b]]
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:
rfl

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

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

Tactic:
by
      apply intervalIntegral.integral_congr_codiscreteWithin
      apply Filter.codiscreteWithin_mono (by tauto : Ι 0 (π / 2) ⊆ Set.univ)
      have t₀ : sin ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_sin.preimage_zero_mem_codiscrete (x := π / 2)
        simp
      have t₁ : cos ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_cos.preimage_zero_mem_codiscrete (x := 0)
        simp
      filter_upwards [t₀, t₁] with y h₁y h₂y
      simp_all only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
        sin_two_mul, ne_eq, mul_eq_zero, OfNat.ofNat_ne_zero, or_self, not_false_eq_true, log_mul]
      ring

Goal state after:
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 ↦ expR (ε * x) • f ↑x) atTop (𝓝 0)

Tactic:
have h₀ : Tendsto (fun x : ℝ => expR (ε * x)) atTop (𝓝 0) :=
      Real.tendsto_exp_atBot.comp (tendsto_const_nhds.neg_mul_atTop ε₀ tendsto_id)

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‖
h₀ : Tendsto (fun x ↦ expR (ε * x)) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ expR (ε * x) • f ↑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]]
t₀ : ∀ (u : ↑[[a, b]]), meromorphicOrderAt f ↑u = ⊤
x : ℝ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ [[a, b]]
hCon : ¬f x = 0
⊢ False

Tactic:
simp_all [← h₁x.meromorphicOrderAt_eq_zero_iff, t₀ ⟨x, h₂x⟩]

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

Goal state before:
pp: a b : ℝ
h : 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, 1 / x = log (b / a)

Tactic:
simp only [one_div, integral_inv h]

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

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
⊢ circleAverage (fun x ↦ log ‖x - a‖) 0 1 = circleAverage (fun x ↦ log ‖1 - x⁻¹ * a‖) 0 1

Tactic:
apply circleAverage_congr_sphere
    intro z hz
    simp_all only [abs_one, mem_sphere_iff_norm, sub_zero]
    congr 1
    have : z ≠ 0 := fun h ↦ by simp [h] at hz
    calc ‖z - a‖
    _ = ‖z⁻¹ * (z - a)‖ := by simp [hz]
    _ = ‖1 - z⁻¹ * a‖ := by field_simp

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

Goal state before:
pp: case hderiv
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y ↦ y * z) z ↑x
c : HasDerivAt (Complex.sin ∘ fun y ↦ y * z) (Complex.cos (↑x * z) * z) ↑x
d : HasDerivAt (fun y ↦ (Complex.sin ∘ fun y ↦ y * z) ↑y / z) (Complex.cos (↑x * z) * z / z) x
⊢ HasDerivAt (fun b ↦ Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

Tactic:
grind

Goal state after:
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|)
t₀ : ∀ (u : ↑(sphere c |R|)), meromorphicOrderAt f ↑u = ⊤
x : ℂ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ sphere c |R|
hCon : ¬f x = 0
⊢ False

Tactic:
simp_all [← h₁x.meromorphicOrderAt_eq_zero_iff, t₀ ⟨x, h₂x⟩]

Goal state after:
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

pp: case hx
a b t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ 0 ≤ 1 + x ^ 2

Tactic:
ofReal_pow,

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

case hx
a b t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ 0 ≤ 1 + x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b t : ℝ
ht : t ≠ -1
⊢ ∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t = (1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))

Tactic:
have : ∀ x s : ℝ, (((↑1 + x ^ 2) ^ s : ℝ) : ℂ) = (1 + (x : ℂ) ^ 2) ^ (s : ℂ) := by
    intro x s
    norm_cast
    rw [ofReal_cpow, ofReal_add, ofReal_pow, ofReal_one]
    exact add_nonneg zero_le_one (sq_nonneg x)

Goal state after:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t = (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: 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:
rfl

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

Goal state before:
pp: case funProp.discharger
w ρ z : ℂ
hz_w : z ≠ w
hz_ρ : z ≠ ρ
this : ‖z - ρ‖ ≠ 0
⊢ z - w ≠ 0

Tactic:
grind

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 θ - ρ‖
⊢ 0 < r₀ - ‖w‖ ∧ 0 < r

Tactic:
grind

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 θ - ρ‖
⊢ (r + ‖w‖) / (r - ‖w‖) ≤ (r + ‖w‖) / (r - ‖w‖)

Tactic:
grind

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

Goal state before:
pp: case hd
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 θ - ρ‖
⊢ 0 < r - ‖w‖

Tactic:
grind

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

Tactic:
grind

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
hzP : ¬eval z P = 0
⊢ (starRingEnd ℂ) (Multiset.map (fun x ↦ 1 / (z - x)) P.roots).sum = 0

Tactic:
rw [← (IsAlgClosed.splits _).eval_derivative_div_eval_of_ne_zero hzP]
      simp [hz]

Goal state after:
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 | (fun x ↦ x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x) x}ᶜ ⊆
    {θ | ‖circleMap 0 R θ - ρ‖ = 0}

Tactic:
grind

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

Goal state before:
pp: case hbc
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := ⋯
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < ↑n + 2
⊢ 1 < ↑n + 2

Tactic:
grind

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

Goal state before:
pp: case hf.refine_2
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
x : ℂ
hx : x ∈ closure (ball 0 (r n))
key : ‖x‖ ≤ r n
⊢ x ≠ ρ

Tactic:
grind

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

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

Tactic:
rfl

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

Goal state before:
pp: case neg
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : D c = 0
x : ℂ
h₁ : ¬c = x
⊢ ↑(D x) * (log R - log ‖c - x‖) = ↑(D x) * log (R * ‖c - x‖⁻¹)

Tactic:
rw [log_mul hR (inv_ne_zero (norm_ne_zero_iff.mpr (sub_eq_zero.not.2 h₁))), log_inv]
      ring

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

Goal state before:
pp: a : ℝ
⊢ √((|a| + a) / 2) = √a

Tactic:
grind

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

Goal state before:
pp: a : ℝ
⊢ sqrt a = √a

Tactic:
simp [← re_sqrt_ofReal (𝕜 := ℝ)]

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 : ∑ᶠ (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:
← finsum_mul,

Goal state after:
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‖)
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
M : Type u_3
inst✝ : Monoid M
f : GL n R →* M
hf : f.comp (GeneralLinearGroup.scalar n) = 1
g : GL n R
⊢ (lift f hf) (mk g) = f g

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
M : Type u_3
inst✝ : Monoid M
f : GL n R →* M
hf : f.comp (GeneralLinearGroup.scalar n) = 1
⊢ (lift f hf).comp mk = f

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
α : Type u_4
inst✝ : MulAction (GL n R) α
h : ∀ (u : Rˣ) (a : α), (GeneralLinearGroup.scalar n) u • a = a
g : GL n R
a : α
⊢ mk g • a = g • a

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : Fact (Even (Fintype.card n))
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
g : GL n R
⊢ signDet (mk g) = (Units.map ↑signHom) (GeneralLinearGroup.det g)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : Fact (Even (Fintype.card n))
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
g : GL n R
⊢ ↑(signDet (mk g)) = SignType.sign ↑(GeneralLinearGroup.det g)

Tactic:
rfl

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

Goal state before:
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|
h2 : 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:
· --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:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 = 0
h₀ : ↑g 1 1 ≠ 0
⊢ g • z = z ↔ z.re = ↑g 0 1 / (2 * ↑g 1 1)

Tactic:
have h : g.val.det < 0 := by simp [Matrix.det_fin_two, *]

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 = 0
h₀ : ↑g 1 1 ≠ 0
h : (↑g).det < 0
⊢ g • z = z ↔ z.re = ↑g 0 1 / (2 * ↑g 1 1)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 = 0
h₀ : ↑g 1 1 ≠ 0
h : (↑g).det < 0
⊢ -(z.re * ↑g 1 1) + ↑g 0 1 = z.re * ↑g 1 1 ↔ z.re * (2 * ↑g 1 1) = ↑g 0 1

Tactic:
grind

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ g • z = z ↔ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) ^ 2 = -(↑g).det / ↑g 1 0 ^ 2

Tactic:
rw [Matrix.trace_fin_two, ← eq_neg_iff_add_eq_zero] at htrace

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 ≠ 0
⊢ g • z = z ↔ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) ^ 2 = -(↑g).det / ↑g 1 0 ^ 2
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 ≠ 0
⊢ -(↑g 1 1 * z.re) + ↑g 0 1 = z.re * (z.re * ↑g 1 0 + ↑g 1 1) + ↑g 1 0 * z.im ^ 2 ↔
    (z.re * ↑g 1 0 + ↑g 1 1) ^ 2 + ↑g 1 0 ^ 2 * z.im ^ 2 = ↑g 1 0 * ↑g 0 1 + ↑g 1 1 ^ 2

Tactic:
grind

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, y • ↑g = ↑g * m) ∧ m.discr = 0 ↔ (¬∃ y, (diagonal fun x ↦ y) = m) ∧ m.discr = 0

Tactic:
smul_eq_mul_diagonal,

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
h : 0 < (↑g).det
⊢ ↑(↑g 0 0) * ↑z + ↑(↑g 0 1) = ↑z * (↑(↑g 1 0) * ↑z + ↑(↑g 1 1)) ↔
    ↑(↑g 1 0) * (↑z * ↑z) + (↑(↑g 1 1) - ↑(↑g 0 0)) * ↑z + -↑(↑g 0 1) = 0

Tactic:
grind

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

Goal state before:
pp: g : GL (Fin 2) ℝ
h : 0 < (↑g).det
z : ℍ
hc : ↑g 1 0 = 0
hgc : ↑g 1 1 = ↑g 0 0 → ¬0 = ↑g 0 1
hz : z.re * ↑g 0 0 + ↑g 0 1 = z.re * ↑g 1 1 ∧ ↑g 0 0 = ↑g 1 1
⊢ False

Tactic:
grind

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

Goal state before:
pp: g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
⊢ (↑(↑g 1 1) - ↑(↑g 0 0)) ^ 2 + 4 * ↑(↑g 1 0) * ↑(↑g 0 1) =
    (↑(↑g 0 0) + ↑(↑g 1 1)) ^ 2 - 4 * (↑(↑g 0 0) * ↑(↑g 1 1) - ↑(↑g 0 1) * ↑(↑g 1 0))

Tactic:
grind

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℝ
g : SL(2, R)
z : ℍ
⊢ num ((mapGL ℝ) g) ↑z / denom ((mapGL ℝ) g) ↑z =
    (↑((algebraMap R ℝ) (↑g 0 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 0 1))) /
      (↑((algebraMap R ℝ) (↑g 1 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 1 1)))

Tactic:
rfl

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

Goal state before:
pp: S : Set ℍ
⊢ (∃ i, im ⁻¹' Set.Ici i ⊆ S) ↔ ∃ A, ∀ (z : ℍ), A ≤ z.im → z ∈ S

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: case «0».«0»
z : ℂ
⊢ ![z.re, z.im] ((fun i ↦ i) ⟨0, ⋯⟩) = ![![z.re, -z.im], ![z.im, z.re]] ((fun i ↦ i) ⟨0, ⋯⟩) 0

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: case «0».«1»
z : ℂ
⊢ ![z.re, z.im] ((fun i ↦ i) ⟨1, ⋯⟩) = ![![z.re, -z.im], ![z.im, z.re]] ((fun i ↦ i) ⟨1, ⋯⟩) 0

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: case «0»
z : ℂ
i : Fin 2
⊢ ![z.re * re 1 - z.im * im 1, z.re * im 1 + z.im * re 1] i = ![![z.re, -z.im], ![z.im, z.re]] i 0

Tactic:
simp only [one_re, mul_one, one_im, mul_zero,
      sub_zero, zero_add]
    fin_cases i <;> rfl

Goal state after:
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: case «1».«0»
z : ℂ
⊢ ![-z.im, z.re] ((fun i ↦ i) ⟨0, ⋯⟩) = ![![z.re, -z.im], ![z.im, z.re]] ((fun i ↦ i) ⟨0, ⋯⟩) 1

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: case «1».«1»
z : ℂ
⊢ ![-z.im, z.re] ((fun i ↦ i) ⟨1, ⋯⟩) = ![![z.re, -z.im], ![z.im, z.re]] ((fun i ↦ i) ⟨1, ⋯⟩) 1

Tactic:
rfl

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

Goal state before:
pp: case h
a b c d : ℝ
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
h : ↑a * ↑d - ↑b * ↑c = 1
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:

Tactic:
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 _

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

Goal state before:
pp: f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ {z | 0 < z.im} ⊆ {z | 0 ≤ z.im}

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
A : Type u_6
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
a : A
⊢ LinearMap.det (↑R ((lmul S A) a)) = LinearMap.det ((lmul R A) a)

Tactic:
rfl

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

Goal state before:
pp: f g : ℍ → ℂ
hf : MDiff f
hg : MDiff g
⊢ f = 0 ∨ g = 0 → f * g = 0

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : IsIntegral K x
⊢ 1 = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

pp: case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ 1 = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
· have h₁ : ¬ FiniteDimensional K⟮x⟯ L := fun H ↦ h <| by
        have : FiniteDimensional K K⟮x⟯ := adjoin.finiteDimensional hx
        exact Finite.trans K⟮x⟯ L
      simp [finrank_of_not_finite h₁]

Goal state after:
case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ 1 = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

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

Tactic:
by
  rw [dist_eq, mul_div_cancel_left₀ (arsinh _) two_ne_zero, sinh_arsinh]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ Tendsto (fun x ↦ dist c (inversion c R x)) (𝓝[≠] c) atTop

Tactic:
have hdist : Tendsto (dist c) (𝓝[≠] c) (𝓝[>] (0 : ℝ)) := by
    rw [tendsto_nhdsWithin_iff]
    refine ⟨tendsto_nhdsWithin_of_tendsto_nhds ?_, eventually_nhdsWithin_of_forall ?_⟩
    · rw [← dist_self c]
      exact ContinuousAt.tendsto <| by fun_prop
    · aesop

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
hdist : Tendsto (dist c) (𝓝[≠] c) (𝓝[>] 0)
⊢ Tendsto (fun x ↦ dist c (inversion c R x)) (𝓝[≠] c) atTop
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
H : 2 * z.im * w.im ≠ 0
⊢ dist ↑z ↑(w.center r) ^ 2 = 2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2

Tactic:
simp only [Complex.dist_eq, Complex.sq_norm, normSq_apply, coe_re, coe_im, center_re, center_im,
    cosh_dist', mul_div_cancel₀ _ H, sub_sq z.im, mul_pow, Real.cosh_sq, sub_re, sub_im, mul_sub, ←
    sq]

Goal state after:
z w : ℍ
r : ℝ
H : 2 * z.im * w.im ≠ 0
⊢ (z.re - w.re) ^ 2 + (z.im ^ 2 - 2 * z.im * (w.im * Real.cosh r) + w.im ^ 2 * (Real.sinh r ^ 2 + 1)) =
    (z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2 - 2 * z.im * w.im * Real.cosh r + w.im ^ 2 * Real.sinh r ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ sinh x ≤ 0 ↔ x ≤ 0

Tactic:
simpa only [sinh_zero] using @sinh_le_sinh x 0

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

Goal state before:
pp: z w : ℍ
⊢ dist { coe := { re := 0, im := z.im }, coe_im_pos := ⋯ } { coe := { re := 0, im := w.im }, coe_im_pos := ⋯ } ≤
    dist z w

Tactic:
simp_rw [dist_eq]

Goal state after:
z w : ℍ
⊢ 2 *
      arsinh
        (dist { re := 0, im := z.im } { re := 0, im := w.im } /
          (2 *
            √({ coe := { re := 0, im := z.im }, coe_im_pos := ⋯ }.im *
                { coe := { re := 0, im := w.im }, coe_im_pos := ⋯ }.im))) ≤
    2 * arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))