mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_4
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t✝ : ↑I
this : Continuous[_, inst✝¹] fun st ↦ (Γ st.2) st.1
t t' : ↑I
⊢ p ((Γ t) 1) = p ((Γ t') 1)

Tactic:
Γ_lifts,

Goal state after:
case refine_4
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t✝ : ↑I
this : Continuous[_, inst✝¹] fun st ↦ (Γ st.2) st.1
t t' : ↑I
⊢ γ (t, 1) = γ (t', 1)
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ ConformalAt f z

Tactic:
rw [conformalAt_iff_isConformalMap_fderiv, (h.hasFDerivAt.restrictScalars ℝ).fderiv]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ IsConformalMap (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case succ.refine_2
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝¹ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
this : Nonempty ↑(p ⁻¹' {x})
q : Bundle.Trivialization (↑(p ⁻¹' {x})) p := ⋯.toTrivialization
x✝ : ↑I
h : x✝ ∈ Set.Icc 0 (t (n + 1)) ∩ {b | b ≤ t n}
⊢ x✝ ∈ Set.Icc 0 (t n)

Tactic:
exact ⟨h.1.1, h.2⟩

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
g : ℂ → E
D : CanonicalDecomp f g R
⊢ ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt g ↑u ≠ ⊤

Tactic:
rw [← D.meromorphicNFOn.meromorphicOn.exists_meromorphicOrderAt_ne_top_iff_forall
      (Metric.isConnected_closedBall hR.le)]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
g : ℂ → E
D : CanonicalDecomp f g R
⊢ ∃ u, meromorphicOrderAt g ↑u ≠ ⊤
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
hs : UniqueDiffWithinAt ℝ s x
h : DifferentiableWithinAt ℂ f s x
⊢ (fderivWithin ℂ f s x) I = I • (fderivWithin ℂ f s x) 1

Tactic:
rw [(by simp : I = I • 1), (fderivWithin ℂ f s x).map_smul]

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
hs : UniqueDiffWithinAt ℝ s x
h : DifferentiableWithinAt ℂ f s x
⊢ I • (fderivWithin ℂ f s x) 1 = (I • 1) • (fderivWithin ℂ f s x) 1
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) = ⊤
⊢ meromorphicOrderAt (f ∘ g) x = ⊤

Tactic:
meromorphicOrderAt_eq_top_iff

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : ∀ᶠ (z : 𝕜) in 𝓝[≠] g x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ∘ g) z = 0
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
x : ℝ
⊢ ∀ x_1 ∈ norm ∘ f '' re ⁻¹' {x}, 0 ≤ x_1

Tactic:
rintro y ⟨z1, _, hz2⟩

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
x y : ℝ
z1 : ℂ
left✝ : z1 ∈ re ⁻¹' {x}
hz2 : (norm ∘ f) z1 = y
⊢ 0 ≤ y
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

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

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

Tactic:
Real.log_mul (Finset.prod_ne_zero_iff.2 η₁)
        (Finset.prod_ne_zero_iff.2 η₀),

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
η₀ : ∀ x ∈ t₁, ‖w - x‖ ^ (-divisor f S₀R) x ≠ 0
η₁ : ∀ x ∈ t₂, ‖canonicalFactor R x w‖ ^ (divisor f B₀R) x ≠ 0
⊢ log (∏ x ∈ t₂, ‖canonicalFactor R x w‖ ^ (divisor f B₀R) x) + log (∏ x ∈ t₁, ‖w - x‖ ^ (-divisor f S₀R) x) +
      log ‖meromorphicTrailingCoeffAt f w‖ =
    ∑ 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‖

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

Tactic:
by simp [h₂w]

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
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
x : X
e : ↑(p ⁻¹' {x})
⊢ (⋯.monodromyPerm x).ker = (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range

Tactic:
ext γ

Goal state after:
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
p : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
x : X
e : ↑(p ⁻¹' {x})
γ : FundamentalGroup X x
⊢ γ ∈ (⋯.monodromyPerm x).ker ↔ γ ∈ (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε ∈ Iio 0
⊢ ‖g ε z • f z‖ ≤ C

Tactic:
change ε < 0 at ε₀

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
⊢ ‖g ε z • f z‖ ≤ C
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
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
x : X
e : ↑(p ⁻¹' {x})
γ : FundamentalGroup X x
h : ⋯.monodromy γ e = e
⊢ MulOpposite.unop ((hp.fundamentalGroupToMulOpposite e) γ) • ↑e = MulOpposite.unop 1 • ↑e

Tactic:
by
    simp [fundamentalGroupToMulOpposite, h]

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

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

Tactic:
refine hB.mono ?_

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
⊢ norm ∘ scale f l u '' verticalClosedStrip 0 1 ⊆ norm ∘ f '' verticalClosedStrip l u
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
⊢ init m 0 = m 0

Tactic:
simp only [init_def, castSucc_zero]

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

Goal state before:
pp: case right
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₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ Δ (f₁ + f₂) =ᶠ[𝓝 x] 0

Tactic:
filter_upwards [h₁.1.laplacian_add_nhds h₂.1, h₁.2, h₂.2]
    simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun x ↦ c) (Ioo r R)
⊢ f R = c

Tactic:
by
  have : Filter.Tendsto f (𝓝[Iio R] R) (𝓝 (f R)) := by
    apply (h₁f R (right_mem_Ioc.mpr hR)).mono_left
    rw [nhdsWithin_le_iff, mem_nhdsLT_iff_exists_Ioo_subset]
    use r
    simp_all [Ioo_subset_Ioc_self]
  apply tendsto_nhds_unique this (tendsto_const_nhds.congr' _)
  apply Filter.eventuallyEq_of_mem (Ioo_mem_nhdsLT hR) (fun _ hx ↦ (h₂f hx).symm)

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|)
⊢ circleAverage f c R = f c

Tactic:
by
  have h : CircleIntegrable f c R :=
    (hf.continuousOn_ball.mono sphere_subset_closedBall).circleIntegrable'
  rw [SeparatingDual.eq_iff_forall_dual_eq (R := ℝ)]
  intro g
  rw [← g.circleAverage_comp_comm h]
  by_cases hR : R = 0
  · simp_all
  have H : ContinuousOn (circleAverage (g ∘ f) c) (Set.Ioc 0 |R|) := by
    refine ((hf.comp_CLM g).2.mono ?_).circleAverage (fun z hz ↦ hz.1.le)
    intro x hx
    rw [closure_ball _ (by aesop), mem_closedBall_iff_norm]
    exact hx.2
  rw [← circleAverage_abs_radius]
  apply H.eq_of_eqOn_Ioo (by aesop)
  intro r hr
  apply HarmonicOnNhd.circleAverage_eq
  apply (hf.comp_CLM g).1.mono
  rw [abs_of_pos hr.1]
  exact closedBall_subset_ball hr.2

Goal state after:
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₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ circleAverage (f₁ - f₂) c R = circleAverage f₁ c R - circleAverage f₂ c R

Tactic:
rw [circleAverage, circleAverage, circleAverage, ← smul_sub]
  congr
  apply intervalIntegral.integral_sub hf₁ 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))
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
have 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) := by
    intro x hx
    simp [h₂F (sphere_subset_ball (lt_add_of_pos_left R h₁e) hx), herglotzRieszKernel_def]

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)
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: c w z : ℂ
⊢ herglotzRieszKernel c w z = (z - c + (w - c)) / (z - c - (w - c))

Tactic:
by rfl

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

Goal state before:
pp: c w : ℂ
⊢ herglotzRieszKernel c w = fun z ↦ (z - c + (w - c)) / (z - c - (w - c))

Tactic:
ext z
  exact herglotzRieszKernel_def c w z

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

Goal state before:
pp: c w z : ℂ
⊢ poissonKernel c w z = (‖z - c‖ ^ 2 - ‖w - c‖ ^ 2) / ‖z - c - (w - c)‖ ^ 2

Tactic:
by rfl

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

Goal state before:
pp: θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 0 < R + r

Tactic:
positivity [h₁.trans h₂]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C
hz_re : 0 ≤ z.re
hz_im : z.im ≤ 0
⊢ ‖f z‖ ≤ C

Tactic:
obtain ⟨z, rfl⟩ : ∃ z', -z' = z := ⟨-z, neg_neg z⟩
  simp only [neg_re, neg_im, neg_nonpos, neg_nonneg] at hz_re hz_im
  change ‖(f ∘ Neg.neg) z‖ ≤ C
  have H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0) := fun w hw ↦ by
    simpa only [mem_reProdIm, neg_re, neg_im, neg_lt_zero, neg_pos, mem_Ioi, mem_Iio] using hw
  refine quadrant_II
    (hd.comp differentiable_neg.diffContOnCl H) ?_ (fun x hx => ?_) (fun x hx => ?_) hz_re hz_im
  · rcases hB with ⟨c, hc, B, hO⟩
    refine ⟨c, hc, B, ?_⟩
    simpa only [Function.comp_def, norm_neg]
      using hO.comp_tendsto (Filter.tendsto_neg_cobounded.inf H.tendsto)
  · rw [comp_apply, ← ofReal_neg]
    exact hre (-x) (neg_nonneg.2 hx)
  · rw [comp_apply, ← neg_mul, ← ofReal_neg]
    exact him (-x) (neg_nonpos.2 hx)

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

Goal state before:
pp: R : ℝ
w : ℂ
g : ℂ → ℝ
hg : CircleIntegrable g 0 R
hw : w ∈ ball 0 R
h₁ : CircleIntegrable (fun ζ ↦ ↑(g ζ)) 0 R
h₂ : CircleIntegrable (fun ζ ↦ herglotzRieszKernel 0 w ζ • ↑(g ζ)) 0 R
⊢ circleAverage (⇑reCLM ∘ fun ζ ↦ herglotzRieszKernel 0 w ζ • ↑(g ζ)) 0 R =
    circleAverage (re ∘ herglotzRieszKernel 0 w • g) 0 R

Tactic:
simp [Function.comp_def, Complex.mul_re, Pi.mul_def]

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ negMulLog x

Tactic:
refine DifferentiableOn.differentiableAt differentiableOn_negMulLog ?_

Goal state after:
x : ℝ
hx : x ≠ 0
⊢ {0}ᶜ ∈ 𝓝 x
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hR : 0 < R
hw : 0 ∈ ball 0 R
⊢ Real.circleAverage (fun z ↦ ((z + 0) / (z - 0)).re • f z) 0 R = f 0

pp: case inr.inr
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
⊢ Real.circleAverage (fun z ↦ ((z + w) / (z - w)).re • f z) 0 R = f w

Tactic:
· refine (circleAverage_congr_sphere fun z hz ↦ ?_).trans (abs_of_pos hR ▸ hf |>.circleAverage)
    rw [abs_of_pos hR] at hz
    simp [div_self (a := z) (by aesop)]

Goal state after:
case inr.inr
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
⊢ Real.circleAverage (fun z ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: ⊢ Continuous sinc

Tactic:
refine continuous_iff_continuousAt.mpr fun x ↦ ?_
  rw [sinc_eq_dslope]
  by_cases hx : x = 0
  · simp [hx]
  · rw [continuousAt_dslope_of_ne hx]
    fun_prop

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
⊢ ∃ x, 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x‖

Tactic:
have hfc : ContinuousOn (fun x : ℝ => f x) (Ici 0) := by
      refine hd.continuousOn.comp continuous_ofReal.continuousOn fun x hx => ?_
      rwa [closure_setOfPred_lt_re]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
hfc : ContinuousOn (fun x ↦ f ↑x) (Ici 0)
⊢ ∃ x, 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑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
⊢ 1 * R = ‖W‖

Tactic:
simp [W, abs_of_pos hR]

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

Goal state before:
pp: case inr.inl
this✝¹ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) (-1)
this✝ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 1
this : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 0
⊢ deriv (fun x ↦ (log x)⁻¹) (-1) = -(-1)⁻¹ / log (-1) ^ 2

Tactic:
rw [deriv_zero_of_not_differentiableAt ‹_›]

Goal state after:
case inr.inl
this✝¹ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) (-1)
this✝ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 1
this : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 0
⊢ 0 = -(-1)⁻¹ / log (-1) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: case inr.inr.inl
this✝¹ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) (-1)
this✝ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 1
this : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 0
⊢ deriv (fun x ↦ (log x)⁻¹) 0 = -0⁻¹ / log 0 ^ 2

Tactic:
rw [deriv_zero_of_not_differentiableAt ‹_›]

Goal state after:
case inr.inr.inl
this✝¹ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) (-1)
this✝ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 1
this : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 0
⊢ 0 = -0⁻¹ / log 0 ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: case inr.inr.inr
this✝¹ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) (-1)
this✝ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 1
this : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 0
⊢ deriv (fun x ↦ (log x)⁻¹) 1 = -1⁻¹ / log 1 ^ 2

Tactic:
rw [deriv_zero_of_not_differentiableAt ‹_›]

Goal state after:
case inr.inr.inr
this✝¹ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) (-1)
this✝ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 1
this : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 0
⊢ 0 = -1⁻¹ / log 1 ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: case pos
x : ℝ
hx : x = 0
⊢ ContinuousAt log⁺ x

Tactic:
apply ContinuousAt.congr (f := fun _ ↦ 0) (by fun_prop)

Goal state after:
case pos
x : ℝ
hx : x = 0
⊢ (fun x ↦ 0) =ᶠ[nhds x] log⁺
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (f a) ≤ log⁺ (f a)

Tactic:
by rfl

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

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

Tactic:
apply Finset.single_le_sum (fun _ _ ↦ posLog_nonneg) ht_max.1

Goal state after: