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

Goal state before:
pp: case pos.inr
R : ℝ
w : ℂ
hw : w ∈ ball 0 R
z : ℂ
hz : z ∈ ball 0 R
h₂z : z ≠ w
⊢ (meromorphicOrderAt (canonicalFactor R w) z).untop₀ =
    (-locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯) z

Tactic:
· have : meromorphicOrderAt (canonicalFactor R w) z = 0 := by
        rw [(meromorphicNFOn_canonicalFactor hw (Set.mem_univ z)).meromorphicOrderAt_eq_zero_iff]
        exact canonicalFactor_ne_zero hw (ball_subset_closedBall hz) h₂z
      simp [this, h₂z, Function.locallyFinsuppWithin.restrict_apply, hz]

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

Goal state before:
pp: R : ℝ
w : ℂ
hw : w ∈ ball 0 R
⊢ divisor (canonicalFactor R w) (ball 0 R) = -locallyFinsuppWithin.restrict (locallyFinsuppWithin.single w 1) ⋯

Tactic:
ext z
  by_cases hz : z ∈ ball 0 R
  · rw [MeromorphicOn.divisor_apply
      (fun z hz ↦ meromorphic_canonicalFactor R w z) hz]
    obtain (rfl | h₂z) := eq_or_ne z w
    · rw [meromorphicOrderAt_canonicalFactor hz]
      simp_all [Function.locallyFinsuppWithin.restrict_apply]
    · have : meromorphicOrderAt (canonicalFactor R w) z = 0 := by
        rw [(meromorphicNFOn_canonicalFactor hw (Set.mem_univ z)).meromorphicOrderAt_eq_zero_iff]
        exact canonicalFactor_ne_zero hw (ball_subset_closedBall hz) h₂z
      simp [this, h₂z, Function.locallyFinsuppWithin.restrict_apply, hz]
  · simp_all

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
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
⊢ Preperfect (closedBall 0 R)

Tactic:
rw [← closure_ball _ hR.ne']

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
⊢ Preperfect (closure (ball 0 R))
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : U \ {x} ⊆ {x}ᶜ
⊢ ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, ContinuousAt f y

Tactic:
exact nhdsWithin_mono _ this (h x hx).eventually_continuousAt

Goal state after:
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
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
H' : ↑I × A → E
⊢ H' = ⇑(cov.liftHomotopy H f H_0) ↔
    (∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)) ∧ p ∘ H' = ⇑H ∧ ∀ (a : A), H' (0, a) = f a

Tactic:
by
  refine ⟨?_, fun ⟨H'_cont, H'_lifts, H'_0⟩ ↦ funext fun ⟨t, a⟩ ↦ ?_⟩
  · rintro rfl; refine ⟨fun a ↦ ?_, cov.liftHomotopy_lifts H f H_0, cov.liftHomotopy_zero H f H_0⟩
    simp_rw [liftHomotopy_apply]; exact (cov.liftPath _ _ <| H_0 a).2
  · apply congr_fun ((cov.eq_liftPath_iff _).mpr ⟨H'_cont a, _, H'_0 a⟩) t
    ext ⟨t, a⟩; exact congr_fun H'_lifts _

Goal state after:
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
cov : IsCoveringMap p
x y : X
γ : Path.Homotopic.Quotient x y
e : ↑(p ⁻¹' {x})
⊢ (cov.liftPathQuotient γ e).map { toFun := p, continuous_toFun := ⋯ } = γ.cast ⋯ ⋯

Tactic:
obtain ⟨γ⟩ := γ
  refine congr_arg Path.Homotopic.Quotient.mk ?_
  ext1
  exact cov.liftPath_lifts _ _ (γ.source.trans e.2.symm)

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

Goal state before:
pp: case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
⊢ re ⁻¹' {z.re} ⊆ verticalClosedStrip 0 1

Tactic:
exact preimage_mono (singleton_subset_iff.mpr hD)

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
⊢ ∑ i ∈ t₂, log (‖canonicalFactor R i w‖ ^ (divisor f B₀R) i) + ∑ i ∈ t₁, log (‖w - i‖ ^ (-divisor f S₀R) i) +
      log ‖meromorphicTrailingCoeffAt f w‖ =
    ∑ i ∈ t₂, ↑((divisor f B₀R) i) * log ‖canonicalFactor R i w‖ + ∑ x ∈ t₁, -(↑((divisor f S₀R) x) * log ‖w - x‖) +
      log ‖meromorphicTrailingCoeffAt f w‖

Tactic:
congr! 3 with i hi i hi

Goal state after:
case e'_5.a
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
i : ℂ
hi : i ∈ t₂
⊢ log (‖canonicalFactor R i w‖ ^ (divisor f B₀R) i) = ↑((divisor f B₀R) i) * log ‖canonicalFactor R i w‖

case e'_6.a
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
i : ℂ
hi : i ∈ t₁
⊢ log (‖w - i‖ ^ (-divisor f S₀R) i) = -(↑((divisor f S₀R) i) * log ‖w - i‖)
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
U : Set ℂ
hf : DifferentiableOn ℂ f U
⊢ IsConservativeOn f U

Tactic:
by
  rintro z w hzw
  rw [← add_eq_zero_iff_eq_neg, wedgeIntegral_add_wedgeIntegral_eq]
  exact integral_boundary_rect_eq_zero_of_differentiableOn f z w <| hf.mono hzw

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

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

Tactic:
rw [sub_mul, div_mul_comm, div_self (by norm_cast; linarith),
    div_mul_comm, div_self (by norm_cast; linarith)]

Goal state after:
l u : ℝ
hul : l < u
z : ℂ
⊢ ↑l + (1 * z - 1 * ↑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

pp: case mpr
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:
case mpr
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
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₂ =ᶠ[𝓝[insert x s] x] (Δ[s] f₁) + Δ[s] f₂

Tactic:
filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp),
    eventually_mem_nhdsWithin] with y h₁y h₂y h₃y

Goal state after:
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
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
h₃y : y ∈ insert x s
⊢ (Δ[s] f₁ + f₂) y = ((Δ[s] f₁) + Δ[s] f₂) y
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₂ =ᶠ[𝓝[s] x] (Δ[s] f₁) + Δ[s] f₂

Tactic:
by
  nth_rw 1 [← s.insert_eq_of_mem hx]
  filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp),
    eventually_mem_nhdsWithin] with y h₁y h₂y h₃y
  rw [s.insert_eq_of_mem hx] at h₃y
  simp [h₁y.laplacianWithin_add h₂y hs h₃y]

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₂ =ᶠ[𝓝[insert x s] x] (Δ[s] f₁) - Δ[s] f₂

Tactic:
filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp),
    eventually_mem_nhdsWithin] with y h₁y h₂y h₃y

Goal state after:
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
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
h₃y : y ∈ insert x s
⊢ (Δ[s] f₁ - f₂) y = ((Δ[s] f₁) - Δ[s] f₂) y
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case inr.refine_1.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
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 : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ (f ∘ cexp) =O[comap re atBot ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))] fun z ↦ expR (max B 0 * expR (c * |z.re|))

pp: case inr.refine_1.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
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 : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ (fun x ↦ ‖((fun z ↦ expR (B * ‖z‖ ^ c)) ∘ cexp) x‖) ≤ᶠ[comap re atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))] fun z ↦
    expR (max B 0 * expR (c * |z.re|))

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

Goal state after:
case inr.refine_1.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
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 : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ (fun x ↦ ‖((fun z ↦ expR (B * ‖z‖ ^ c)) ∘ cexp) x‖) ≤ᶠ[comap re atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))] fun z ↦
    expR (max B 0 * expR (c * |z.re|))
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
⊢ (↑(2 * π))⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) =
    (I⁻¹ * (2 * ↑π)⁻¹) • I • ∫ (x : ℝ) in 0..2 * π, f (circleMap c R x)

Tactic:
smul_smul

Goal state after:
c : ℂ
R : ℝ
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
⊢ (↑(2 * π))⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) =
    (I⁻¹ * (2 * ↑π)⁻¹ * I) • ∫ (x : ℝ) in 0..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:
abs_of_neg hR,

Goal state after:
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
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: a b : ℂ
⊢ ((a + b) / (a - b)).re = (‖a‖ ^ 2 - ‖b‖ ^ 2) / ‖a - b‖ ^ 2

Tactic:
rw [div_re, normSq_eq_norm_sq (a - b), ← add_div, add_re, sub_re, add_im, sub_im]
  calc ((a.re + b.re) * (a.re - b.re) + (a.im + b.im) * (a.im - b.im)) / ‖a - b‖ ^ 2
    _ = ((a.re * a.re + a.im * a.im) - (b.re * b.re + b.im * b.im)) / ‖a - b‖ ^ 2 := by
      congr! 1; ring
    _ = (‖a‖ ^ 2 - ‖b‖ ^ 2) / ‖a - b‖ ^ 2 := by
      simp [← normSq_apply, normSq_eq_norm_sq]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y | y ≠ 0}) ∈ 𝓝 z
⊢ ⇑reCLM ∘ ⇑ofRealCLM ∘ Real.log ∘ ⇑normSq ∘ g =ᶠ[𝓝 z] ⇑reCLM ∘ log ∘ (⇑conjCLE ∘ g * g)

Tactic:
filter_upwards with x
      simp only [Function.comp_apply, ofRealCLM_apply, Pi.mul_apply, conjCLE_apply]
      rw [ofReal_log, normSq_eq_conj_mul_self]
      exact normSq_nonneg (g x)

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

Goal state before:
pp: x y : ℝ
⊢ (x * y).negMulLog = y * x.negMulLog + x * y.negMulLog

Tactic:
simp only [negMulLog, neg_mul]

Goal state after:
x y : ℝ
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

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

Tactic:
simp only [isLittleO_one_left_iff, norm_eq_abs]

Goal state after:
⊢ Tendsto (fun x ↦ |log (log x)|) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: ⊢ MonotoneOn log⁺ (Set.Ici 0)

Tactic:
intro x hx y hy hxy
  simp only [posLog, le_sup_iff, sup_le_iff, le_refl, true_and]
  by_cases! h : log x ≤ 0
  · tauto
  · right
    have := log_le_log (lt_trans Real.zero_lt_one ((log_pos_iff hx).1 h)) hxy
    simp only [this, and_true, ge_iff_le]
    linarith

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

Goal state before:
pp: a b : ℝ
h : 0 ∉ [[a, b]]
h' : ∀ x ∈ [[a, b]], x ≠ 0
⊢ ∫ (x : ℝ) in a..b, x⁻¹ = log (b / a)

Tactic:
integral_deriv_eq_sub' _ deriv_log' (fun x hx => differentiableAt_log (h' x hx))
      (continuousOn_inv₀.mono <| subset_compl_singleton_iff.mpr h),

Goal state after:
a b : ℝ
h : 0 ∉ [[a, b]]
h' : ∀ x ∈ [[a, b]], x ≠ 0
⊢ log b - log a = log (b / a)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: r : ℝ
⊢ -(Complex.sin ↑r * (Complex.I * Complex.I) - -Complex.sin ↑r * (Complex.I * Complex.I)) = 2 * Complex.sin ↑r

Tactic:
two_mul

Goal state after:
r : ℝ
⊢ -(Complex.sin ↑r * (Complex.I * Complex.I) - -Complex.sin ↑r * (Complex.I * Complex.I)) =
    Complex.sin ↑r + Complex.sin ↑r
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

Tactic:
by
  simpa only [sq, sub_eq_add_neg, neg_mul_eq_mul_neg] using
    integral_deriv_mul_eq_sub (fun x _ => hasDerivAt_sin x) (fun x _ => hasDerivAt_cos x)
      continuousOn_cos.intervalIntegrable continuousOn_sin.neg.intervalIntegrable

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

Goal state before:
pp: case inl
a : ℂ
h : 1 < ‖a‖
⊢ log ‖a‖ = log⁺ ‖a‖

Tactic:
apply (posLog_eq_log _).symm

Goal state after:
a : ℂ
h : 1 < ‖a‖
⊢ 1 ≤ |‖a‖|
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ circleAverage ((fun z ↦ log ‖R‖) + fun z ↦ log ‖z + ↑R⁻¹ * (c - a)‖) 0 1 = log R + log⁺ (|R|⁻¹ * ‖c - a‖)

Tactic:
circleAverage_add (circleIntegrable_const (log ‖R‖) 0 1)
      (MeromorphicOn.circleIntegrable_log_norm (fun _ _ ↦ by fun_prop)),

Goal state after:
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ circleAverage (fun x ↦ log ‖R‖) 0 1 + circleAverage (fun x ↦ log ‖x + ↑R⁻¹ * (c - a)‖) 0 1 =
    log R + log⁺ (|R|⁻¹ * ‖c - a‖)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ z : ℂ
hz_w : z ≠ w
hz_ρ : z ≠ ρ
⊢ ‖z - ρ‖ ≠ 0

Tactic:
simp_all [sub_eq_zero]

Goal state after:
Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : SeminormedCommRing 𝕜
inst✝² : SeminormedRing β
inst✝¹ : Algebra 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
l : Filter α
f g : α → β
hf : f ∈ boundedFilterSubmodule 𝕜 l
hg : g ∈ boundedFilterSubmodule 𝕜 l
⊢ f * g ∈ boundedFilterSubmodule 𝕜 l

Tactic:
by simpa only [Pi.one_apply, mul_one, norm_mul] using! hf.mul hg

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

Goal state before:
pp: case inr
n : ℕ
inst✝ : NeZero (-↑n)
⊢ IsOpenQuotientMap fun z ↦ ⟨↑z ^ (-↑n), ⋯⟩

Tactic:
· have : NeZero n := ⟨Nat.cast_ne_zero.mp <| neg_ne_zero.mp (NeZero.ne (-n : ℤ))⟩
    convert! (isOpenQuotientMap_pow_compl_zero n).comp (Homeomorph.inv₀ ℂ).isOpenQuotientMap
    simp [Homeomorph.inv₀]

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

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ z - c
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
hz' : z - c = ↑(z - c).re
⊢ 0 ≤ f z

Tactic:
rw [hz'] at hz₁ H

Goal state after:
f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ ↑(z - c).re
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * ↑(z - c).re ^ n = f z
hz' : z - c = ↑(z - c).re
⊢ 0 ≤ f z
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
u : ℂ
hu : u ∈ h.toFinset
⊢ IntervalIntegrable (fun x ↦ log ‖circleMap c R x - u‖) volume 0 (2 * π)

Tactic:
apply (analyticOnNhd_id.sub analyticOnNhd_const).meromorphicOn.circleIntegrable_log_norm

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

Goal state before:
pp: case pos
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
⊢ ↑(ENat.map Nat.cast (analyticOrderAt f u)).untop₀ * Real.log (R / r) ≤
    ↑(ENat.map Nat.cast (analyticOrderAt f u)).untop₀ * Real.log (R * ‖c - u‖⁻¹)

Tactic:
h3,

Goal state after:
case pos
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
⊢ ↑(ENat.map Nat.cast (analyticOrderAt f c)).untop₀ * Real.log (R / r) ≤
    ↑(ENat.map Nat.cast (analyticOrderAt f c)).untop₀ * Real.log (R * ‖c - c‖⁻¹)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case inr.inl
g g' : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g).det
h' : (↑g').det < 0
⊢ (if 0 < ↑(GeneralLinearGroup.det g) * ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ
      else Complex.conjCAE)
      z =
    (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
      ((if 0 < ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z)

pp: case inr.inr
g g' : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g).det
h' : 0 < (↑g').det
⊢ (if 0 < ↑(GeneralLinearGroup.det g) * ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ
      else Complex.conjCAE)
      z =
    (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
      ((if 0 < ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z)

Tactic:
· simp [(mul_neg_of_pos_of_neg h h').not_gt, h, h'.not_gt]

Goal state after:
case inr.inr
g g' : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g).det
h' : 0 < (↑g').det
⊢ (if 0 < ↑(GeneralLinearGroup.det g) * ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ
      else Complex.conjCAE)
      z =
    (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
      ((if 0 < ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case «0».«0»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ ((m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2)) ((fun i ↦ i) ⟨0, ⋯⟩)
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    diagonal (fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Matrix.mul_apply]
    field

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

Goal state before:
pp: case «0».«1»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ ((m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2)) ((fun i ↦ i) ⟨0, ⋯⟩)
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    diagonal (fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Matrix.mul_apply]
    field

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

Goal state before:
pp: case «1».«0»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ ((m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2)) ((fun i ↦ i) ⟨1, ⋯⟩)
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    diagonal (fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Matrix.mul_apply]
    field

Goal state after: