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

Goal state before:
pp: ⊢ |rexp 1 -
        expNear 19 1
          ((((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) *
                                                            7 -
                                                          1) *
                                                        8 -
                                                      1) *
                                                    9 -
                                                  1) *
                                                10 -
                                              1) *
                                            11 -
                                          1) *
                                        12 -
                                      1) *
                                    13 -
                                  1) *
                                14 -
                              1) *
                            15 -
                          1) *
                        16 -
                      1) *
                    17 -
                  1) *
                18 -
              1) *
            19)| ≤
    |1| ^ 19 / ↑(Nat.factorial 19) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 * 18 * 19)

Tactic:
refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_

Goal state after:
⊢ |rexp 1 -
        expNear 20 1
          (((((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) *
                                                                7 -
                                                              1) *
                                                            8 -
                                                          1) *
                                                        9 -
                                                      1) *
                                                    10 -
                                                  1) *
                                                11 -
                                              1) *
                                            12 -
                                          1) *
                                        13 -
                                      1) *
                                    14 -
                                  1) *
                                15 -
                              1) *
                            16 -
                          1) *
                        17 -
                      1) *
                    18 -
                  1) *
                19 -
              1) *
            20)| ≤
    |1| ^ 20 / ↑(Nat.factorial 20) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 * 18 * 19 * 20)
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |log 5 - 160943791243 / 100000000000| ≤ (4 / 5) ^ 131 / 5⁻¹ + (1 / 10 ^ 10 - (4 / 5) ^ 131 / 5⁻¹)

Tactic:
have t : |4 / 5| = (4 : ℝ) / 5 := by norm_num

Goal state after:
t : |4 / 5| = 4 / 5
⊢ |log 5 - 160943791243 / 100000000000| ≤ (4 / 5) ^ 131 / 5⁻¹ + (1 / 10 ^ 10 - (4 / 5) ^ 131 / 5⁻¹)
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
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
x : ℂ
hx : x ∈ t₂
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ (divisor f B₀R) x *
      meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ (-(divisor f B₀R) x) =
    1

Tactic:
← zpow_add₀,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
x : ℂ
hx : x ∈ t₂
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ ((divisor f B₀R) x + -(divisor f B₀R) x) = 1

case ha
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
x : ℂ
hx : x ∈ t₂
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ≠ 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
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
x : ℂ
hx : x ∈ t₁
⊢ meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ^ (-divisor f S₀R) x *
      meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ^ (divisor f S₀R) x =
    1

Tactic:
← zpow_add₀,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
x : ℂ
hx : x ∈ t₁
⊢ meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ^ ((-divisor f S₀R) x + (divisor f S₀R) x) = 1

case ha
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
x : ℂ
hx : x ∈ t₁
⊢ meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ≠ 0
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
⊢ cov.monodromy ((Path.Homotopic.Quotient.mk (pγ.map ⋯)).trans (Path.Homotopic.Quotient.mk (pγ'.map ⋯).symm)) ⟨e₀, he⟩ =
    cov.monodromy ((Path.Homotopic.Quotient.mk (pγ'.map ⋯)).trans (Path.Homotopic.Quotient.mk (pγ'.map ⋯).symm))
      ⟨e₀, he⟩

Tactic:
← mk_trans

Goal state after:
case refine_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
⊢ cov.monodromy (Path.Homotopic.Quotient.mk ((pγ.map ⋯).trans (pγ'.map ⋯).symm)) ⟨e₀, he⟩ =
    cov.monodromy (Path.Homotopic.Quotient.mk ((pγ'.map ⋯).trans (pγ'.map ⋯).symm)) ⟨e₀, he⟩
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
s_ball₁ : s ×ℂ {z.im} ⊆ ball z r₁
this : s ×ℂ {z.im} ⊆ ball c r
⊢ ↑x + ↑z.im * I ∈ s ×ℂ {z.im}

Tactic:
simp [mem_reProdIm, hx]

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

Goal state before:
pp: case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ f (↑l + (z - ↑l) / (↑u - ↑l) * (↑u - ↑l)) = e

Tactic:
div_mul_comm,

Goal state after:
case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ f (↑l + (↑u - ↑l) / (↑u - ↑l) * (z - ↑l)) = e
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ f (↑l + (z - ↑l) / (↑u - ↑l) * (↑u - ↑l)) = e

Tactic:
div_mul_comm,

Goal state after:
case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ f (↑l + (↑u - ↑l) / (↑u - ↑l) * (z - ↑l)) = e
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ Tendsto (fun x ↦ ‖f z‖) (𝓝[>] 0) (𝓝 ‖f z‖)

Tactic:
simp only [tendsto_const_nhds_iff]

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

Goal state before:
pp: case neg
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
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re

Tactic:
simp_rw [interpStrip_eq_of_pos f _ (lt_of_le_of_ne (sSupNormIm_nonneg f 0) h0)
        (lt_of_le_of_ne (sSupNormIm_nonneg f 1) h1)]

Goal state after:
case neg
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
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ ‖↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: l u : ℝ
hul : l < u
z : ℂ
⊢ ↑l + (z / (↑u - ↑l) * (↑u - ↑l) - ↑l / (↑u - ↑l) * (↑u - ↑l)) = z

Tactic:
div_mul_comm,

Goal state after:
l u : ℝ
hul : l < u
z : ℂ
⊢ ↑l + ((↑u - ↑l) / (↑u - ↑l) * z - ↑l / (↑u - ↑l) * (↑u - ↑l)) = z
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: l u : ℝ
hul : l < u
z : ℂ
⊢ ↑l + (1 * z - ↑l / (↑u - ↑l) * (↑u - ↑l)) = z

Tactic:
div_mul_comm,

Goal state after:
l u : ℝ
hul : l < u
z : ℂ
⊢ ↑l + (1 * z - (↑u - ↑l) / (↑u - ↑l) * ↑l) = z
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: case mp
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
hf : HarmonicAt f₁ x
⊢ HarmonicAt f₂ x

Tactic:
exact ⟨hf.1.congr_of_eventuallyEq h.symm, (laplacian_congr_nhds h.symm).trans hf.2⟩

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
⊢ IsConservativeOn f U ∧ ContinuousOn f U ↔ DifferentiableOn ℂ f U

Tactic:
refine ⟨fun ⟨hf, hf'⟩ z hz ↦ ?_, fun hf ↦ ⟨hf.isConservativeOn, hf.continuousOn⟩⟩
  obtain ⟨r, h₀, h₁⟩ : ∃ r > 0, ball z r ⊆ U := Metric.isOpen_iff.mp hU z hz
  have : DifferentiableOn ℂ f (ball z r) :=
    (IsConservativeOn.isExactOn_ball (hf'.mono h₁) (hf.mono h₁)).differentiableOn isOpen_ball
  apply (this z (mem_ball_self h₀)).mono_of_mem_nhdsWithin
  exact mem_nhdsWithin.mpr ⟨ball z r, isOpen_ball, mem_ball_self h₀, inter_subset_left⟩

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

Goal state before:
pp: ⊢ Continuous negMulLog

Tactic:
simpa only [negMulLog_eq_neg] using continuous_mul_log.fun_neg

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ -deriv (fun x ↦ x * log x) x = -log x - 1

Tactic:
deriv_mul_log hx

Goal state after:
x : ℝ
hx : x ≠ 0
⊢ -(log x + 1) = -log x - 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: case inr.inr
x : ℝ
hx : 0 < x
⊢ sin x / x ≤ |x|⁻¹

Tactic:
· rw [abs_of_nonneg hx.le, div_eq_mul_inv, mul_inv_le_iff₀ hx, inv_mul_cancel₀ hx.ne']
    exact sin_le_one x

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

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

Tactic:
have : ∀ x : ℝ, x ∈ Ioo c 0 → ‖Complex.exp (↑π * Complex.I * r)‖ = ‖(x : ℂ) ^ r‖ := by
        intro x hx
        rw [Complex.ofReal_cpow_of_nonpos hx.2.le, norm_mul, ← Complex.ofReal_neg,
          Complex.norm_cpow_eq_rpow_re_of_pos (neg_pos.mpr hx.2), ← h',
          rpow_zero, one_mul]
      refine IntegrableOn.congr_fun ?_ this measurableSet_Ioo
      rw [integrableOn_const_iff]
      right
      refine (measure_mono Set.Ioo_subset_Icc_self).trans_lt ?_
      exact isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure.lt_top_of_isCompact isCompact_Icc

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

Goal state before:
pp: x : ℝ
hx : x = 0
y : ℝ
hy : y ∈ Metric.ball x 1
⊢ 0 = log⁺ y

Tactic:
rw [eq_comm, posLog_eq_zero_iff y]

Goal state after:
x : ℝ
hx : x = 0
y : ℝ
hy : y ∈ Metric.ball x 1
⊢ |y| ≤ 1
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|
⊢ ∑ t ∈ s, |f t_max| ∈ Set.Ici 0

Tactic:
by simp [mul_nonneg]

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

Goal state before:
pp: b : ℝ
h : b < 0
| ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
arg 1; arg 1; intro t; rw [← log_neg_eq_log]

Goal state after:
b : ℝ
h : b < 0
t : ℝ
| log (-t)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case inl
b : ℝ
h : b < 0
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

pp: case inr.inl
b : ℝ
h : b = 0
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

pp: case inr.inr
b : ℝ
h : 0 < b
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
· -- If t is negative, use that log is an even function to reduce to the positive case.
    conv => arg 1; arg 1; intro t; rw [← log_neg_eq_log]
    rw [intervalIntegral.integral_comp_neg, intervalIntegral.integral_symm, neg_zero,
      integral_log_from_zero_of_pos (Left.neg_pos_iff.mpr h), log_neg_eq_log]
    ring

Goal state after:
case inr.inl
b : ℝ
h : b = 0
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

case inr.inr
b : ℝ
h : 0 < b
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: case h₀
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‖
⊢ ∀ x ∈ [[0, 2 * π]], ‖g (circleMap c R x)‖ ≠ 0

Tactic:
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.Complex.OpenMapping

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
⊢ (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)

Tactic:
by
  by_cases h : ∃ z₀ ∈ U, ∀ᶠ z in 𝓝 z₀, g z = g z₀
  · obtain ⟨z₀, hz₀, h⟩ := h
    exact Or.inl ⟨g z₀, hg.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const hU hz₀ h⟩
  · simp only [not_exists, not_and] at h
    refine Or.inr fun s hs1 hs2 => isOpen_iff_mem_nhds.mpr ?_
    rintro z ⟨w, hw1, rfl⟩
    exact (hg w (hs1 hw1)).eventually_constant_or_nhds_le_map_nhds.resolve_left (h w (hs1 hw1))
        (image_mem_map (hs2.mem_nhds hw1))

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_bd : I∞.BoundedAtFilter f
q : ℂ
hq : q ∈ {0}ᶜ
⊢ (f ∘ invQParam h) q = f (invQParam h q)

Tactic:
comp_def

Goal state after:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_bd : I∞.BoundedAtFilter f
q : ℂ
hq : q ∈ {0}ᶜ
⊢ (fun x ↦ f (invQParam h x)) q = f (invQParam h q)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: n : ℕ
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (n + 1) ≤ ∫ (x : ℝ) in 0..π, sin x ^ n

Tactic:
by
  let H x h := pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (n.le_add_right 1)
  refine integral_mono_on pi_pos.le ?_ ?_ H <;> exact (continuous_sin.pow _).intervalIntegrable 0 π

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
⊢ cuspFunction h (-f) = -cuspFunction h f

Tactic:
by
  simpa using cuspFunction_smul hfcts (-1)

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 θ - ρ‖|)
h_measure_zero : volume {θ | circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ} = 0
θ : ℝ
⊢ ¬(circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ) →
    θ ∈ uIoc 0 (2 * π) →
      Tendsto (fun n ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)) atTop
        (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R θ)))

Tactic:
hθ

Goal state after:
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ :=
  fun θ ↦ (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
h_measure_zero : volume {θ | circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ} = 0
θ : ℝ
hθ : ¬(circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ)
⊢ θ ∈ uIoc 0 (2 * π) →
    Tendsto (fun n ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)) atTop
      (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R θ)))
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : StrictMonoOn f (Iic a)
h₂ : StrictMonoOn f (Ici a)
⊢ StrictMono f

Tactic:
rw [← strictMonoOn_univ, ← @Iic_union_Ici _ _ a]
  exact StrictMonoOn.union h₁ h₂ isGreatest_Iic isLeast_Ici

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
⊢ sqrt (-I) = ↑√2⁻¹ * (1 + I) * -I

Tactic:
rw [sqrt_eq_ite]
  split_ifs with h
  · simp_rw [RingEquiv.symm_apply_eq, map_mul]
    simp [h, mul_assoc, add_comm, Complex.sqrt_neg_I, neg_mul, mul_add, add_mul, mul_sub,
      mul_comm Complex.I, ← sub_eq_add_neg]
  grind [I_eq_zero_or_im_I_eq_one]

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

Goal state before:
pp: 𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝ : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
⊢ TietzeExtension ↑(Metric.closedBall 0 1)

Tactic:
classical
  suffices this : Continuous (piecewise (Metric.closedBall 0 1) id g) by
    refine .of_retract ⟨Subtype.val, by fun_prop⟩ ⟨_, this.codRestrict fun x ↦ ?_⟩ ?_
    · by_cases hx : x ∈ Metric.closedBall 0 1
      · simpa [piecewise_eq_of_mem (hi := hx)] using hx
      · simp only [g, piecewise_eq_of_notMem (hi := hx), RCLike.real_smul_eq_coe_smul (K := 𝕜)]
        by_cases hx' : x = 0 <;> simp [hx']
    · ext x
      simp
  refine continuous_piecewise (fun x hx ↦ ?_) continuousOn_id ?_
  · replace hx : ‖x‖ = 1 := by simpa [frontier_closedBall (0 : E) one_ne_zero] using hx
    simp [g, hx]
  · refine continuousOn_id.norm.inv₀ ?_ |>.smul continuousOn_id
    simp only [closure_compl, interior_closedBall (0 : E) one_ne_zero, mem_compl_iff,
      Metric.mem_ball, dist_zero_right, not_lt, id_eq, ne_eq, norm_eq_zero]
    exact fun x hx ↦ norm_pos_iff.mp <| one_pos.trans_le hx

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

Goal state before:
pp: case hxy
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|
h3 : u ≠ c
⊢ |R / r| ≤ |R * ‖c - u‖⁻¹|

Tactic:
have : ‖c - u‖ ≠ 0 := by simpa [sub_eq_zero] using h3.symm
            simpa [field, abs_div, r_pos.trans r_lt_R, dist_eq_norm'] using h2

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✝ : Nonempty n
h : Function.Surjective ⇑toPGL
r : Rˣ
A : GL n R
hA : GeneralLinearGroup.det A = r
X : SpecialLinearGroup n R
hX : toPGL ↑X = mk A
u : Rˣ
hu : toGL X * (GeneralLinearGroup.scalar n) u = A
⊢ u ^ Fintype.card n = r

Tactic:
by simpa [hA] using congr(Matrix.GeneralLinearGroup.det $hu)

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ denom (-g) z = -denom g z

Tactic:
simp [denom]

Goal state after:
g : GL (Fin 2) ℝ
z : ℂ
⊢ -(↑(↑g 1 0) * z) + -↑(↑g 1 1) = -↑(↑g 1 1) + -(↑(↑g 1 0) * z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℂ
⊢ (σ g) (denom h z) = denom h ((σ g) z)

Tactic:
simp [denom]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
hP : C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
hb : ↑g 0 1 = 0
hc : ↑g 1 0 = 0
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) = ↑g

Tactic:
have hd : g 1 1 = g 0 0 := by simpa [sub_eq_zero] using congr_arg (coeff · 1) hP

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
hP : C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
hb : ↑g 0 1 = 0
hc : ↑g 1 0 = 0
hd : ↑g 1 1 = ↑g 0 0
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) = ↑g
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case mpr
g : GL (Fin 2) ℝ
⊢ g ∈ Subgroup.center (GL (Fin 2) ℝ) → ∀ (z : ℍ), g • z = z

Tactic:
· aesop (add simp GeneralLinearGroup.center_eq_range_scalar)

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

Goal state before:
pp: z : ℍ
⊢ denom 1 ↑z = 1

Tactic:
simp [denom]

Goal state after: