mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
p : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
x : X
e : ↑(p ⁻¹' {x})
⊢ (hp.fundamentalGroupToMulOpposite e).ker = (⋯.monodromyPerm x).ker

Tactic:
ext; simp [fundamentalGroupToMulOpposite_eq_one_iff, DFunLike.ext'_iff, ← hp.monodromy_eq_id_iff]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
z : ℂ
hz : z.re = 0
⊢ ↑l + z * (↑u - ↑l) ∈ re ⁻¹' {l}

Tactic:
simp [hz]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
z : ℂ
hz : z.re = 1
⊢ ↑l + z * (↑u - ↑l) ∈ re ⁻¹' {u}

Tactic:
simp [hz]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ sSupNormIm f 1 ≤ b

Tactic:
· rw [sSupNormIm]
      apply csSup_le _
      · simpa [comp_apply, mem_image, forall_exists_index,
          and_imp, forall_apply_eq_imp_iff₂] using hb
      · use ‖(f 1)‖, 1
        simp only [mem_preimage, one_re, mem_singleton_iff, comp_apply,
          and_self]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f (↑x + ↑c.im * I)
I₂ : E := I • ∫ (y : ℝ) in c.im..w.im, f (↑w.re + ↑y * I)
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f (↑x + ↑c.im * I)
I₄ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑z.re + ↑y * I)
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₆ : E := I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑c.im * I)
I₈ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑w.re + ↑y * I)
z_ball : ball z (r - dist z c) ⊆ ball c r
w_mem : w ∈ ball c r
integrableHoriz :
  ∀ (a₁ a₂ b : ℝ),
    ↑a₁ + ↑b * I ∈ ball c r → ↑a₂ + ↑b * I ∈ ball c r → IntervalIntegrable (fun x ↦ f (↑x + ↑b * I)) volume a₁ a₂
integrableVert :
  ∀ (a b₁ b₂ : ℝ),
    ↑a + ↑b₁ * I ∈ ball c r → ↑a + ↑b₂ * I ∈ ball c r → IntervalIntegrable (fun y ↦ f (↑a + ↑y * I)) volume b₁ b₂
hI₁ : I₁ = I₃ + I₇
hI₂ : I₂ = I₈ + I₆
wzInBall : ↑w.re + ↑z.im * I ∈ ball c r
wcInBall : ↑w.re + ↑c.im * I ∈ ball c r
hU : (↑z.re + ↑c.im * I).Rectangle (↑w.re + ↑z.im * I) ⊆ ball c r
⊢ I₇ - I₅ + I₈ - I₄ = 0

Tactic:
simpa [← add_eq_zero_iff_eq_neg, wedgeIntegral_add_wedgeIntegral_eq] using
      hf (z.re + c.im * I) (w.re + z.im * I) hU

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
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun x ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
c : ℝ
hc : c < π / (b - a)
B : ℝ
hO : f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.im|))
this :
  Tendsto (fun x ↦ x * -I) (comap (fun x ↦ |x.re|) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b))
    (comap (fun x ↦ |x.im|) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b))
⊢ (fun z ↦ f (z * -I)) =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|))

Tactic:
simpa [Function.comp_def] using hO.comp_tendsto this

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

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

Tactic:
fderiv_clm_apply (by fun_prop) (by fun_prop),

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

Goal state before:
pp: case inr.refine_1
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
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
⊢ ∃ c < π / (π / 2 - 0),
    ∃ B, (f ∘ cexp) =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))] fun z ↦ expR (B * expR (c * |z.re|))

Tactic:
rw [sub_zero, div_div_cancel₀ Real.pi_pos.ne']
    rcases hB with ⟨c, hc, B, hO⟩
    refine ⟨c, hc, max B 0, ?_⟩
    rw [← comap_comap, comap_abs_atTop, comap_sup, inf_sup_right]
    -- We prove separately the estimates as `ζ.re → ∞` and as `ζ.re → -∞`
    refine IsBigO.sup ?_ <| (hO.comp_tendsto <| tendsto_exp_comap_re_atTop.inf H.tendsto).trans <|
      .of_norm_eventuallyLE ?_
    · -- For the estimate as `ζ.re → -∞`, note that `f` is continuous within the first quadrant at
      -- zero, hence `f (exp ζ)` has a limit as `ζ.re → -∞`, `0 < ζ.im < π / 2`.
      have hc : ContinuousWithinAt f (Ioi 0 ×ℂ Ioi 0) 0 := by
        refine (hd.continuousOn _ ?_).mono subset_closure
        simp [closure_reProdIm, mem_reProdIm]
      refine ((hc.tendsto.comp <| tendsto_exp_comap_re_atBot.inf H.tendsto).isBigO_one ℝ).trans
        (isBigO_of_le _ fun w => ?_)
      rw [norm_one, Real.norm_of_nonneg (Real.exp_pos _).le, Real.one_le_exp_iff]
      positivity
    · -- For the estimate as `ζ.re → ∞`, we reuse the upper estimate on `f`
      simp only [EventuallyLE, eventually_inf_principal, eventually_comap, comp_apply,
        Real.norm_of_nonneg (Real.exp_pos _).le, norm_exp, ← Real.exp_mul, Real.exp_le_exp]
      filter_upwards [eventually_ge_atTop 0] with x hx z hz _
      rw [hz, abs_of_nonneg hx, mul_comm _ c]
      gcongr; apply le_max_left

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: case h
f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun x ↦ c) (Ioo r R)
⊢ r ∈ Iio R ∧ Ioo r R ⊆ Ioc r R

Tactic:
simp_all [Ioo_subset_Ioc_self]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a : E
c : ℂ
R : ℝ
⊢ circleAverage (fun x ↦ a) c R = a

Tactic:
simp only [circleAverage, intervalIntegral.integral_const, ← smul_assoc, sub_zero, smul_eq_mul]
  ring_nf
  simp

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

Goal state before:
pp: a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), IntervalIntegrable (fun x ↦ x ^ r) volume 0 c
⊢ IntervalIntegrable (fun x ↦ x ^ r) volume a b

Tactic:
exact IntervalIntegrable.trans (this a).symm (this b)

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
hfc : ContinuousOn (fun x ↦ f ↑x) (Ici 0)
⊢ ∃ x, 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x‖

Tactic:
by_cases! h₀ : ∀ x : ℝ, 0 ≤ x → f x = 0

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

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.Log.InvLog

Goal state before:
pp: ⊢ (fun x ↦ (log x)⁻¹) =o[atTop] fun x ↦ 1

Tactic:
by
  rw [isLittleO_one_iff]
  convert tendsto_log_atTop.inv_tendsto_atTop; simp

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

Goal state before:
pp: ⊢ ¬ContinuousAt (fun x ↦ log (log x)) 1

Tactic:
by
  suffices Tendsto (fun x ↦ log (log x)) (nhdsWithin 1 {1}ᶜ) (cobounded ℝ) from
    not_continuousAt_of_tendsto this nhdsWithin_le_nhds (disjoint_nhds_cobounded _)
  exact (tendsto_log_nhdsNE_zero.mono_right atBot_le_cobounded).comp <| log_one ▸
    HasDerivAt.tendsto_nhdsNE (by simpa using hasDerivAt_log one_ne_zero) one_ne_zero

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

Goal state before:
pp: a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), IntervalIntegrable (fun x ↦ ↑x ^ r) volume 0 c
⊢ IntervalIntegrable (fun x ↦ ↑x ^ r) volume a b

Tactic:
exact IntervalIntegrable.trans (this a).symm (this b)

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

Goal state before:
pp: case hst
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
⊢ (fun x ↦ x ^ r.re) x = (fun t ↦ ‖↑t ^ r‖) x

Tactic:
dsimp only

Goal state after:
case hst
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
⊢ x ^ r.re = ‖↑x ^ r‖
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case inr
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x ↦ Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Ioc 0 (-c)) volume
x : ℝ
hx : x ∈ Ioc 0 (-c)
⊢ (fun x ↦ Complex.exp (↑π * Complex.I * r) * ↑x ^ r) x = ↑(-x) ^ r

Tactic:
dsimp only

Goal state after:
case inr
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (fun x ↦ Complex.exp (↑π * Complex.I * r) * ↑x ^ r) (Ioc 0 (-c)) volume
x : ℝ
hx : x ∈ Ioc 0 (-c)
⊢ Complex.exp (↑π * Complex.I * r) * ↑x ^ r = ↑(-x) ^ r
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

Tactic:
have := @integral_pow a b 1

Goal state after:
a b : ℝ
this : ∫ (x : ℝ) in a..b, x ^ 1 = (b ^ (1 + 1) - a ^ (1 + 1)) / (↑1 + 1)
⊢ ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
z : ℂ
hz : ‖z‖ = 1
this : z ≠ 0
⊢ ‖z - a‖ = ‖z⁻¹ * (z - a)‖

Tactic:
simp [hz]

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

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

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

Goal state after:
⊢ π * (log 2 + log 2) + 2 * (-log 2 * π) = 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b c : ℝ
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, (c ^ 2)⁻¹ * (1 + (x / c) ^ 2)⁻¹ = c⁻¹ * (arctan (b / c) - arctan (a / c))

Tactic:
simp [integral_comp_div (fun x => (c ^ 2)⁻¹ * (1 + x ^ 2)⁻¹) hc]
    field_simp

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)
hR : 0 ≤ R
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖) c R

Tactic:
by
  rw [← abs_of_nonneg hR] at hf
  exact hf.circleIntegrable_posLog_norm

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

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 < ‖circleMap 0 r θ‖ - ‖w‖

Tactic:
all_goals simp only [norm_circleMap_zero, abs_of_pos hr]; grind

Goal state after:
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:
by
  apply (tendsto_nhdsWithin_of_tendsto_nhds hcts.tendsto).congr'
  filter_upwards [self_mem_nhdsWithin] with a using cuspFunction_eq_of_nonzero h f

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 ℂ) (eval z (derivative P) / eval z P) = 0

Tactic:
simp [hz]

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
⊢ ∀ z ∈ U, f z ≠ 0

Tactic:
intro z hz hfz

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
z : ℂ
hz : z ∈ U
hfz : f z = 0
⊢ False
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
⊢ f '' U ∈ 𝓝 (f x)

Tactic:
rw [← (hdf x hx).map_nhds_eq (by simpa using hf₀ x hx)]

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
⊢ f '' U ∈ map f (𝓝 x)
Module: Mathlib.Analysis.Complex.SummableUniformlyOn

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
h : SummableLocallyUniformlyOn f s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
⊢ DifferentiableOn ℂ (fun z ↦ ∑' (n : ι), f n z) s

Tactic:
obtain ⟨g, hg⟩ := h

Goal state after:
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
⊢ DifferentiableOn ℂ (fun z ↦ ∑' (n : ι), f n z) s
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case h₂f
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‖
⊢ ∀ x ∈ sphere c |R|, Real.log ‖f x‖ ≤ Real.log M

Tactic:
· peel f_bound with z hz _
      obtain (h | h) := eq_zero_or_norm_pos (f z)
      · simpa [h] using log_nonneg hM
      · gcongr

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

Goal state before:
pp: case h
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
hR : ∀ (r : Rˣ), ∃ k, k ^ Fintype.card n = r
g : GL n R
r : Rˣ
hr : (↑r • ↑g).det = 1
⊢ ↑(toGL ⟨↑r • ↑g, hr⟩ * (GeneralLinearGroup.scalar n) r⁻¹) = ↑g

Tactic:
simp only [Units.val_mul, coe_GL_coe_matrix, GeneralLinearGroup.coe_scalar]

Goal state after:
case h
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
hR : ∀ (r : Rˣ), ∃ k, k ^ Fintype.card n = r
g : GL n R
r : Rˣ
hr : (↑r • ↑g).det = 1
⊢ ↑r • ↑g * (scalar n) ↑r⁻¹ = ↑g
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✝² : Nonempty n
F : Type u_3
inst✝¹ : Field F
inst✝ : IsAlgClosed F
r : Fˣ
⊢ (X ^ Fintype.card n - C ↑r).degree ≠ 0

Tactic:
by
    simp [Polynomial.degree_X_pow_sub_C Fintype.card_pos]

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

Goal state before:
pp: z : ℍ
⊢ z.toSL2R • I = z

Tactic:
by
  have : √z.im ≠ (0 : ℂ) := by simpa [Real.sqrt_ne_zero'] using z.im_pos
  ext
  suffices z.re / √z.im + √z.im * Complex.I = z * (↑√z.im)⁻¹ by
    rw [coe_specialLinearGroup_apply, div_eq_iff (mod_cast denom_ne_zero z.toSL2R I)]
    simpa [add_comm]
  rw [div_add' (hc := this), mul_right_comm, ← Complex.ofReal_mul, ← Real.sqrt_mul z.im_pos.le,
    Real.sqrt_mul_self z.im_pos.le, re_add_im, div_eq_mul_inv]

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

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

Tactic:
by
  rw [← sq_eq_sq₀, cosh_sq', sinh_half_dist, div_pow, div_pow, one_add_div, mul_pow, sq_sqrt]
  · congr 1
    simp only [Complex.dist_eq, Complex.sq_norm, Complex.normSq_sub, Complex.normSq_conj,
      Complex.conj_conj, Complex.mul_re, Complex.conj_re, Complex.conj_im, coe_im]
    ring
  all_goals positivity

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

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

Tactic:
rw [dist_eq_iff_eq_sinh, ← sq_eq_sq₀, div_pow, mul_pow, sq_sqrt, 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.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z✝ w : ℍ
r : ℝ
z : ℍ
⊢ 2 * arsinh (0 / (2 * √(z.im * z.im))) = 0

Tactic:
zero_div,

Goal state after:
z✝ w : ℍ
r : ℝ
z : ℍ
⊢ 2 * arsinh 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x✝ : ℂ
⊢ (deriv cosh / cosh) x✝ = tanh x✝

Tactic:
Complex.deriv_cosh,

Goal state after:
x✝ : ℂ
⊢ (sinh / cosh) x✝ = tanh x✝
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ ProperSpace ℍ

Tactic:
by
  refine ⟨fun z r => ?_⟩
  rw [isEmbedding_coe.isCompact_iff (f := ((↑) : ℍ → ℂ)), image_coe_closedBall]
  apply isCompact_closedBall

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
A : Ultrafilter α
⊢ ∀ x ∈ connectedComponent A, x = A

Tactic:
intro B hB

Goal state after:
α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
⊢ B = A
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ t ∈ S, (∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ) ∧ IsOpen[inst✝] (some ⁻¹' t)
this : IsOpen[inst✝] (some ⁻¹' ⋃₀ S)
⊢ (∞ ∈ ⋃₀ S → IsCompact (some ⁻¹' ⋃₀ S)ᶜ) ∧ IsOpen[inst✝] (some ⁻¹' ⋃₀ S)

Tactic:
refine ⟨?_, this⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ t ∈ S, (∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ) ∧ IsOpen[inst✝] (some ⁻¹' t)
this : IsOpen[inst✝] (some ⁻¹' ⋃₀ S)
⊢ ∞ ∈ ⋃₀ S → IsCompact (some ⁻¹' ⋃₀ S)ᶜ
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] (some ⁻¹' (some '' s)ᶜᶜ) ∧ IsCompact (some ⁻¹' (some '' s)ᶜᶜ) ↔ IsClosed[inst✝] s ∧ IsCompact s

pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ ∞ ∈ (some '' s)ᶜ

Tactic:
compl_compl,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] (some ⁻¹' some '' s) ∧ IsCompact (some ⁻¹' some '' s) ↔ IsClosed[inst✝] s ∧ IsCompact s

X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ ∞ ∈ (some '' s)ᶜ
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
⊢ NormalSpace (OnePoint X)

Tactic:
suffices R1Space (OnePoint X) by infer_instance
  have key : ∀ z : X, Disjoint (𝓝 (some z)) (𝓝 ∞) := fun z ↦ by
    rw [nhds_infty_eq, disjoint_sup_right, nhds_coe_eq, coclosedCompact_eq_cocompact,
      disjoint_map coe_injective, ← principal_singleton, disjoint_principal_right, compl_infty]
    exact ⟨disjoint_nhds_cocompact z, range_mem_map⟩
  refine ⟨fun x y ↦ ?_⟩
  induction x using OnePoint.rec <;> induction y using OnePoint.rec
  · exact .inl le_rfl
  · exact .inr (key _).symm
  · exact .inr (key _)
  · rw [nhds_coe_eq, nhds_coe_eq, disjoint_map coe_injective, specializes_coe]
    apply specializes_or_disjoint_nhds

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case infty
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
s : Set (OnePoint X✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
y : OnePoint X
x✝¹ : y ∈ univ
x✝ : ∞ ∈ univ
hxy : ∞ ≠ y
⊢ ∃ u v, IsOpen[instTopologicalSpace] u ∧ IsOpen[instTopologicalSpace] v ∧ ∞ ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
refine ⟨{y}ᶜ, {y}, isOpen_compl_singleton, ?_, hxy, rfl, (compl_union_self _).symm.subset,
        disjoint_compl_left⟩

Goal state after:
case infty
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
s : Set (OnePoint X✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
y : OnePoint X
x✝¹ : y ∈ univ
x✝ : ∞ ∈ univ
hxy : ∞ ≠ y
⊢ IsOpen[instTopologicalSpace] {y}
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ characteristic f ⊤ - characteristic f⁻¹ ⊤ = proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤)

Tactic:
unfold characteristic
    ring

Goal state after: