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

Goal state before:
pp: case left
l u : ℝ
hul : l < u
z : ℂ
hz : 0 ≤ z.re ∧ z.re ≤ 1
⊢ l ≤ l + z.re * (u - l)

pp: case right
l u : ℝ
hul : l < u
z : ℂ
hz : 0 ≤ z.re ∧ z.re ≤ 1
⊢ l + z.re * (u - l) ≤ u

Tactic:
<;>

Goal state after:
case left
l u : ℝ
hul : l < u
z : ℂ
hz : 0 ≤ z.re ∧ z.re ≤ 1
⊢ l ≤ l + z.re * (u - l)

case right
l u : ℝ
hul : l < u
z : ℂ
hz : 0 ≤ z.re ∧ z.re ≤ 1
⊢ l + z.re * (u - l) ≤ u
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c : ℂ
r a₁ a₂ b : ℝ
ha₁ : ↑a₁ + ↑b * I ∈ ball c r
ha₂ : ↑a₂ + ↑b * I ∈ ball c r
⊢ (fun x ↦ ↑x + ↑b * I) '' [[a₁, a₂]] = (↑a₁ + ↑b * I).Rectangle (↑a₂ + ↑b * I)

pp: case convert_1
c : ℂ
r a₁ a₂ b : ℝ
ha₁ : ↑a₁ + ↑b * I ∈ ball c r
ha₂ : ↑a₂ + ↑b * I ∈ ball c r
⊢ ↑(↑a₁ + ↑b * I).re + ↑(↑a₂ + ↑b * I).im * I ∈ ball c r

pp: case convert_2
c : ℂ
r a₁ a₂ b : ℝ
ha₁ : ↑a₁ + ↑b * I ∈ ball c r
ha₂ : ↑a₂ + ↑b * I ∈ ball c r
⊢ ↑(↑a₂ + ↑b * I).re + ↑(↑a₁ + ↑b * I).im * I ∈ ball c r

Tactic:
<;>

Goal state after:
c : ℂ
r a₁ a₂ b : ℝ
ha₁ : ↑a₁ + ↑b * I ∈ ball c r
ha₂ : ↑a₂ + ↑b * I ∈ ball c r
⊢ (fun x ↦ ↑x + ↑b * I) '' [[a₁, a₂]] = (↑a₁ + ↑b * I).Rectangle (↑a₂ + ↑b * I)

case convert_1
c : ℂ
r a₁ a₂ b : ℝ
ha₁ : ↑a₁ + ↑b * I ∈ ball c r
ha₂ : ↑a₂ + ↑b * I ∈ ball c r
⊢ ↑(↑a₁ + ↑b * I).re + ↑(↑a₂ + ↑b * I).im * I ∈ ball c r

case convert_2
c : ℂ
r a₁ a₂ b : ℝ
ha₁ : ↑a₁ + ↑b * I ∈ ball c r
ha₂ : ↑a₂ + ↑b * I ∈ ball c r
⊢ ↑(↑a₂ + ↑b * I).re + ↑(↑a₁ + ↑b * I).im * I ∈ ball c r
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c : ℂ
r a b₁ b₂ : ℝ
hb₁ : ↑a + ↑b₁ * I ∈ ball c r
hb₂ : ↑a + ↑b₂ * I ∈ ball c r
⊢ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]] = (↑a + ↑b₁ * I).Rectangle (↑a + ↑b₂ * I)

pp: case convert_1
c : ℂ
r a b₁ b₂ : ℝ
hb₁ : ↑a + ↑b₁ * I ∈ ball c r
hb₂ : ↑a + ↑b₂ * I ∈ ball c r
⊢ ↑(↑a + ↑b₁ * I).re + ↑(↑a + ↑b₂ * I).im * I ∈ ball c r

pp: case convert_2
c : ℂ
r a b₁ b₂ : ℝ
hb₁ : ↑a + ↑b₁ * I ∈ ball c r
hb₂ : ↑a + ↑b₂ * I ∈ ball c r
⊢ ↑(↑a + ↑b₂ * I).re + ↑(↑a + ↑b₁ * I).im * I ∈ ball c r

Tactic:
<;>

Goal state after:
c : ℂ
r a b₁ b₂ : ℝ
hb₁ : ↑a + ↑b₁ * I ∈ ball c r
hb₂ : ↑a + ↑b₂ * I ∈ ball c r
⊢ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]] = (↑a + ↑b₁ * I).Rectangle (↑a + ↑b₂ * I)

case convert_1
c : ℂ
r a b₁ b₂ : ℝ
hb₁ : ↑a + ↑b₁ * I ∈ ball c r
hb₂ : ↑a + ↑b₂ * I ∈ ball c r
⊢ ↑(↑a + ↑b₁ * I).re + ↑(↑a + ↑b₂ * I).im * I ∈ ball c r

case convert_2
c : ℂ
r a b₁ b₂ : ℝ
hb₁ : ↑a + ↑b₁ * I ∈ ball c r
hb₂ : ↑a + ↑b₂ * I ∈ ball c r
⊢ ↑(↑a + ↑b₂ * I).re + ↑(↑a + ↑b₁ * I).im * I ∈ ball c r
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: case hb₁
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ ↑w.re + ↑z.im * I ∈ ball c r

pp: case hb₂
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ ↑w.re + ↑w.im * I ∈ ball c r

Tactic:
<;>

Goal state after:
case hb₁
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ ↑w.re + ↑z.im * I ∈ ball c r

case hb₂
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ ↑w.re + ↑w.im * I ∈ ball c r
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init m 0 = m 0
hmtail : tail m (last n) = m (last n.succ)
⊢ ∂_{m 0} (∂^{tail m} f) = ∂_{m 0} (∂^{init (tail m)} (∂_{tail m (last n)} f))

Tactic:
by
        congr 1
        exact IH _

Goal state after:
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₂
⊢ 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₂
⊢ HarmonicAt f₂ x → HarmonicAt f₁ x

Tactic:
<;>

Goal state after:
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₂
⊢ HarmonicAt f₁ x → HarmonicAt f₂ x

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₂
⊢ HarmonicAt f₂ x → HarmonicAt f₁ x
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: case e_6.«0»
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
e : ℝ
s : Set ℝ
f : ℝ → F
hs : UniqueDiffOn ℝ s
he : e ∈ s
⊢ ![1, 1] ((fun i ↦ i) ⟨0, ⋯⟩) = 1

pp: case e_6.«1»
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
e : ℝ
s : Set ℝ
f : ℝ → F
hs : UniqueDiffOn ℝ s
he : e ∈ s
⊢ ![1, 1] ((fun i ↦ i) ⟨1, ⋯⟩) = 1

Tactic:
<;>

Goal state after:
case e_6.«0»
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
e : ℝ
s : Set ℝ
f : ℝ → F
hs : UniqueDiffOn ℝ s
he : e ∈ s
⊢ ![1, 1] ((fun i ↦ i) ⟨0, ⋯⟩) = 1

case e_6.«1»
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
e : ℝ
s : Set ℝ
f : ℝ → F
hs : UniqueDiffOn ℝ s
he : e ∈ s
⊢ ![1, 1] ((fun i ↦ i) ⟨1, ⋯⟩) = 1
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
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
⊢ HarmonicAt (⇑l ∘ 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
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
⊢ HarmonicAt f x → HarmonicAt (⇑l ∘ f) x

Tactic:
<;>

Goal state after:
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
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
⊢ HarmonicAt (⇑l ∘ f) x → HarmonicAt f x

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
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
⊢ HarmonicAt f x → HarmonicAt (⇑l ∘ f) x
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: case calc_2.calc.step.e_a.e_a.e_a
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
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
⊢ ↑w.re - ↑z.re = ↑(algebraMap ℝ ℂ).toMonoidWithZeroHom (w - z).re

pp: case calc_2.calc.step.e_a.e_a.e_a.e_a
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
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
⊢ ↑w.im - ↑z.im = ↑(algebraMap ℝ ℂ).toMonoidWithZeroHom (w - z).im

Tactic:
<;>

Goal state after:
case calc_2.calc.step.e_a.e_a.e_a
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
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
⊢ ↑w.re - ↑z.re = ↑(algebraMap ℝ ℂ).toMonoidWithZeroHom (w - z).re

case calc_2.calc.step.e_a.e_a.e_a.e_a
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
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
⊢ ↑w.im - ↑z.im = ↑(algebraMap ℝ ℂ).toMonoidWithZeroHom (w - z).im
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
⊢ ⨍ (x : ℝ) in a..b, f x = ⨍ (x : ℝ) in b..a, f x

Tactic:
rw [setAverage_eq, setAverage_eq, uIoc_comm]

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

Goal state before:
pp: case left
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
this✝ : 0 < Real.cos z.im
this : 0 < Real.sin z.im
⊢ 0 < expR z.re * Real.cos z.im

pp: case right
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
this✝ : 0 < Real.cos z.im
this : 0 < Real.sin z.im
⊢ 0 < expR z.re * Real.sin z.im

Tactic:
<;>

Goal state after:
case left
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
this✝ : 0 < Real.cos z.im
this : 0 < Real.sin z.im
⊢ 0 < expR z.re * Real.cos z.im

case right
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
z : ℂ
hz : z ∈ im ⁻¹' Ioo 0 (π / 2)
this✝ : 0 < Real.cos z.im
this : 0 < Real.sin z.im
⊢ 0 < expR z.re * Real.sin z.im
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
⊢ circleAverage f c R = f c

Tactic:
SeparatingDual.eq_iff_forall_dual_eq (R := ℝ)

Goal state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
⊢ ∀ (g : StrongDual ℝ F), g (circleAverage f c R) = g (f c)
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
  congr 1
  calc ∫ θ in 0..2 * π, f (circleMap 0 1 θ)⁻¹
  _ = ∫ θ in 0..2 * π, f (circleMap 0 1 (-θ)) := by
    simp [circleMap_zero_inv]
  _ = ∫ θ in 0..2 * π, f (circleMap 0 1 θ) := by
    rw [intervalIntegral.integral_comp_neg (fun w ↦ f (circleMap 0 1 w))]
    have t₀ : Function.Periodic (fun w ↦ f (circleMap 0 1 w)) (2 * π) :=
      fun x ↦ by simp [periodic_circleMap 0 1 x]
    simpa using (t₀.intervalIntegral_add_eq (-(2 * π)) 0)

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

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
h : CircleIntegrable f c R
⊢ circleAverage f c R = f c

Tactic:
SeparatingDual.eq_iff_forall_dual_eq (R := ℝ)

Goal state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
h : CircleIntegrable f c R
⊢ ∀ (g : StrongDual ℝ F), g (circleAverage f c R) = g (f c)
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
  rw [map_smul]
  congr
  exact L.intervalIntegral_comp_comm hf

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

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun z ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
h₄F :
  Set.EqOn (re ∘ herglotzRieszKernel c w • f) (⇑reCLM ∘ fun z ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c |R|)
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
rw [circleAverage_congr_sphere h₄F, reCLM.circleAverage_comp_comm,
    h₃F.diffContOnCl.circleAverage_re_herglotzRieszKernel_smul' hw]

Goal state after:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun z ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
h₄F :
  Set.EqOn (re ∘ herglotzRieszKernel c w • f) (⇑reCLM ∘ fun z ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c |R|)
⊢ reCLM (F w) = f w

f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun z ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
h₄F :
  Set.EqOn (re ∘ herglotzRieszKernel c w • f) (⇑reCLM ∘ fun z ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c |R|)
⊢ CircleIntegrable (fun z ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z) c R
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: z : ℍ
⊢ Function.Injective fun x ↦ x • z

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ h

Goal state after:
z : ℍ
x : ℝ
hx : 0 < x
y : ℝ
hy : 0 < y
h : (fun x ↦ x • z) ⟨x, hx⟩ = (fun x ↦ x • z) ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℤ
⊢ x ^ 2 ≠ ↑n ^ 2

Tactic:
by
  have := not_exists.mp hx n
  have := not_exists.mp hx (-n)
  simp_all [sq_eq_sq_iff_eq_or_eq_neg, eq_comm]

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

Goal state before:
pp: φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
⊢ (R ^ 2 - r ^ 2) * (R - r) ≤ (R + r) * (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ))

pp: case hb
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
⊢ 0 < R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)

pp: case hd
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
⊢ 0 < R - r

Tactic:
<;>

Goal state after:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
⊢ (R ^ 2 - r ^ 2) * (R - r) ≤ (R + r) * (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ))

case hb
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
⊢ 0 < R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)

case hd
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
⊢ 0 < R - r
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: case neg.inl
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : ¬0 < x
h✝ : 0 < x
⊢ x - 1 < x * log x

pp: case neg.inr
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : ¬0 < x
h✝ : 0 = x
⊢ x - 1 < x * log x

Tactic:
<;>

Goal state after:
case neg.inl
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : ¬0 < x
h✝ : 0 < x
⊢ x - 1 < x * log x

case neg.inr
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : ¬0 < x
h✝ : 0 = x
⊢ x - 1 < x * log x
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: case inr
⊢ ContinuousAt (fun x ↦ x * log x) 0

Tactic:
ContinuousAt,

Goal state after:
case inr
⊢ Filter.Tendsto (fun x ↦ x * log x) (𝓝 0) (𝓝 (0 * log 0))
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: case mpr.h
x : ℝ
hx : x ≠ 0
this✝ : x ∈ {0}ᶜ
this : DifferentiableWithinAt ℝ negMulLog {0}ᶜ x
⊢ DifferentiableWithinAt ℝ negMulLog {0}ᶜ x

pp: case mpr.hs
x : ℝ
hx : x ≠ 0
this✝ : x ∈ {0}ᶜ
this : DifferentiableWithinAt ℝ negMulLog {0}ᶜ x
⊢ {0}ᶜ ∈ 𝓝 x

Tactic:
<;>

Goal state after:
case mpr.h
x : ℝ
hx : x ≠ 0
this✝ : x ∈ {0}ᶜ
this : DifferentiableWithinAt ℝ negMulLog {0}ᶜ x
⊢ DifferentiableWithinAt ℝ negMulLog {0}ᶜ x

case mpr.hs
x : ℝ
hx : x ≠ 0
this✝ : x ∈ {0}ᶜ
this : DifferentiableWithinAt ℝ negMulLog {0}ᶜ x
⊢ {0}ᶜ ∈ 𝓝 x
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 : ℂ
h : ‖x‖ ≤ R
⊢ ‖↑q * x‖ = q * ‖x‖

Tactic:
by simp [abs_of_pos h₁q]

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

Goal state before:
pp: H : Tendsto (fun t ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (fun x ↦ (log x)⁻¹) 0))
x : ℝ
x✝ : x ∈ Set.Ioo (-1) 0
hx₁ : -1 < x
hx₂ : x < 0
⊢ log x < 0

Tactic:
apply log_neg_eq_log x ▸ log_neg

Goal state after:
case h0
H : Tendsto (fun t ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (fun x ↦ (log x)⁻¹) 0))
x : ℝ
x✝ : x ∈ Set.Ioo (-1) 0
hx₁ : -1 < x
hx₂ : x < 0
⊢ 0 < -x

case h1
H : Tendsto (fun t ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (fun x ↦ (log x)⁻¹) 0))
x : ℝ
x✝ : x ∈ Set.Ioo (-1) 0
hx₁ : -1 < x
hx₂ : x < 0
⊢ -x < 1
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: case h0
H : Tendsto (fun t ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (fun x ↦ (log x)⁻¹) 0))
x : ℝ
x✝ : x ∈ Set.Ioo (-1) 0
hx₁ : -1 < x
hx₂ : x < 0
⊢ 0 < -x

pp: case h1
H : Tendsto (fun t ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (fun x ↦ (log x)⁻¹) 0))
x : ℝ
x✝ : x ∈ Set.Ioo (-1) 0
hx₁ : -1 < x
hx₂ : x < 0
⊢ -x < 1

Tactic:
<;>

Goal state after:
case h0
H : Tendsto (fun t ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (fun x ↦ (log x)⁻¹) 0))
x : ℝ
x✝ : x ∈ Set.Ioo (-1) 0
hx₁ : -1 < x
hx₂ : x < 0
⊢ 0 < -x

case h1
H : Tendsto (fun t ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (fun x ↦ (log x)⁻¹) 0))
x : ℝ
x✝ : x ∈ Set.Ioo (-1) 0
hx₁ : -1 < x
hx₂ : x < 0
⊢ -x < 1
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ AEStronglyMeasurable (fun x ↦ ↑x ^ r) (volume.restrict (Ι 0 c))

Tactic:
refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_uIoc
      refine continuousOn_of_forall_continuousAt fun x hx => ?_
      rw [uIoc_of_le hc] at hx
      refine (continuousAt_cpow_const (Or.inl ?_)).comp Complex.continuous_ofReal.continuousAt
      rw [Complex.ofReal_re]
      exact hx.1

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

Goal state before:
pp: case refine_1
R : ℝ
w c : ℂ
hw : w ∈ ball c R
this : Disjoint {w} (ball c R)ᶜ
d : ℝ
hd : 0 < d
h_disj : Disjoint (thickening d {w}) (thickening d (ball c R)ᶜ)
⊢ ball w d ⊆ ball c R

pp: case refine_2
R : ℝ
w c : ℂ
hw : w ∈ ball c R
this : Disjoint {w} (ball c R)ᶜ
d : ℝ
hd : 0 < d
h_disj : Disjoint (thickening d {w}) (thickening d (ball c R)ᶜ)
⊢ ∀ x ∈ ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap c R θ - x‖

Tactic:
<;>

Goal state after:
case refine_1
R : ℝ
w c : ℂ
hw : w ∈ ball c R
this : Disjoint {w} (ball c R)ᶜ
d : ℝ
hd : 0 < d
h_disj : Disjoint (thickening d {w}) (thickening d (ball c R)ᶜ)
⊢ ball w d ⊆ ball c R

case refine_2
R : ℝ
w c : ℂ
hw : w ∈ ball c R
this : Disjoint {w} (ball c R)ᶜ
d : ℝ
hd : 0 < d
h_disj : Disjoint (thickening d {w}) (thickening d (ball c R)ᶜ)
⊢ ∀ x ∈ ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap c R θ - x‖
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 ↑s.card + log⁺ |f t_max| ≤ log ↑s.card + ∑ t ∈ s, log⁺ (f t)

Tactic:
gcongr
    rw [posLog_abs]
    apply Finset.single_le_sum (fun _ _ ↦ posLog_nonneg) ht_max.1

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

Goal state before:
pp: case e'_3
x y : ℝ
⊢ log⁺ (x + y) = log⁺ (∑ t, ![x, y] t)

pp: case e'_4
x y : ℝ
⊢ log 2 + log⁺ x + log⁺ y = log ↑Finset.univ.card + ∑ t, log⁺ (![x, y] t)

Tactic:
<;>

Goal state after:
case e'_3
x y : ℝ
⊢ log⁺ (x + y) = log⁺ (∑ t, ![x, y] t)

case e'_4
x y : ℝ
⊢ log 2 + log⁺ x + log⁺ y = log ↑Finset.univ.card + ∑ t, log⁺ (![x, y] t)
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
a b : E
⊢ log⁺ (‖a‖ + ‖b‖) ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2

Tactic:
posLog_add,

Goal state after:
E : Type u_1
inst✝ : SeminormedAddCommGroup E
a b : E
⊢ log 2 + log⁺ ‖a‖ + log⁺ ‖b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

Tactic:
by_cases hc : c = 0

Goal state after:
case pos
a b c : ℝ
hc : c = 0
⊢ ∫ (x : ℝ) in a..b, c * (c ^ 2 + x ^ 2)⁻¹ = arctan (b / c) - arctan (a / c)

case neg
a b c : ℝ
hc : ¬c = 0
⊢ ∫ (x : ℝ) in a..b, c * (c ^ 2 + x ^ 2)⁻¹ = arctan (b / c) - arctan (a / c)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case neg
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
⊢ |R|⁻¹ * |‖c - a‖| ≤ 1

Tactic:
abs_of_nonneg (norm_nonneg (c - a))

Goal state after:
case neg
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
⊢ |R|⁻¹ * ‖c - a‖ ≤ 1