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 : ℂ
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 : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
⊢ ‖f z‖ ≤ C

Tactic:
suffices ∀ᶠ ε : ℝ in 𝓝[<] 0, ‖exp (ε * z) • f z‖ ≤ C by
    refine le_of_tendsto (Tendsto.mono_left ?_ nhdsWithin_le_nhds) this
    exact Continuous.tendsto' (by fun_prop) _ _ (by simp)
  filter_upwards [self_mem_nhdsWithin] with ε ε₀; change ε < 0 at ε₀
  set g : ℂ → E := fun z => exp (ε * z) • f z; change ‖g z‖ ≤ C
  replace hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re} :=
    (differentiable_id.const_mul _).cexp.diffContOnCl.smul hd
  have hgn : ∀ z, ‖g z‖ = expR (ε * z.re) * ‖f z‖ := fun z ↦ by
    rw [norm_smul, norm_exp, re_ofReal_mul]
  refine right_half_plane_of_tendsto_zero_on_real hd ?_ ?_ (fun y => ?_) hz
  · rcases hexp with ⟨c, hc, B, hO⟩
    refine ⟨c, hc, B, .trans (.of_bound' ?_) hO⟩
    refine eventually_inf_principal.2 <| Eventually.of_forall fun z hz => ?_
    rw [hgn]
    refine mul_le_of_le_one_left (norm_nonneg _) (Real.exp_le_one_iff.2 ?_)
    exact mul_nonpos_of_nonpos_of_nonneg ε₀.le (le_of_lt hz)
  · simp_rw [g, ← ofReal_mul, ← ofReal_exp, coe_smul]
    have h₀ : Tendsto (fun x : ℝ => expR (ε * x)) atTop (𝓝 0) :=
      Real.tendsto_exp_atBot.comp (tendsto_const_nhds.neg_mul_atTop ε₀ tendsto_id)
    exact h₀.zero_smul_isBoundedUnder_le hre
  · rw [hgn, re_ofReal_mul, I_re, mul_zero, mul_zero, Real.exp_zero,
      one_mul]
    exact him y

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

Goal state before:
pp: a b : ℝ
⊢ (∫ (x : ℝ) in a..0, log x) + ∫ (x : ℝ) in 0..b, log x = b * log b - a * log a - b + a

Tactic:
rw [intervalIntegral.integral_symm, integral_log_from_zero, integral_log_from_zero]

Goal state after:
a b : ℝ
⊢ -(a * log a - a) + (b * log b - b) = b * log b - a * log a - b + a
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hcts : ContinuousAt (cuspFunction h f) 0
⊢ Tendsto (fun x ↦ f (invQParam h x)) (𝓝[≠] 0) (𝓝 (cuspFunction h f 0))

Tactic:
apply (tendsto_nhdsWithin_of_tendsto_nhds hcts.tendsto).congr'

Goal state after:
h : ℝ
f : ℂ → ℂ
hcts : ContinuousAt (cuspFunction h f) 0
⊢ cuspFunction h f =ᶠ[𝓝[≠] 0] fun x ↦ f (invQParam h x)
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: z : ℂ
hP : 0 < degree 0
⊢ False

Tactic:
simp at hP

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

Goal state before:
pp: a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ m * (1 - u ^ 2) ^ n
⊢ ∫ (x : ℝ) in a..b, sin x ^ m * cos x ^ (2 * n + 1) = ∫ (x : ℝ) in a..b, sin x ^ m * (1 - sin x ^ 2) ^ n * cos x

Tactic:
simp only [_root_.pow_zero, _root_.pow_succ, mul_assoc, pow_mul, one_mul]
      congr! 5
      rw [← sq, ← sq, cos_sq']

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

Goal state before:
pp: case e'_5
c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
n : ℕ
⊢ (↑n !)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n !)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c)

Tactic:
mul_assoc

Goal state after:
case e'_5
c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
n : ℕ
⊢ (↑n !)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c) = (↑n !)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c)
Module: Mathlib.Analysis.Complex.TaylorSeries

Goal state before:
pp: case e'_5
c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
n : ℕ
⊢ (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c

Tactic:
rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]

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

Goal state before:
pp: case e'_5
c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ Metric.eball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.eball c r)
n : ℕ
⊢ (↑n !)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n !)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c)

Tactic:
mul_assoc

Goal state after:
case e'_5
c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ Metric.eball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.eball c r)
n : ℕ
⊢ (↑n !)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c) = (↑n !)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c)
Module: Mathlib.Analysis.Complex.TaylorSeries

Goal state before:
pp: case e'_5
c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ Metric.eball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.eball c r)
n : ℕ
⊢ (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c

Tactic:
rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]

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

Goal state before:
pp: case e'_5
c z : ℂ
f : ℂ → ℂ
hf : Differentiable ℂ f
n : ℕ
⊢ (↑n !)⁻¹ * (z - c) ^ n * iteratedDeriv n f c = (↑n !)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c)

Tactic:
mul_assoc

Goal state after:
case e'_5
c z : ℂ
f : ℂ → ℂ
hf : Differentiable ℂ f
n : ℕ
⊢ (↑n !)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c) = (↑n !)⁻¹ * ((z - c) ^ n * iteratedDeriv n f c)
Module: Mathlib.Analysis.Complex.TaylorSeries

Goal state before:
pp: case e'_5
c z : ℂ
f : ℂ → ℂ
hf : Differentiable ℂ f
n : ℕ
⊢ (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c

Tactic:
rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
a : ℂ
ha : a ∈ U
b : ℂ
hb : b ∈ U
hab : f b = -f a
⊢ a = b

Tactic:
← hf_inv b,

Goal state after:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
a : ℂ
ha : a ∈ U
b : ℂ
hb : b ∈ U
hab : f b = -f a
⊢ a = (fun x ↦ x ^ 2) (f b)
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
⊢ ∑ᶠ (u : ℂ), ↑(D u) * (log R - log ‖c - u‖) = ∑ᶠ (u : ℂ), ↑(D u) * log (R * ‖c - u‖⁻¹)

Tactic:
refine finsum_congr fun x ↦ ?_

Goal state after:
case neg
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : D c = 0
x : ℂ
⊢ ↑(D x) * (log R - log ‖c - x‖) = ↑(D x) * log (R * ‖c - x‖⁻¹)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case pos
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
⊢ circleAverage (fun x ↦ log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * log (R * ‖c - u‖⁻¹) +
        ↑((divisor f (closedBall c |R|)) c) * log R +
      log ‖meromorphicTrailingCoeffAt f c‖

Tactic:
have h₃f := (divisor f CB).finiteSupport (isCompact_closedBall c |R|)
    -- Extract zeros & poles and compute
    obtain ⟨g, h₁g, h₂g, h₃g⟩ := h₁f.extract_zeros_poles (by simp_all) h₃f
    calc circleAverage (log ‖f ·‖) c R
    _ = circleAverage ((∑ᶠ u, (divisor f CB u * log ‖· - u‖)) + (log ‖g ·‖)) c R := by
      have h₄g := extract_zeros_poles_log h₂g h₃g
      rw [circleAverage_congr_codiscreteWithin (codiscreteWithin_mono sphere_subset_closedBall h₄g)
        hR]
    _ = circleAverage (∑ᶠ u, (divisor f CB u * log ‖· - u‖)) c R + circleAverage (log ‖g ·‖) c R :=
      circleAverage_add (circleIntegrable_log_norm_factorizedRational (divisor f CB))
        ((h₁g.mono sphere_subset_closedBall).meromorphicOn.circleIntegrable_log_norm)
    _ = ∑ᶠ u, divisor f CB u * log R + log ‖g c‖ := by
      simp only [circleAverage_log_norm_factorizedRational, add_right_inj]
      rw [h₁g.circleAverage_log_norm_of_ne_zero]
      exact fun u hu ↦ h₂g ⟨u, hu⟩
    _ = ∑ᶠ u, divisor f CB u * log R
      + (log ‖meromorphicTrailingCoeffAt f c‖ - ∑ᶠ u, divisor f CB u * log ‖c - u‖) := by
      have t₀ : c ∈ CB := by simp [CB]
      have t₁ : AccPt c (𝓟 CB) := by
        apply accPt_iff_frequently_nhdsNE.mpr
        apply compl_notMem
        apply mem_nhdsWithin.mpr
        use ball c |R|
        simpa [hR] using! fun _ ⟨h, _⟩ ↦ ball_subset_closedBall h
      simp [MeromorphicOn.log_norm_meromorphicTrailingCoeffAt_extract_zeros_poles h₃f t₀ t₁
        (h₁f c t₀) (h₁g c t₀) (h₂g ⟨c, t₀⟩) h₃g]
    _ = ∑ᶠ u, divisor f CB u * log R - ∑ᶠ u, divisor f CB u * log ‖c - u‖
      + log ‖meromorphicTrailingCoeffAt f c‖ := by
      ring
    _ = (∑ᶠ u, divisor f CB u * (log R - log ‖c - u‖)) + log ‖meromorphicTrailingCoeffAt f c‖ := by
      rw [← finsum_sub_distrib]
      · simp_rw [← mul_sub]
      repeat apply h₃f.subset (fun _ ↦ (by simp_all))
    _ = ∑ᶠ u, divisor f CB u * log (R * ‖c - u‖⁻¹) + divisor f CB c * log R
      + log ‖meromorphicTrailingCoeffAt f c‖ := by
      rw [countingFunction_finsum_eq_finsum_add hR h₃f]

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

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ 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‖

Tactic:
rw [h₁f.meromorphicOn.circleAverage_log_norm hR, h₁f.divisor_apply (by simp),
    (h₁f c (by simp)).analyticOrderAt_eq_zero.mpr h₂f,
    (h₁f c (by simp)).meromorphicTrailingCoeffAt_of_ne_zero h₂f]

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) +
        ↑(ENat.map Nat.cast 0).untop₀ * Real.log R +
      Real.log ‖f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed[inst✝²] s
Y : Type v
inst✝ : TopologicalSpace Y
f : C(↑s, Y)
t : Set Y
hf : ∀ (x : ↑s), f x ∈ t
ht : TietzeExtension ↑t
g : C(X, ↑t)
hg : restrict s g = { toFun := Set.codRestrict (⇑f) t hf, continuous_toFun := ⋯ }
x : ↑s
⊢ (restrict s ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp g)) x = f x

Tactic:
congrm(($(hg) x : Y))

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X₁ : Type u₁
inst✝³ : TopologicalSpace X₁
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
e : X₁ → X
he : IsClosedEmbedding e
Y : Type v
inst✝ : TopologicalSpace Y
f : C(X₁, Y)
t : Set Y
hf : ∀ (x : X₁), f x ∈ t
ht : TietzeExtension ↑t
g : C(X, ↑t)
hg : g.comp { toFun := e, continuous_toFun := ⋯ } = { toFun := Set.codRestrict (⇑f) t hf, continuous_toFun := ⋯ }
x : X₁
⊢ (({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp g).comp { toFun := e, continuous_toFun := ⋯ }) x = f x

Tactic:
congrm(($(hg) x : Y))

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:
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 : ℍ
⊢ 0 < (smulAux' g ↑z).im

Tactic:
smulAux'_im

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
⊢ 0 < |↑(GeneralLinearGroup.det g)| * (↑z).im / Complex.normSq (denom g ↑z)
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case succ
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)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ dist ((F (f - (g n).compContinuous e)).compContinuous e) (f - (g n).compContinuous e) ≤ 2 / 3 * (2 / 3) ^ n * ‖f‖

Tactic:
mul_assoc

Goal state after:
case succ
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)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ dist ((F (f - (g n).compContinuous e)).compContinuous e) (f - (g n).compContinuous e) ≤ 2 / 3 * ((2 / 3) ^ n * ‖f‖)
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case succ
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)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ dist ((F (f - (g n).compContinuous e)).compContinuous e) (f - (g n).compContinuous e) ≤ 2 / 3 * ((2 / 3) ^ n * ‖f‖)

Tactic:
refine (hF_dist _).trans (mul_le_mul_of_nonneg_left ?_ (by norm_num1))

Goal state after:
case succ
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)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ ‖f - (g n).compContinuous e‖ ≤ (2 / 3) ^ n * ‖f‖
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
hpos : 0 < (↑g).det
hell : g.IsElliptic
⊢ g • z = z ↔ z = fixedPt g hell

Tactic:
wlog hc : 0 < g 1 0 generalizing g
  · replace hc := hell.c_ne_zero.lt_or_gt.resolve_right hc
    simpa using @this (-g) (by simpa [Matrix.det_neg]) hell.neg (by simpa)
  have hd : discrim (g 1 0 : ℂ) (g 1 1 - g 0 0) (-g 0 1) = (.I * √(-g.val.discr)) ^ 2 := by
    rw [mul_pow, ← Complex.ofReal_pow, Real.sq_sqrt]
    · simp [discrim, Matrix.discr_fin_two, Matrix.trace_fin_two, Matrix.det_fin_two]
      grind
    · simpa using hell.le
  rw [gl_smul_eq_self_iff_quadratic hpos, quadratic_eq_zero_iff (mod_cast hell.c_ne_zero)
    (hd.trans (pow_two _))]
  rw [or_iff_left]
  · simp [fixedPt, UpperHalfPlane.ext_iff, abs_of_pos hc, field]
  · intro h
    refine z.im_pos.not_ge ?_
    rw [← coe_im, h]
    simp [Complex.div_im, div_nonpos_iff, hc.le, mul_nonneg]

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
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‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
⊢ (atTop.limUnder g).compContinuous e = f

Tactic:
refine tendsto_nhds_unique this (tendsto_iff_dist_tendsto_zero.2 ?_)

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‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
⊢ Tendsto (fun b ↦ dist ((g b).compContinuous e) f) atTop (𝓝 0)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
⊢ ∏ i ∈ s, f i = 0 ↔ ∃ i ∈ s, f i = 0

Tactic:
by
  refine ⟨fun h0 ↦ ?_, fun ⟨i, hi, hi'⟩ ↦ Finset.prod_eq_zero hi hi'⟩
  have : ∃ᶠ τ in 𝓝[≠] I, ∏ i ∈ s, f i τ = 0 := .of_forall <| by simpa using congrFun h0
  simp only [Finset.prod_eq_zero_iff, Finset.frequently_exists] at this
  exact this.imp fun i hi ↦ ⟨hi.1, eq_zero_of_frequently (hf i hi.1) hi.2⟩

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

Goal state before:
pp: case inr
g : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g).det
⊢ (↑↑(if 0 < ↑(Matrix.GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) ∘SL
        ContinuousLinearMap.restrictScalars ℝ
          (ContinuousLinearMap.toSpanSingleton ℂ (↑↑(Matrix.GeneralLinearGroup.det g) / denom g z ^ 2))).det =
    ↑(SignType.sign ↑(Matrix.GeneralLinearGroup.det g)) * ↑(Matrix.GeneralLinearGroup.det g) ^ 2 / ‖denom g z‖ ^ 4

Tactic:
· simp [ContinuousLinearMap.det, h, LinearMap.det_restrictScalars,
      Algebra.norm_complex_eq, Complex.normSq_eq_norm_sq, ← pow_mul]

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

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
⊢ dist b c * dist b d ≤ dist b b * dist c d + dist b c * dist b d

Tactic:
rw [dist_self, zero_mul, zero_add]

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

Goal state before:
pp: z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ dist ↑z ↑w ^ 2 / (2 ^ 2 * (z.im * w.im)) = sinh (r / 2) ^ 2 ↔ dist ↑z ↑w ^ 2 / (4 * z.im * w.im) = sinh (r / 2) ^ 2

pp: z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ z.im * w.im

pp: case ha
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ dist ↑z ↑w / (2 * √(z.im * w.im))

pp: case hb
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ sinh (r / 2)

Tactic:
mul_assoc

Goal state after:
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ dist ↑z ↑w ^ 2 / (2 ^ 2 * (z.im * w.im)) = sinh (r / 2) ^ 2 ↔ dist ↑z ↑w ^ 2 / (4 * (z.im * w.im)) = sinh (r / 2) ^ 2

z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ z.im * w.im

case ha
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ dist ↑z ↑w / (2 * √(z.im * w.im))

case hb
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ sinh (r / 2)
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
s : Set G
t : Set X
hs : IsClosed[inst✝²] s
ht : IsCompact t
Ψ : G × ↑t → X × ↑t := fun gx ↦ (gx.1 • ↑gx.2, gx.2)
Ψ_proper : IsProperMap Ψ
this✝ : s • t = fst ∘ Ψ '' fst ⁻¹' s
this : CompactSpace ↑t
⊢ IsClosed[inst✝¹] (fst ∘ Ψ '' fst ⁻¹' s)

Tactic:
exact (isProperMap_fst_of_compactSpace.comp Ψ_proper).isClosedMap _ (hs.preimage continuous_fst)

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

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := ⟨!![0, -1; 1, 0], ⋯⟩
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ S • K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A
g : SL(2, ℝ)
hg : g • I ∈ K
⊢ ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 = ↑(S * g) 1 0 ^ 2 + ↑(S * g) 1 1 ^ 2

Tactic:
rw [Matrix.SpecialLinearGroup.coe_mul, Matrix.eta_fin_two g.val, Matrix.mul_fin_two]

Goal state after:
K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := ⟨!![0, -1; 1, 0], ⋯⟩
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ S • K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A
g : SL(2, ℝ)
hg : g • I ∈ K
⊢ !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] 0 0 ^ 2 + !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] 0 1 ^ 2 =
    !![0 * ↑g 0 0 + -1 * ↑g 1 0, 0 * ↑g 0 1 + -1 * ↑g 1 1; 1 * ↑g 0 0 + 0 * ↑g 1 0, 1 * ↑g 0 1 + 0 * ↑g 1 1] 1 0 ^ 2 +
      !![0 * ↑g 0 0 + -1 * ↑g 1 0, 0 * ↑g 0 1 + -1 * ↑g 1 1; 1 * ↑g 0 0 + 0 * ↑g 1 0, 1 * ↑g 0 1 + 0 * ↑g 1 1] 1 1 ^ 2
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ |(proximity f ⊤ - proximity (fun x ↦ f x - a₀) ⊤) r| ≤ log⁺ ‖a₀‖ + log 2

Tactic:
simp only [proximity, reduceDIte, Pi.sub_apply, ← circleAverage_sub h₁f h₂f]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ |circleAverage ((fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x - a₀‖) 0 r| ≤ log⁺ ‖a₀‖ + log 2
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case refl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx hy : x ∈ s
⊢ eVariationOn f (s ∩ Icc x x) = ENNReal.ofReal (↑l * (x - x))

Tactic:
rw [eVariationOn.subsingleton f (fun y hy z hz => hs hy.1 hz.1 : (s ∩ Icc x x).Subsingleton)]

Goal state after:
case refl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx hy : x ∈ s
⊢ 0 = ENNReal.ofReal (↑l * (x - x))
Module: Mathlib.Topology.Semicontinuity.Lindelof

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (X → E) → E → Set X := fun f d ↦ {x | f x < d}
U_open : ∀ {f : X → E}, f ∈ 𝓕 → ∀ (d : E), IsOpen (U f d)
this✝ : ∀ (d : E), {x | s x < d} = ⋃ f, U (↑f) d
this : ∀ (d : E), ∃ A ⊆ 𝓕, A.Countable ∧ {x | s x < d} = ⋃ f ∈ A, U f d
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval a '' 𝓕') (s a)

Tactic:
choose A A_sub A_count hA using this

Goal state after:
X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (X → E) → E → Set X := fun f d ↦ {x | f x < d}
U_open : ∀ {f : X → E}, f ∈ 𝓕 → ∀ (d : E), IsOpen (U f d)
this : ∀ (d : E), {x | s x < d} = ⋃ f, U (↑f) d
A : E → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), {x | s x < d} = ⋃ f ∈ A d, U f d
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval a '' 𝓕') (s a)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case empty
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
α : Type u_3
f : α → 𝕜 → E
r : ℝ
hr : 1 ≤ r
h₁f : ∀ a ∈ ∅, Meromorphic (f a)
⊢ logCounting (∑ a ∈ ∅, f a) ⊤ r ≤ (∑ a ∈ ∅, logCounting (f a) ⊤) r

Tactic:
| empty =>

Goal state after: