mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case refine_1
R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ MeromorphicNFAt (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w

pp: case refine_2
R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ ↑R ^ 2 - (starRingEnd ℂ) w * w ≠ 0

Tactic:
· apply AnalyticAt.meromorphicNFAt
      fun_prop

Goal state after:
case refine_2
R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ ↑R ^ 2 - (starRingEnd ℂ) w * w ≠ 0
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
η₁ : AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x
η₀ : f =ᶠ[𝓝[≠] x] (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g
a : ℂ
ha : a ∈ ball 0 R
⊢ (canonicalFactor R a ^ (-(divisor f (ball 0 R)) a)) x ≠ 0

Tactic:
exact zpow_ne_zero _ (canonicalFactor_ne_zero ha (by aesop) (by aesop))

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
x : ℂ
hx : x ∈ t₁
⊢ ‖w - x‖ ^ (-divisor f S₀R) x ≠ 0

Tactic:
refine zpow_ne_zero _ ?_

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
x : ℂ
hx : x ∈ t₁
⊢ ‖w - x‖ ≠ 0
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
η₀ : ∀ x ∈ t₁, ‖w - x‖ ^ (-divisor f S₀R) x ≠ 0
x : ℂ
hx : x ∈ t₂
⊢ ‖canonicalFactor R x w‖ ^ (divisor f B₀R) x ≠ 0

Tactic:
refine zpow_ne_zero _ ?_

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
η₀ : ∀ x ∈ t₁, ‖w - x‖ ^ (-divisor f S₀R) x ≠ 0
x : ℂ
hx : x ∈ t₂
⊢ ‖canonicalFactor R x w‖ ≠ 0
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
e₀ : E
f : C(A, ↑s)
he : p e₀ = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a₀
hs : ∀ (a : A), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a ∈ s
⊢ e₀ ∈ p ⁻¹' s

Tactic:
by rw [Set.mem_preimage, he]; apply hs

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
⊢ norm ∘ scale f l u '' verticalClosedStrip 0 1 ⊆ norm ∘ f '' verticalClosedStrip l u

Tactic:
rintro _ ⟨z, hz, rfl⟩

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
⊢ (norm ∘ scale f l u) z ∈ norm ∘ f '' verticalClosedStrip l u
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
h : IsExactOn f s
x₀ : ℂ
y : E
⊢ ∃ g, g x₀ = y ∧ ∀ x ∈ s, HasDerivAt g (f x) x

Tactic:
by
  obtain ⟨η, hη⟩ := h
  use fun z ↦ η z - η x₀ + y, by simp, by simpa using hη

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
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
A : ℝ
hA₀ : A > 0
hA :
  ∀ᶠ (b_1 : ℝ) in atTop,
    ∀ (a_1 : ℂ), |a_1.re| = b_1 → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
H : Tendsto (fun R ↦ δ + B * (expR ((d - c) * R))⁻¹) atTop (𝓝 (δ + B * 0))
⊢ Tendsto (fun R ↦ δ * expR (d * R) + B * expR (c * R) + Real.log A) atTop atBot

Tactic:
rw [mul_zero, add_zero] at H
      refine Tendsto.atBot_add ?_ tendsto_const_nhds
      simpa only [id, (· ∘ ·), add_mul, mul_assoc, ← div_eq_inv_mul, ← Real.exp_sub, ← sub_mul,
        sub_sub_cancel]
        using H.neg_mul_atTop δ₀ <| Real.tendsto_exp_atTop.comp <| tendsto_id.const_mul_atTop hd₀

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ (Δ[s] f₁ - f₂) x = (Δ[s] f₁) x - (Δ[s] f₂) x

Tactic:
by
  simp [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs hx,
    ← Finset.sum_sub_distrib, iteratedFDerivWithin_sub_apply h₁ h₂ hs hx]

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
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
this : ∀ᶠ (w : ℂ) in 𝓝 z, ∀ y ∈ Ι z.im w.im, ‖f (↑w.re + ↑y * I) - f z‖ ≤ ε
⊢ ∀ᶠ (x : ℂ) in 𝓝 z, ‖∫ (y : ℝ) in z.im..x.im, f (↑x.re + ↑y * I) - f z‖ ≤ ε * ‖x - z‖

Tactic:
filter_upwards [this] with w hw

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
this : ∀ᶠ (w : ℂ) in 𝓝 z, ∀ y ∈ Ι z.im w.im, ‖f (↑w.re + ↑y * I) - f z‖ ≤ ε
w : ℂ
hw : ∀ y ∈ Ι z.im w.im, ‖f (↑w.re + ↑y * I) - f z‖ ≤ ε
⊢ ‖∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) - f z‖ ≤ ε * ‖w - z‖
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic (fun θ ↦ f (circleMap c R θ)) (2 * π)
this : ∫ (x : ℝ) in 0..2 * π, f (circleMap c R x) = ∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x)
⊢ circleAverage f c R = (2 * π)⁻¹ • ∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x)

Tactic:
rw [zero_add]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic (fun θ ↦ f (circleMap c R θ)) (2 * π)
this : ∫ (x : ℝ) in 0..2 * π, f (circleMap c R x) = ∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x)
⊢ circleAverage f c R = (2 * π)⁻¹ • ∫ (x : ℝ) in η..2 * π + η, f (circleMap c R x)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
hR : R < 0
⊢ circleAverage f c |R| = circleAverage f c R

Tactic:
· rw [abs_of_neg hR, circleAverage_neg_radius]

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

Goal state before:
pp: R : ℝ
w c z : ℂ
hz : z ∈ sphere c R
hw : w ∈ ball c R
⊢ ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (R + ‖w - c‖) / (R - ‖w - c‖)

Tactic:
by
  obtain ⟨η₀, rfl, η₂⟩ : 0 < R ∧ R = ‖z - c‖ ∧ z - c ≠ 0 := by
    grind [ball_eq_empty, mem_sphere, dist_eq_norm, norm_pos_iff]
  by_cases h₁w : ‖w - c‖ = 0
  · aesop
  simpa using re_herglotzRieszKernel_le_aux (w - c).arg (z - c).arg ‖w - c‖ ‖z - c‖
    (by simpa using h₁w) (mem_ball_iff_norm.1 hw)

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

Goal state before:
pp: θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 1 / (R + r) ≤ (R + r) / ‖↑R * cexp (↑θ * I) - ↑r * cexp (↑φ * I)‖ ^ 2

Tactic:
rw [div_le_div_iff₀ (by positivity [h₁.trans h₂]) ?hpos, ← normSq_eq_norm_sq, normSq_sub,
    normSq_eq_norm_sq, normSq_eq_norm_sq]

Goal state after:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 1 *
      (‖↑R * cexp (↑θ * I)‖ ^ 2 + ‖↑r * cexp (↑φ * I)‖ ^ 2 -
        2 * (↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I))).re) ≤
    (R + r) * (R + r)

case hpos
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 0 < ‖↑R * cexp (↑θ * I) - ↑r * cexp (↑φ * I)‖ ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

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

Tactic:
by
    simp [Finset.sum_const]

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

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

Tactic:
calc log⁺ (∑ t ∈ s, f t)
  _ = log⁺ |∑ t ∈ s, f t| := by
    rw [Real.posLog_abs]
  _ ≤ log⁺ (∑ t ∈ s, |f t|) := by
    apply monotoneOn_posLog (by simp) (by simp [Finset.sum_nonneg])
    simp [Finset.abs_sum_le_sum_abs]
  _ ≤ log⁺ (∑ t ∈ s, |f t_max|) := by
    apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp [mul_nonneg])
    apply Finset.sum_le_sum (fun i ih ↦ ht_max.2 i ih)
  _ = log⁺ (s.card * |f t_max|) := by
    simp [Finset.sum_const]
  _ ≤ log s.card + log⁺ |f t_max| := posLog_nat_mul
  _ ≤ log s.card + ∑ t ∈ s, log⁺ (f t) := by
    gcongr
    rw [posLog_abs]
    apply Finset.single_le_sum (fun _ _ ↦ posLog_nonneg) ht_max.1

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

Goal state before:
pp: case e'_2
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
⊢ MeasureTheory.Integrable (fun x ↦ ↑x ^ ↑r) (MeasureTheory.volume.restrict (Ι a b))

Tactic:
refine intervalIntegrable_iff.mp ?_

Goal state after:
case e'_2
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
⊢ IntervalIntegrable (fun x ↦ ↑x ^ ↑r) MeasureTheory.volume a b
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

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

Tactic:
rw [← intervalIntegral.integral_add_adjacent_intervals (a := 0) (b := π / 2) (c := π)
    (by apply intervalIntegrable_log_sin) (by apply intervalIntegrable_log_sin)]
  conv =>
    left; right; arg 1
    intro x
    rw [← sin_pi_sub]
  rw [intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)), sub_self,
    (by linarith : π - π / 2 = π / 2)]
  ring!

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

Goal state before:
pp: t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
⊢ {x | (fun x ↦ (fun x ↦ log (sin x)) x = (fun x ↦ log (sin (2 * x)) - log 2 - log (cos x)) x) x} ∈
    codiscreteWithin Set.univ

Tactic:
have t₁ : cos ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_cos.preimage_zero_mem_codiscrete (x := 0)
        simp

Goal state after:
t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
t₁ : cos ⁻¹' {0}ᶜ ∈ codiscrete ℝ
⊢ {x | (fun x ↦ (fun x ↦ log (sin x)) x = (fun x ↦ log (sin (2 * x)) - log 2 - log (cos x)) x) x} ∈
    codiscreteWithin Set.univ
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

Goal state before:
pp: ⊢ IntervalIntegrable (fun x ↦ log (sin (2 * x)) - log 2) MeasureTheory.volume 0 (π / 2)

pp: ⊢ IntervalIntegrable (fun x ↦ log (cos x)) MeasureTheory.volume 0 (π / 2)

Tactic:
· apply IntervalIntegrable.sub _ intervalIntegrable_const
        simpa using (intervalIntegrable_log_sin (a := 0) (b := π)).comp_mul_left

Goal state after:
⊢ IntervalIntegrable (fun x ↦ log (cos x)) MeasureTheory.volume 0 (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hb
b : ℝ
ht : 0 < b
⊢ Filter.Tendsto (fun x ↦ x * log x - x) (nhdsWithin b (Set.Iio b)) (nhds (b * log b - b))

Tactic:
· exact tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))

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

Goal state before:
pp: case hg
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 ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : ↑(sphere c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (sphere c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (sphere c |R|)) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    (∑ᶠ (u : ℂ), fun x ↦ ↑((divisor f (sphere c |R|)) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
⊢ CircleIntegrable (fun x ↦ log ‖g x‖) c R

Tactic:
apply ContinuousOn.intervalIntegrable
      apply ContinuousOn.log
      · apply ContinuousOn.norm
        apply h₁g.continuousOn.comp (t := sphere c |R|) (continuous_circleMap c R).continuousOn
        intro x hx
        simp
      · intro x hx
        rw [ne_eq, norm_eq_zero]
        apply h₂g ⟨circleMap c R x, circleMap_mem_sphere' c R x⟩

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

Goal state before:
pp: a b : ℝ
ha : 1 < a
hb : 1 < b
⊢ ∫ (t : ℝ) in a..b, deriv (fun t ↦ (log t)⁻¹) t = (log b)⁻¹ - (log a)⁻¹

Tactic:
refine integral_deriv_eq_sub (fun _ _ ↦ ?_) (ContinuousOn.intervalIntegrable ?_)

Goal state after:
case refine_1
a b : ℝ
ha : 1 < a
hb : 1 < b
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[a, b]]
⊢ DifferentiableAt ℝ (fun t ↦ (log t)⁻¹) x✝¹

case refine_2
a b : ℝ
ha : 1 < a
hb : 1 < b
⊢ ContinuousOn (deriv fun t ↦ (log t)⁻¹) [[a, b]]
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
hh : h ≠ 0
z : ℂ
⊢ ∃ m, ↑h / (2 * ↑π * I) * log (cexp (2 * ↑π * I * z / ↑h)) = z + ↑m * ↑h

Tactic:
obtain ⟨m, hm⟩ := log_exp_exists (2 * ↑π * I * z / ↑h)

Goal state after:
h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * ↑π * I * z / ↑h)) = 2 * ↑π * I * z / ↑h + ↑m * (2 * ↑π * I)
⊢ ∃ m, ↑h / (2 * ↑π * I) * log (cexp (2 * ↑π * I * z / ↑h)) = z + ↑m * ↑h
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
⊢ cuspFunction h f (𝕢 h z) = f z

Tactic:
have : (cuspFunction h f) (𝕢 h z) = f (invQParam h (𝕢 h z)) := by
    rw [cuspFunction, update_of_ne, comp_apply]
    exact exp_ne_zero _

Goal state after:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
this : cuspFunction h f (𝕢 h z) = f (invQParam h (𝕢 h z))
⊢ cuspFunction h f (𝕢 h z) = f z
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ (Polynomial.X ^ n).natDegree ≠ 0

Tactic:
simpa using NeZero.ne n

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0
a : ℂ
⊢ Tendsto (fun x ↦ f (invQParam h x)) (𝓝[≠] 0) (𝓝 ((𝓝[≠] 0).limUnder (f ∘ invQParam h)))

Tactic:
simpa using! hfcts

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

Goal state before:
pp: case inr
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
this :
  ∀ {U : Set ℂ} (hUo : IsOpen U) (hUc : IsSimplyConnected U) (hU : U ≠ univ),
    0 ∉ U → ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
hU₀ : ¬0 ∉ U
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
ne_univ_iff_exists_notMem

Goal state after:
case inr
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU✝ : U ≠ univ
hU : ∃ a, a ∉ U
this :
  ∀ {U : Set ℂ} (hUo : IsOpen U) (hUc : IsSimplyConnected U) (hU : U ≠ univ),
    0 ∉ U → ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
hU₀ : ¬0 ∉ U
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case hf
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := ⋯
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 : ℕ
⊢ InnerProductSpace.HarmonicContOnCl (fun x ↦ log ‖x - ρ‖) (ball 0 (r n))

pp: case hw
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := ⋯
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 : ℕ
⊢ w ∈ ball 0 (r n)

Tactic:
· refine ⟨fun z hz ↦ ?_, fun x hx ↦ ?_⟩
      · exact AnalyticAt.harmonicAt_log_norm (by fun_prop) (by grind [mem_ball, dist_zero_right])
      · suffices ‖x - ρ‖ ≠ 0 by fun_prop
        suffices x ≠ ρ by simpa [sub_eq_zero]
        have key := by simpa using closure_ball_subset_closedBall hx
        grind

Goal state after:
case hw
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := ⋯
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 : ℕ
⊢ w ∈ ball 0 (r n)
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, (∀ (x : X), g x ∈ t) ∧ restrict s g = f

Tactic:
obtain ⟨g, hg⟩ := mk _ (map_continuous f |>.codRestrict hf) |>.exists_restrict_eq hs
  exact ⟨comp ⟨Subtype.val, by fun_prop⟩ g, by simp, by ext x; congrm(($(hg) x : Y))⟩

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
g : GL n R
⊢ (lift f hf) (mk g) = f g

Tactic:
by
  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:
by
  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:
by
  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:
by
  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:
by
  rfl

Goal state after:
Module: Mathlib.Topology.TietzeExtension

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

Tactic:
simp [g0]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Preorder R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ ((↑g)⁻¹ * m * ↑g).IsHyperbolic ↔ m.IsHyperbolic

Tactic:
by
  simpa using isHyperbolic_conj_iff g⁻¹

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

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

Tactic:
simp_rw [← f.mapMatrix_apply, ← compRingEquiv_apply, map_mul, det_mul, f.mapMatrix_apply,
      compRingEquiv_apply, ((auxMat_blockTriangular M k).map f).comp.det_fintype, Fintype.prod_Prop,
      comp_toSquareBlock (b := (· ≠ k)), det_reindex_self, map_toSquareBlock,
      auxMat_toSquareBlock_eq, auxMat_toSquareBlock_ne, smul_one_eq_diagonal, ← diagonal_one,
      diagonal_map (map_zero _), comp_diagonal, det_reindex_self]

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det * ((blockDiagonal fun m ↦ f (M k k)).det * (blockDiagonal fun m ↦ f 1).det)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case refine_1
n : ℕ∞ω
f : ℍ → ℂ
τ : ℍ
hf : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ ↑ofComplex) ↑τ

Tactic:
exact (ofComplex_apply τ ▸ hf).comp _ (contMDiffAt_ofComplex τ.im_pos)

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NoncompactSpace X
⊢ DenseRange some

Tactic:
by
  rw [DenseRange, ← compl_infty]
  exact dense_compl_singleton _

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ circleAverage ((fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x‖⁻¹) 0 R =
    circleAverage (fun x ↦ log⁺ ‖f x‖ - log⁺ ‖f x‖⁻¹) 0 R

Tactic:
Pi.sub_def

Goal state after: