mathlib-initiative/mathlib-tactics huggingface dataset:
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
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
g : G
x : X
e : ↑(p ⁻¹' {x})
γ✝ γ γ' : FundamentalGroup X x
⊢ (hp.fiberEquivGroup e) (⋯.monodromy γ (⋯.monodromy γ' e)) • ↑e =
    (hp.fiberEquivGroup e) (⋯.monodromy γ' e) • (hp.fiberEquivGroup e) (⋯.monodromy γ e) • ↑e

Tactic:
fiberEquivGroup_smul_self,

Goal state after:
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
g : G
x : X
e : ↑(p ⁻¹' {x})
γ✝ γ γ' : FundamentalGroup X x
⊢ ↑(⋯.monodromy γ (⋯.monodromy γ' e)) = (hp.fiberEquivGroup e) (⋯.monodromy γ' e) • ↑(⋯.monodromy γ e)
Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor

Goal state before:
pp: case e_f
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
m : Fin (Module.finrank ℝ E)
⊢ w m ⊗ₜ[ℝ] w m = (if m = m then 1 else 0) • w m ⊗ₜ[ℝ] w m

pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
m : Fin (Module.finrank ℝ E)
⊢ ∀ (x : Fin (Module.finrank ℝ E)), x ≠ m → ⟪w m, w x⟫_ℝ • w m ⊗ₜ[ℝ] w x = 0

Tactic:
· simp only [↓reduceIte, one_smul]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
m : Fin (Module.finrank ℝ E)
⊢ ∀ (x : Fin (Module.finrank ℝ E)), x ≠ m → ⟪w m, w x⟫_ℝ • w m ⊗ₜ[ℝ] w x = 0
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ Differentiable ℂ (interpStrip f)

Tactic:
intro z

Goal state after:
case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (interpStrip f) z
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
⊢ ∀ (z : ℂ), z.re = 0 → ‖f (↑l + z * (↑u - ↑l))‖ ≤ a

Tactic:
intro z

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
z : ℂ
⊢ z.re = 0 → ‖f (↑l + z * (↑u - ↑l))‖ ≤ a
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
⊢ ∀ (z : ℂ), z.re = 1 → ‖f (↑l + z * (↑u - ↑l))‖ ≤ b

Tactic:
intro z

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
z : ℂ
⊢ z.re = 1 → ‖f (↑l + z * (↑u - ↑l))‖ ≤ b
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ ∀ ⦃x : ℂ⦄, x ∈ verticalStrip 0 1 → ↑l + x • (↑u - ↑l) ∈ verticalStrip l u

Tactic:
intro z

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
z : ℂ
⊢ z ∈ verticalStrip 0 1 → ↑l + z • (↑u - ↑l) ∈ verticalStrip l u
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 : E → F
x : E
s : Set E
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ (Δ[s] -f) x = -(Δ[s] f) x

Tactic:
by
  simp only [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs hx]
  rw [iteratedFDerivWithin_neg_apply hs hx]
  aesop

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
⊢ ∀ (z w : ℂ), f z = f w

Tactic:
intro z

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
z : ℂ
⊢ ∀ (w : ℂ), f z = f w
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 = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x

Tactic:
rcases le_or_gt a b with h | h
  · rw [setAverage_eq, uIoc_of_le h, Real.volume_real_Ioc_of_le h, integral_of_le h]
  · rw [setAverage_eq, uIoc_of_ge h.le, Real.volume_real_Ioc_of_le h.le, integral_of_ge h.le,
      smul_neg, ← neg_smul, ← inv_neg, neg_sub]

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

Goal state before:
pp: case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
inst✝ : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
⊢ ∀ z ∈ univ, HasDerivAt (fun x ↦ wedgeIntegral 0 x f) (f z) z

Tactic:
intro z

Goal state after:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
inst✝ : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
z : ℂ
⊢ z ∈ univ → HasDerivAt (fun x ↦ wedgeIntegral 0 x f) (f z) z
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: case right.hs'
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)
x : ℂ
hx : x ∈ ball z R
⊢ UniqueDiffOn ℝ (ball z R)

pp: case right.hf'
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)
x : ℂ
hx : x ∈ ball z R
⊢ EqOn (fderivWithin ℝ (⇑reCLM ∘ F) (ball z R)) (fderivWithin ℝ f (ball z R)) (ball z R)

pp: case right.hx
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)
x : ℂ
hx : x ∈ ball z R
⊢ z ∈ ball z R

pp: case right.hfgx
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)
x : ℂ
hx : x ∈ ball z R
⊢ (⇑reCLM ∘ F) z = f z

pp: case right.a
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)
x : ℂ
hx : x ∈ ball z R
⊢ x ∈ ball z R

Tactic:
· exact isOpen_ball.uniqueDiffOn

Goal state after:
case right.hf'
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)
x : ℂ
hx : x ∈ ball z R
⊢ EqOn (fderivWithin ℝ (⇑reCLM ∘ F) (ball z R)) (fderivWithin ℝ f (ball z R)) (ball z R)

case right.hx
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)
x : ℂ
hx : x ∈ ball z R
⊢ z ∈ ball z R

case right.hfgx
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)
x : ℂ
hx : x ∈ ball z R
⊢ (⇑reCLM ∘ F) z = f z

case right.a
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)
x : ℂ
hx : x ∈ ball z R
⊢ x ∈ ball z R
Module: Mathlib.Analysis.Complex.MeanValue

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
⊢ EqOn (fun z ↦ (z - c)⁻¹ • ((z - c) * (z - w)⁻¹) • f z) (fun z ↦ (z - w)⁻¹ • f z) (sphere c |R|)

Tactic:
intro z

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
z : ℂ
⊢ z ∈ sphere c |R| → (fun z ↦ (z - c)⁻¹ • ((z - c) * (z - w)⁻¹) • f z) z = (fun z ↦ (z - w)⁻¹ • f z) z
Module: Mathlib.Analysis.Complex.MeanValue

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hw : w ∈ ball c |R|
hR : ¬|R| ≤ 0
⊢ ∀ z ∈ ball c |R| \ ∅, DifferentiableAt ℂ f z

Tactic:
intro z

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hw : w ∈ ball c |R|
hR : ¬|R| ≤ 0
z : ℂ
⊢ z ∈ ball c |R| \ ∅ → DifferentiableAt ℂ f z
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case inr.refine_3
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
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℂ
hζ : ζ.im = π / 2
⊢ ‖f (cexp (↑ζ.re + ↑(π / 2) * I))‖ ≤ C

Tactic:
exp_add_mul_I,

Goal state after:
case inr.refine_3
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
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℂ
hζ : ζ.im = π / 2
⊢ ‖f (cexp ↑ζ.re * (cos ↑(π / 2) + sin ↑(π / 2) * I))‖ ≤ C
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 (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
⊢ ‖(f ∘ fun x ↦ x * I) z‖ ≤ C

Tactic:
have H : MapsTo (· * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0) := fun w hw ↦ by
    simpa only [mem_reProdIm, mul_I_re, mul_I_im, neg_lt_zero, mem_Iio] using! hw.symm

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun x ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
⊢ ‖(f ∘ fun x ↦ x * I) z‖ ≤ C
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 (⇑reCLM ∘ fun z ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z) c R = f w

Tactic:
reCLM.circleAverage_comp_comm,

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 (circleAverage (fun z ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z) c R) = 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: τ τ' : ℍ
hre : τ.re = τ'.re
hnorm : ‖↑τ‖ = ‖↑τ'‖
⊢ τ = τ'

Tactic:
by
  apply_fun (· ^ 2) at hnorm
  simpa [UpperHalfPlane.ext_iff, Complex.ext_iff, hre, Complex.normSq, Complex.sq_norm,
    ← pow_two, pow_left_inj₀ τ.im_pos.le τ'.im_pos.le two_ne_zero] using hnorm

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

Goal state before:
pp: case hs
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ ∀ r ∈ Set.Ioc ‖w - c‖ R, 0 ≤ r

Tactic:
grind [norm_nonneg (w - c)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: case neg
x : ℝ
hx : ¬x = 0
⊢ ContinuousAt (dslope sin 0) x

Tactic:
· 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₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
⊢ ball (↑x₀) (dist 0 ↑x₀) ⊆ {z | 0 < z.re}

Tactic:
intro z

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'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
z : ℂ
⊢ z ∈ ball (↑x₀) (dist 0 ↑x₀) → z ∈ {z | 0 < z.re}
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
⊢ log⁺ ↑n = log ↑n

Tactic:
simp [posLog_eq_log, Nat.one_le_iff_ne_zero.2 hn]

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

Goal state before:
pp: case neg
n : ℕ
x : ℝ
hn : ¬n = 0
hx : 1 < |x|
this : 1 ≤ |x ^ n|
⊢ log⁺ (x ^ n) = ↑n * log⁺ x

Tactic:
simp [posLog_eq_log this, posLog_eq_log hx.le]

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

Goal state before:
pp: case hderiv.refine_1.inr
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hc : 0 ≤ c
⊢ x ≠ 0

Tactic:
rw [min_eq_left hc] at hx

Goal state after:
case hderiv.refine_1.inr
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo 0 (max 0 c)
hc : 0 ≤ c
⊢ x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case e'_3
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (r + 1)⁻¹ * (b ^ (r + 1) - a ^ (r + 1)) = (r + 1)⁻¹ * (↑b ^ ↑(r + 1) - ↑a ^ ↑(r + 1)).re

Tactic:
Complex.sub_re,

Goal state after:
case e'_3
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (r + 1)⁻¹ * (b ^ (r + 1) - a ^ (r + 1)) = (r + 1)⁻¹ * ((↑b ^ ↑(r + 1)).re - (↑a ^ ↑(r + 1)).re)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ι a b, |x - a| ^ n = ∫ (x : ℝ) in a..b, |x - a| ^ n

Tactic:
uIoc_of_le hab,

Goal state after:
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Set.Ioc a b, |x - a| ^ n = ∫ (x : ℝ) in a..b, |x - a| ^ n
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
⊢ Set.EqOn (fun x ↦ log ‖x - a‖) (fun x ↦ log ‖1 - x⁻¹ * a‖) (sphere 0 |1|)

Tactic:
intro z

Goal state after:
a : ℂ
h : ‖a‖ < 1
z : ℂ
⊢ z ∈ sphere 0 |1| → (fun x ↦ log ‖x - a‖) z = (fun x ↦ log ‖1 - x⁻¹ * a‖) z
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
x : ℂ
hx : x ∈ closedBall 0 |1|
this : ‖x * a‖ < 1
hCon : 1 = x * a
⊢ False

Tactic:
rwa [← hCon, CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, lt_self_iff_false] at this

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

Goal state before:
pp: a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun y ↦ Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x) * c / c) x

Tactic:
apply ((Complex.hasDerivAt_exp _).comp x _).div_const c

Goal state after:
a b : ℝ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun x ↦ c * ↑x) c x
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
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 : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
⊢ ∀ (z : ℂ), 0 < z.re → f z = 0

Tactic:
intro z

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
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 : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
⊢ 0 < z.re → f z = 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
ha : 1 < a
hb : 1 < b
this : ∫ (t : ℝ) in a..b, deriv (fun t ↦ (log t)⁻¹) t = (log b)⁻¹ - (log a)⁻¹
⊢ ∫ (t : ℝ) in a..b, t⁻¹ / log t ^ 2 = (log a)⁻¹ - (log b)⁻¹

Tactic:
simp_rw [deriv_inv_log, neg_div, intervalIntegral.integral_neg] at this
    linarith

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

Goal state before:
pp: a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y ↦ 1 + y ^ 2) (2 * ↑x) ↑x
⊢ ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z

Tactic:
intro z

Goal state after:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y ↦ 1 + y ^ 2) (2 * ↑x) ↑x
z : ℂ
⊢ 0 < z.re → HasDerivAt (fun z ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ ∀ z ∈ sphere 0 |1|, ∃ t ∈ nhds z, (t ∩ (sphere 0 |1| \ {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0})).Finite

Tactic:
intro z

Goal state after:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
⊢ z ∈ sphere 0 |1| → ∃ t ∈ nhds z, (t ∩ (sphere 0 |1| \ {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0})).Finite
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

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

Tactic:
rw [← Pi.add_def, circleAverage_add (circleIntegrable_const (log ‖R‖) 0 1)
      (MeromorphicOn.circleIntegrable_log_norm (fun _ _ ↦ by fun_prop)), circleAverage_const]

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

Goal state before:
pp: P : ℂ[X]
h₀ : 0 < P.degree
⊢ (derivative P).rootSet ℂ ⊆ (convexHull ℝ) (P.rootSet ℂ)

Tactic:
intro z

Goal state after:
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
⊢ z ∈ (derivative P).rootSet ℂ → z ∈ (convexHull ℝ) (P.rootSet ℂ)
Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
⊢ Irreducible p

Tactic:
by
  refine hp.irreducible_of_coprime fun q hq hq' => ?_
  suffices ¬0 < q.natDegree by
    rcases hq with ⟨p, rfl⟩
    replace hp := hp.leadingCoeff_isUnit
    rw [leadingCoeff_mul] at hp
    replace hp := isUnit_of_mul_isUnit_left hp
    rw [not_lt, Nat.le_zero] at this
    rwa [eq_C_of_natDegree_eq_zero this, isUnit_C, ← this]
  intro hq''
  rw [natDegree_pos_iff_degree_pos] at hq''
  rw [← degree_map_eq_of_injective (algebraMap ℤ ℂ).injective_int] at hq''
  obtain ⟨z, hz⟩ := Complex.exists_root hq''
  rw [IsRoot, eval_map_algebraMap] at hz
  refine h z ⟨?_, ?_⟩
  · obtain ⟨g', hg'⟩ := hq
    rw [hg', aeval_mul, hz, zero_mul]
  · obtain ⟨g', hg'⟩ := hq'
    rw [hg', aeval_mul, hz, zero_mul]

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
⊢ ∀ z ∈ U, f z ≠ 0

Tactic:
intro z

Goal state after:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
z : ℂ
⊢ z ∈ U → f z ≠ 0
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
⊢ ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z

Tactic:
intro z

Goal state after:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
z : ℂ
⊢ z ∈ U → HasStrictDerivAt f (2 * f z)⁻¹ z