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

Goal state before:
pp: f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
        I • fderiv ℝ (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I) x)
      I =
    I •
      (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
          I • fderiv ℝ (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I) x)
        1

pp: case hg
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1)

pp: case hf
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (fun x ↦ (fderiv ℝ f x) 1) x

Tactic:
]

Goal state after:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
        I • fderiv ℝ (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I) x)
      I =
    I •
      (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
          I • fderiv ℝ (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I) x)
        1

case hg
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1)

case hf
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (fun x ↦ (fderiv ℝ f x) 1) x
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: 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
⊢ Filter.Tendsto f (𝓝 z) (𝓝 (f z))

Tactic:
]

Goal state after:
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
⊢ Filter.Tendsto f (𝓝 z) (𝓝 (f z))
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
⊢ ∑ i, (-iteratedFDerivWithin ℝ 2 f s x) ![(stdOrthonormalBasis ℝ E) i, (stdOrthonormalBasis ℝ E) i] =
    -∑ i, (iteratedFDerivWithin ℝ 2 f s x) ![(stdOrthonormalBasis ℝ E) i, (stdOrthonormalBasis ℝ E) i]

Tactic:
]

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
s : Set E
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ ∑ i, (-iteratedFDerivWithin ℝ 2 f s x) ![(stdOrthonormalBasis ℝ E) i, (stdOrthonormalBasis ℝ E) i] =
    -∑ i, (iteratedFDerivWithin ℝ 2 f s x) ![(stdOrthonormalBasis ℝ E) i, (stdOrthonormalBasis ℝ E) i]
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: 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
this : ∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.IsBigOWith c (𝓝 z) (fun w ↦ f w - f z) fun x ↦ 1
⊢ ∀ ⦃c : ℝ⦄,
    0 < c → Asymptotics.IsBigOWith c (𝓝 z) (fun w ↦ ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) - f z) fun w ↦ w - z

Tactic:
]

Goal state after:
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
this : ∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.IsBigOWith c (𝓝 z) (fun w ↦ f w - f z) fun x ↦ 1
⊢ ∀ ⦃c : ℝ⦄,
    0 < c → Asymptotics.IsBigOWith c (𝓝 z) (fun w ↦ ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I) - f z) fun w ↦ w - z
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: 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
ε : ℝ
ε_pos : 0 < ε
this : ∃ i, 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ‖f x - f z‖ ≤ ε
⊢ ∃ i, 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ∀ y ∈ Ι z.im x.im, ‖f (↑x.re + ↑y * I) - f z‖ ≤ ε

Tactic:
]

Goal state after:
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
ε : ℝ
ε_pos : 0 < ε
this : ∃ i, 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ‖f x - f z‖ ≤ ε
⊢ ∃ i, 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ∀ y ∈ Ι z.im x.im, ‖f (↑x.re + ↑y * I) - f z‖ ≤ ε
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ Δ[s] f₁ - f₂ =ᶠ[𝓝[insert x s] x] (Δ[s] f₁) - Δ[s] f₂

Tactic:
]

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ Δ[s] f₁ - f₂ =ᶠ[𝓝[insert x s] x] (Δ[s] f₁) - Δ[s] f₂
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
        I • fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) I) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) I) x)
      I =
    I •
      (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
          I • fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) I) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) I) x)
        1

pp: case hg
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (⇑ofRealCLM) ((fderiv ℝ f x) I)

pp: case hf
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (fun x ↦ (fderiv ℝ f x) I) x

Tactic:
]

Goal state after:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
        I • fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) I) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) I) x)
      I =
    I •
      (fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) 1) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) 1) x -
          I • fderiv ℝ (⇑ofRealCLM) ((fderiv ℝ f x) I) ∘SL fderiv ℝ (fun x ↦ (fderiv ℝ f x) I) x)
        1

case hg
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (⇑ofRealCLM) ((fderiv ℝ f x) I)

case hf
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (fun x ↦ (fderiv ℝ f x) I) x
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
h₃y : y ∈ s
⊢ (Δ[s] f₁ - f₂) y = ((Δ[s] f₁) - Δ[s] f₂) y

Tactic:
]

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
h₃y : y ∈ s
⊢ (Δ[s] f₁ - f₂) y = ((Δ[s] f₁) - Δ[s] f₂) y
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: 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)
⊢ (fun x' ↦ c.wedgeIntegral x' f - c.wedgeIntegral z f - (x' - z) • f z) =o[𝓝 z] fun x' ↦ x' - z

Tactic:
]

Goal state after:
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)
⊢ (fun x' ↦ c.wedgeIntegral x' f - c.wedgeIntegral z f - (x' - z) • f z) =o[𝓝 z] fun x' ↦ x' - z
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: case 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 - z = w - z

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F →L[ℝ] G
h : ContDiffAt ℝ 2 f x
a : E
ha : ContDiffAt ℝ 2 f a
⊢ (⇑l ∘ Δ f) a = (⇑l ∘ Δ f) a

Tactic:
]

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

Goal state before:
pp: case hb
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
h_bound : ∃ C, ∀ x ∈ range f, ‖x‖ ≤ C
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun z ↦ (F z).re) = f
⊢ ∃ C, ∀ x ∈ range fun z ↦ cexp (F z), ‖x‖ ≤ C

Tactic:
]

Goal state after:
case hb
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
h_bound : ∃ C, ∀ x ∈ range f, ‖x‖ ≤ C
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun z ↦ (F z).re) = f
⊢ ∃ C, ∀ x ∈ range fun z ↦ cexp (F z), ‖x‖ ≤ C
Module: Mathlib.Analysis.Complex.Harmonic.Liouville

Goal state before:
pp: case h
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun z ↦ (F z).re) = f
M : ℝ
hM : ∀ (a : ℂ), |(fun z ↦ (F z).re) a| ≤ M
⊢ ∀ (a : ℂ), (F a).re ≤ M

Tactic:
]

Goal state after:
case h
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun z ↦ (F z).re) = f
M : ℝ
hM : ∀ (a : ℂ), |(fun z ↦ (F z).re) a| ≤ M
⊢ ∀ (a : ℂ), (F a).re ≤ M
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: case calc_2
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)
⊢ I₁ + I • I₂ - ((↑w.re - ↑z.re) • f z + ((↑w.im - ↑z.im) * I) • f z) =
    I₁ - (↑w.re - ↑z.re) • f z + (I • I₂ - ((↑w.im - ↑z.im) * I) • f z)

Tactic:
]

Goal state after:
case calc_2
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)
⊢ I₁ + I • I₂ - ((↑w.re - ↑z.re) • f z + ((↑w.im - ↑z.im) * I) • f z) =
    I₁ - (↑w.re - ↑z.re) • f z + (I • I₂ - ((↑w.im - ↑z.im) * I) • f z)
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 : ℂ
ℓ : StrongDual ℝ E
h₁ℓ : ‖ℓ‖ ≤ 1
h₂ℓ : ℓ (f z) - ℓ (f w) = ‖f z - f w‖
⊢ f z = f w

Tactic:
]

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 : ℂ
ℓ : StrongDual ℝ E
h₁ℓ : ‖ℓ‖ ≤ 1
h₂ℓ : ℓ (f z) - ℓ (f w) = ‖f z - f w‖
⊢ f z = f w
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ ↑((fderiv ℝ f x ∘SL fderiv ℝ (fun x ↦ 1) x + (fderiv ℝ (fderiv ℝ f) x).flip 1) I) -
      I * ↑((fderiv ℝ f x ∘SL fderiv ℝ (fun x ↦ I) x + (fderiv ℝ (fderiv ℝ f) x).flip I) I) =
    I * ↑((fderiv ℝ f x ∘SL fderiv ℝ (fun x ↦ 1) x + (fderiv ℝ (fderiv ℝ f) x).flip 1) 1) -
      I ^ 2 * ↑((fderiv ℝ f x ∘SL fderiv ℝ (fun x ↦ I) x + (fderiv ℝ (fderiv ℝ f) x).flip I) 1)

Tactic:
]

Goal state after:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ ↑((fderiv ℝ f x ∘SL fderiv ℝ (fun x ↦ 1) x + (fderiv ℝ (fderiv ℝ f) x).flip 1) I) -
      I * ↑((fderiv ℝ f x ∘SL fderiv ℝ (fun x ↦ I) x + (fderiv ℝ (fderiv ℝ f) x).flip I) I) =
    I * ↑((fderiv ℝ f x ∘SL fderiv ℝ (fun x ↦ 1) x + (fderiv ℝ (fderiv ℝ f) x).flip 1) 1) -
      I ^ 2 * ↑((fderiv ℝ f x ∘SL fderiv ℝ (fun x ↦ I) x + (fderiv ℝ (fderiv ℝ f) x).flip I) 1)
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 : ℂ
ℓ : StrongDual ℝ E
h₁ℓ : ‖ℓ‖ ≤ 1
h₂ℓ : ℓ (f z) - ℓ (f w) = ‖f z - f w‖
η₁ : IsBounded (range (⇑ℓ ∘ f))
⊢ ℓ (f z) - ℓ (f w) = 0

Tactic:
]

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 : ℂ
ℓ : StrongDual ℝ E
h₁ℓ : ‖ℓ‖ ≤ 1
h₂ℓ : ℓ (f z) - ℓ (f w) = ‖f z - f w‖
η₁ : IsBounded (range (⇑ℓ ∘ f))
⊢ ℓ (f z) - ℓ (f w) = 0
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
⊢ (volume.real (Ι b a))⁻¹ • ∫ (x : ℝ) in Ι b a, f x = (volume.real (Ι b a))⁻¹ • ∫ (x : ℝ) in Ι b a, f x

Tactic:
]

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

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : a ≤ b
⊢ (b - a)⁻¹ • ∫ (x : ℝ) in Ioc a b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in Ioc a b, f x ∂volume

Tactic:
]

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

Goal state before:
pp: f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ ↑(((fderiv ℝ (fderiv ℝ f) x) I) 1) + -(I * ↑(((fderiv ℝ (fderiv ℝ f) x) I) I)) =
    ↑(((fderiv ℝ (fderiv ℝ f) x) 1) I) + I * ↑(((fderiv ℝ (fderiv ℝ f) x) 1) 1)

Tactic:
]

Goal state after:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
⊢ ↑(((fderiv ℝ (fderiv ℝ f) x) I) 1) + -(I * ↑(((fderiv ℝ (fderiv ℝ f) x) I) I)) =
    ↑(((fderiv ℝ (fderiv ℝ f) x) 1) I) + I * ↑(((fderiv ℝ (fderiv ℝ f) x) 1) 1)
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ (a - b)⁻¹ • ∫ (x : ℝ) in Ioc b a, f x = (a - b)⁻¹ • ∫ (x : ℝ) in Ioc b a, f x ∂volume

Tactic:
]

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
⊢ (b - a)⁻¹ * ∫ (x : ℝ) in a..b, f x = (b - a)⁻¹ * ∫ (x : ℝ) in a..b, f x

Tactic:
]

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 ×ℂ 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
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
hzne : z ≠ 0
⊢ z.arg ∈ Icc 0 (π / 2)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
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
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
hzne : z ≠ 0
⊢ z.arg ∈ Icc 0 (π / 2)
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: a b : ℝ
f₁ f₂ : ℝ → ℝ
hf : f₁ =ᶠ[Filter.codiscreteWithin (Ι a b)] f₂
⊢ ⨍ (x : ℝ) in a..b, f₂ x = ⨍ (x : ℝ) in a..b, f₂ x

Tactic:
]

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᵐ[μ] Ι a b
⊢ μ (Ι a b) = μ (Ι a b)

Tactic:
]

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᵐ[μ] Ι a b
hμ : μ s = μ (Ι a b)
⊢ μ (Ι a b) ≠ 0

Tactic:
]

Goal state after:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᵐ[μ] Ι a b
hμ : μ s = μ (Ι a b)
⊢ μ (Ι a b) ≠ 0
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᵐ[μ] Ι a b
hμ0' : μ s ≠ 0
c : ℝ
hc : c ∈ uIoo a b
heq : f c = ⨍ (x : ℝ) in uIoo a b, f x ∂μ
⊢ f c = ⨍ (x : ℝ) in s, f x ∂μ

Tactic:
]

Goal state after:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
h : a ≠ b
s : Set ℝ := uIoo a b
hs' : s ⊆ Ι a b
hs_ev : s =ᵐ[μ] Ι a b
hμ0' : μ s ≠ 0
c : ℝ
hc : c ∈ uIoo a b
heq : f c = ⨍ (x : ℝ) in uIoo a b, f x ∂μ
⊢ f c = ⨍ (x : ℝ) in s, f x ∂μ
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 (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)
⊢ 0 < expR z.re * Real.cos z.im ∧ 0 < expR z.re * Real.sin z.im

Tactic:
]

Goal state after:
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)
⊢ 0 < expR z.re * Real.cos z.im ∧ 0 < expR z.re * Real.sin z.im
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: case right
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)
⊢ EqOn (⇑reCLM ∘ F) f (ball z R)

Tactic:
]

Goal state after:
case right
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)
⊢ EqOn (⇑reCLM ∘ F) f (ball z R)
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case inr.refine_1
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)
⊢ ∃ c < 2, ∃ B, (f ∘ cexp) =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))] fun z ↦ expR (B * expR (c * |z.re|))

Tactic:
]

Goal state after:
case inr.refine_1
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)
⊢ ∃ c < 2, ∃ B, (f ∘ cexp) =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))] fun z ↦ expR (B * expR (c * |z.re|))