mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : ¬MeromorphicOn f₁ U
⊢ divisor f₁ U = divisor f₂ U

Tactic:
· simp [divisor, hf₁, (meromorphicOn_congr_codiscreteWithin h₁ h₂).not.1 hf₁]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mp.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hfg : f =ᶠ[𝓝 x] g
n : ℤ
h : 𝕜 → E
h₁h : AnalyticAt 𝕜 h x
h₂h : h x ≠ 0
h₃h : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • h
⊢ MeromorphicNFAt g x

Tactic:
· exact .inr ⟨n, h, h₁h, h₂h, hfg.symm.trans h₃h⟩

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
R : ℝ
f : 𝕜 → E
⊢ (divisor (f ∘ fun x ↦ x - c) (ball c R)) (z + c) = (divisor f (ball 0 R)) z

Tactic:
by
  rw [divisor_comp_sub_const_eq_divisor, ball_sub_singleton, sub_self]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
⊢ E

Tactic:
by
  by_cases h₁ : MeromorphicAt f x
  · by_cases h₂ : meromorphicOrderAt f x = ⊤
    · exact 0
    · exact ((meromorphicOrderAt_ne_top_iff h₁).1 h₂).choose x
  · exact 0

Goal state after:
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ : AnalyticAt 𝕜 ⋯.choose x
h'₂ : ⋯.choose x ≠ 0
h'₃ : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose z
y : 𝕜
h₁y : (y - x) ^ (meromorphicOrderAt f x).untop₀ • (⋯.choose y - g y) = 0
h₂y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose y
h₃y : y ∈ {x}ᶜ
⊢ ⋯.choose y - g y = 0

Tactic:
smul_eq_zero_iff_right

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ : AnalyticAt 𝕜 ⋯.choose x
h'₂ : ⋯.choose x ≠ 0
h'₃ : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose z
y : 𝕜
h₁y : ⋯.choose y - g y = 0
h₂y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose y
h₃y : y ∈ {x}ᶜ
⊢ ⋯.choose y - g y = 0

𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
h'₁ : AnalyticAt 𝕜 ⋯.choose x
h'₂ : ⋯.choose x ≠ 0
h'₃ : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose z
y : 𝕜
h₁y : (y - x) ^ (meromorphicOrderAt f x).untop₀ • (⋯.choose y - g y) = 0
h₂y : f y = (y - x) ^ (meromorphicOrderAt f x).untop₀ • ⋯.choose y
h₃y : y ∈ {x}ᶜ
⊢ (y - x) ^ (meromorphicOrderAt f x).untop₀ ≠ 0
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
U : Set 𝕜
hf : MeromorphicAt f x
⊢ 𝕜 → E

Tactic:
classical -- do not complain about decidability issues in Function.update
    apply Function.update f x
    by_cases h₁f : meromorphicOrderAt f x = (0 : ℤ)
    · rw [meromorphicOrderAt_eq_int_iff hf] at h₁f
      exact (Classical.choose h₁f) x
    · exact 0

Goal state after:
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 : 𝕜
n : ℤ
hf : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = 0
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = (x_1 - x) ^ n • g x_1
z : 𝕜
hfz : ((z - x) ^ Exists.choose hf * (z - x) ^ n) • g z = 0
hfz_eq : z ∈ {x}ᶜ → f z = (z - x) ^ n • g z
hz : z ∈ {x}ᶜ
⊢ g z = 0

Tactic:
smul_eq_zero_iff_right

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = 0
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = (x_1 - x) ^ n • g x_1
z : 𝕜
hfz : g z = 0
hfz_eq : z ∈ {x}ᶜ → f z = (z - x) ^ n • g z
hz : z ∈ {x}ᶜ
⊢ g z = 0

𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = 0
x✝ : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, x_1 ∈ {x}ᶜ → f x_1 = (x_1 - x) ^ n • g x_1
z : 𝕜
hfz : ((z - x) ^ Exists.choose hf * (z - x) ^ n) • g z = 0
hfz_eq : z ∈ {x}ᶜ → f z = (z - x) ^ n • g z
hz : z ∈ {x}ᶜ
⊢ (z - x) ^ Exists.choose hf * (z - x) ^ n ≠ 0
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x c : 𝕜
⊢ meromorphicTrailingCoeffAt (f ∘ fun x ↦ x + c) x = meromorphicTrailingCoeffAt f (x + c)

Tactic:
by_cases h : ¬ MeromorphicAt f (x + c)
  · simp_all [meromorphicAt_comp_add_const_iff_meromorphicAt.not.2 h]
  rw [MeromorphicAt.meromorphicTrailingCoeffAt_comp (by simp_all) (by fun_prop)
    (by simp [eventuallyConst_iff_analyticOrderAt_sub_eq_top])]
  simp [meromorphicTrailingCoeffAt_id_sub_const]

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

Goal state before:
pp: case refine_2
R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ ¬R = ‖w‖

Tactic:
mem_ball_iff_norm,

Goal state after:
case refine_2
R : ℝ
w : ℂ
h : ‖w - 0‖ < R
⊢ ¬R = ‖w‖
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f⁻¹ z = 0

Tactic:
filter_upwards [h₂f]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
⊢ ∀ (a : 𝕜), f a = 0 → f⁻¹ a = 0
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: case refine_1
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = I
⊢ f = LinearIsometryEquiv.refl ℝ ℂ

Tactic:
apply LinearIsometryEquiv.toLinearEquiv_injective

Goal state after:
case refine_1
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = I
⊢ f.toLinearEquiv = (LinearIsometryEquiv.refl ℝ ℂ).toLinearEquiv
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: case refine_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = -I
⊢ f = conjLIE

Tactic:
apply LinearIsometryEquiv.toLinearEquiv_injective

Goal state after:
case refine_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = -I
⊢ f.toLinearEquiv = conjLIE.toLinearEquiv
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case h₂
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f ((starRingEnd ℂ) ((starRingEnd ℂ) z))
g : ℂ →L[ℂ] ℂ
⊢ fderiv ℝ f z ∘SL ↑conjCLE = fderiv ℝ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)

Tactic:
have : fderiv ℝ conj (conj z) = _ := conjCLE.fderiv

Goal state after:
case h₂
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f ((starRingEnd ℂ) ((starRingEnd ℂ) z))
g : ℂ →L[ℂ] ℂ
this : fderiv ℝ (⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z) = ↑conjCLE
⊢ fderiv ℝ f z ∘SL ↑conjCLE = fderiv ℝ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
x : ℝ
⊢ 0 ≤ sSupNormIm f x

Tactic:
apply Real.sSup_nonneg
  rintro y ⟨z1, _, hz2⟩
  simp only [← hz2, comp, norm_nonneg]

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 : ℂ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ z ∈ closure (verticalStrip 0 1)

Tactic:
rwa [verticalClosedStrip, ← closure_Ioo zero_ne_one, ← closure_preimage_re] at hz

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
⊢ ‖↑(sSupNormIm f 0) ^ (1 - z)‖ * ‖↑(sSupNormIm f 1) ^ z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re

Tactic:
norm_cpow_eq_rpow_re_of_pos ((Ne.le_iff_lt h0).mp (sSupNormIm_nonneg f _)) _

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).re * ‖↑(sSupNormIm f 1) ^ z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: case neg
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = ↑(f z) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
⊢ ∃ F, AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun z ↦ (F z).re) f (ball z R)

Tactic:
use F, h₁F.analyticOnNhd isOpen_ball

Goal state after:
case right
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := ⋯
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = ↑(f z) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
⊢ EqOn (fun z ↦ (F z).re) f (ball z R)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ circleAverage f c (-R) = circleAverage f c R

Tactic:
unfold circleAverage

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c (-R) θ) = (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
⊢ circleAverage f₁ c R = circleAverage f₂ c R

Tactic:
unfold circleAverage

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ) = (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: case e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
⊢ ∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ) = ∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ)

Tactic:
apply intervalIntegral.integral_congr_ae_restrict

Goal state after:
case e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
⊢ (fun x ↦ f₁ (circleMap c R x)) =ᵐ[MeasureTheory.volume.restrict (uIoc 0 (2 * π))] fun x ↦ f₂ (circleMap c R x)
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: case right
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = ↑(f 0) ∧ ∀ x ∈ univ, HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x : ℂ
⊢ (F x).re = f x

Tactic:
rw [← Complex.reCLM_apply, ← Function.comp_apply (f := reCLM)]

Goal state after:
case right
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = ↑(f 0) ∧ ∀ x ∈ univ, HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x : ℂ
⊢ (⇑reCLM ∘ F) x = f x
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : EqOn f₁ f₂ (sphere c |R|)
⊢ circleAverage f₁ c R = circleAverage f₂ c R

Tactic:
unfold circleAverage

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : EqOn f₁ f₂ (sphere c |R|)
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ) = (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
⊢ circleAverage (fun x ↦ f x⁻¹) 0 1 = circleAverage f 0 1

Tactic:
unfold circleAverage

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, (fun x ↦ f x⁻¹) (circleMap 0 1 θ) =
    (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
L : E →L[ℝ] F
f : ℂ → E
hf : CircleIntegrable f c R
⊢ circleAverage (⇑L ∘ f) c R = L (circleAverage f c R)

Tactic:
unfold circleAverage

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
L : E →L[ℝ] F
f : ℂ → E
hf : CircleIntegrable f c R
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, (⇑L ∘ f) (circleMap c R θ) =
    L ((2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ))
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
𝕜 : Type u_3
inst✝³ : NormedDivisionRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : NormSMulClass 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : ℂ → E
c : ℂ
R : ℝ
a : 𝕜
⊢ circleAverage (a • f) c R = a • circleAverage f c R

Tactic:
unfold circleAverage

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
𝕜 : Type u_3
inst✝³ : NormedDivisionRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : NormSMulClass 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : ℂ → E
c : ℂ
R : ℝ
a : 𝕜
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, (a • f) (circleMap c R θ) =
    a • (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℂ
R : ℝ
ι : Type u_4
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ circleAverage (∑ i ∈ s, f i) c R = ∑ i ∈ s, circleAverage (f i) c R

Tactic:
unfold circleAverage

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℂ
R : ℝ
ι : Type u_4
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, (∑ i ∈ s, f i) (circleMap c R θ) =
    ∑ i ∈ s, (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f i (circleMap c R θ)
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: ⊢ Tendsto (fun x ↦ derivWithin (fun x ↦ x * log x) (Set.Ioi x) x) atTop atTop

Tactic:
refine (tendsto_congr' ?_).mpr (tendsto_log_atTop.atTop_add (tendsto_const_nhds (x := 1)))
  rw [EventuallyEq, eventually_atTop]
  exact ⟨1, fun _ hx ↦ rightDeriv_mul_log (zero_lt_one.trans_le hx).ne'⟩

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

Goal state before:
pp: x : ℝ
⊢ deriv^[2] (fun x ↦ -(x * log x)) x = -x⁻¹

Tactic:
have h := deriv2_mul_log

Goal state after:
x : ℝ
h : ∀ (x : ℝ), deriv^[2] (fun x ↦ x * log x) x = x⁻¹
⊢ deriv^[2] (fun x ↦ -(x * log x)) x = -x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: x : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
hx₂ : x ≠ -1
⊢ HasDerivAt (fun x ↦ (log x)⁻¹) (-x⁻¹ / log x ^ 2) x

Tactic:
by
  simpa using (differentiableAt_inv_log hx₀ hx₁ hx₂).hasDerivAt

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
z : ℂ
hz : z ∈ sphere 0 |R|
⊢ ((z + w) / (z - w)).re • f z = (z / (z - w) - q • z / (q • z - W)) • f z

Tactic:
have hzR : ‖z‖ = R := by simpa [abs_of_pos hR] using hz

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
z : ℂ
hz : z ∈ sphere 0 |R|
hzR : ‖z‖ = R
⊢ ((z + w) / (z - w)).re • f z = (z / (z - w) - q • z / (q • z - W)) • f z
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * (k + 1) + 1) =
    (2 * ↑k + 2) / (2 * ↑k + 3) * (2 * ∏ x ∈ Finset.range k, (2 * ↑x + 2) / (2 * ↑x + 3))

Tactic:
← ih,

Goal state after:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * (k + 1) + 1) = (2 * ↑k + 2) / (2 * ↑k + 3) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * (k + 1)) =
    (2 * ↑k + 1) / (2 * ↑k + 2) * (π * ∏ x ∈ Finset.range k, (2 * ↑x + 1) / (2 * ↑x + 2))

Tactic:
← ih,

Goal state after:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * (k + 1)) = (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : w ∈ ball 0 R
hR : 0 < R
⊢ circleAverage (Complex.re ∘ herglotzRieszKernel 0 w • fun x ↦ log ‖x - ρ‖) 0 R = log ‖w - ρ‖

Tactic:
mem_ball_iff_norm,

Goal state after:
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w - 0‖ < R
hR : 0 < R
⊢ circleAverage (Complex.re ∘ herglotzRieszKernel 0 w • fun x ↦ log ‖x - ρ‖) 0 R = log ‖w - ρ‖
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
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 : ℕ
x : ℂ
hx : x ∈ closure (ball 0 (r n))
this : x ≠ ρ
⊢ ‖x - ρ‖ ≠ 0

Tactic:
simpa [sub_eq_zero]

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

Goal state before:
pp: z : ℂ
hz : z ∈ slitPlane
⊢ HasStrictDerivAt sqrt (z ^ (-1 / 2) / 2) z

Tactic:
exact (Complex.hasStrictDerivAt_cpow_const (c := 2⁻¹) hz).congr_deriv (by
    rw [show (2 : ℂ)⁻¹ - 1 = -1 / 2 by norm_num, mul_comm, ← div_eq_mul_inv])

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

Goal state before:
pp: case h
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := ⋯
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
t₀ : c ∈ CB
⊢ IsOpen (ball c |R|) ∧ c ∈ ball c |R| ∧ ball c |R| ∩ {c}ᶜ ⊆ CB

Tactic:
simpa [hR] using! fun _ ⟨h, _⟩ ↦ ball_subset_closedBall h

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

Goal state before:
pp: case refine_2
𝕜 : 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
⊢ ContinuousOn g (closure (Metric.closedBall 0 1)ᶜ)

Tactic:
refine continuousOn_id.norm.inv₀ ?_ |>.smul continuousOn_id

Goal state after:
case refine_2
𝕜 : 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
⊢ ∀ x ∈ closure (Metric.closedBall 0 1)ᶜ, ‖id x‖ ≠ 0
Module: Mathlib.Analysis.Complex.Tietze

Goal state before:
pp: case neg
X : Type u
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
f : ↑s →ᵇ E
hf : ¬‖f‖ = 0
this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)
hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖
g : C(X, E)
hg : ContinuousMap.restrict s g = ↑f
hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖
g' : X →ᵇ E := ⋯
⊢ ‖f‖ ≤ ‖g'‖

Tactic:
refine (f.norm_le <| by positivity).mpr fun x ↦ ?_

Goal state after:
case neg
X : Type u
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
f : ↑s →ᵇ E
hf : ¬‖f‖ = 0
this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)
hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖
g : C(X, E)
hg : ContinuousMap.restrict s g = ↑f
hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖
g' : X →ᵇ E := ofNormedAddCommGroup ⇑g ⋯ ‖f‖ hg_mem
x : ↑s
⊢ ‖f x‖ ≤ ‖g'‖