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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
t₁ : (support fun u x ↦ ↑(D u) * log ‖x - u‖) = D.support
h₃f : D.support.Finite
z : 𝕜
hz : f z = ((∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g) z
h₂z : D z = 0
h₃z : z ∈ U
⊢ ∀ x ∈ h₃f.toFinset, ‖z - x‖ ^ D x ≠ 0

Tactic:
intro x

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
t₁ : (support fun u x ↦ ↑(D u) * log ‖x - u‖) = D.support
h₃f : D.support.Finite
z : 𝕜
hz : f z = ((∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g) z
h₂z : D z = 0
h₃z : z ∈ U
x : 𝕜
⊢ x ∈ h₃f.toFinset → ‖z - x‖ ^ D x ≠ 0
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
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
a : ℂ
ha : a ∈ (-divisor f (ball 0 R)).supportᶜ
h₂a : a ∈ closedBall 0 R
⊢ ∀ x ∈ η₀.toFinset,
    canonicalFactor R x a ^ (-(divisor f (ball 0 R)) x) • canonicalFactor R x a ^ (divisor f (ball 0 R)) x = 1

Tactic:
intro x

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
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
a : ℂ
ha : a ∈ (-divisor f (ball 0 R)).supportᶜ
h₂a : a ∈ closedBall 0 R
x : ℂ
⊢ x ∈ η₀.toFinset →
    canonicalFactor R x a ^ (-(divisor f (ball 0 R)) x) • canonicalFactor R x a ^ (divisor f (ball 0 R)) x = 1
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖map 1‖ ≠ 0
⊢ ∀ (x : ℂ), ‖(‖map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖

Tactic:
intro x

Goal state after:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖map 1‖ ≠ 0
x : ℂ
⊢ ‖(‖map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = fderiv ℝ f z ∘SL ↑conjCLE) ↔
    DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)

Tactic:
have h_diff := h.imp_symm fderiv_zero_of_not_differentiableAt

Goal state after:
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = fderiv ℝ f z ∘SL ↑conjCLE) ↔
    DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ {x | AnalyticAt 𝕜 f x}))

Tactic:
intro x

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
⊢ x ∈ U → Disjoint (𝓝[≠] x) (𝓟 (U \ {x | AnalyticAt 𝕜 f x}))
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ Subtype.val '' {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤}))

Tactic:
intro x

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
⊢ x ∈ U → Disjoint (𝓝[≠] x) (𝓟 (U \ Subtype.val '' {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤}))
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ (rexp 1)⁻¹ < 0.3678794412

Tactic:
inv_lt_comm₀ (exp_pos _) (by norm_num)

Goal state after:
⊢ 0.3678794412⁻¹ < rexp 1
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
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
⊢ ((∏ i ∈ t₂, meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
        ∏ i ∈ t₁, meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) •
      meromorphicTrailingCoeffAt
          ((∏ i ∈ t₂, canonicalFactor R i ^ (-(divisor f B₀R) i)) * ∏ i ∈ t₁, (fun x ↦ x - i) ^ (divisor f S₀R) i) w •
        meromorphicTrailingCoeffAt h w =
    ((∏ i ∈ t₂, meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
        ∏ i ∈ t₁, meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) •
      ((∏ n ∈ t₂, meromorphicTrailingCoeffAt (canonicalFactor R n ^ (-(divisor f B₀R) n)) w) *
          ∏ n ∈ t₁, meromorphicTrailingCoeffAt ((fun x ↦ x - n) ^ (divisor f S₀R) n) w) •
        h w

Tactic:
MeromorphicAt.meromorphicTrailingCoeffAt_mul (by fun_prop) (by fun_prop),

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
⊢ ((∏ i ∈ t₂, meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
        ∏ i ∈ t₁, meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) •
      (meromorphicTrailingCoeffAt (∏ i ∈ t₂, canonicalFactor R i ^ (-(divisor f B₀R) i)) w *
          meromorphicTrailingCoeffAt (∏ i ∈ t₁, (fun x ↦ x - i) ^ (divisor f S₀R) i) w) •
        meromorphicTrailingCoeffAt h w =
    ((∏ i ∈ t₂, meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
        ∏ i ∈ t₁, meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) •
      ((∏ n ∈ t₂, meromorphicTrailingCoeffAt (canonicalFactor R n ^ (-(divisor f B₀R) n)) w) *
          ∏ n ∈ t₁, meromorphicTrailingCoeffAt ((fun x ↦ x - n) ^ (divisor f S₀R) n) w) •
        h w
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
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
⊢ (((∏ i ∈ t₂, meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
          ∏ i ∈ t₁, meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) *
        ((∏ n ∈ t₂, meromorphicTrailingCoeffAt (canonicalFactor R n ^ (-(divisor f B₀R) n)) w) *
          ∏ n ∈ t₁, meromorphicTrailingCoeffAt ((fun x ↦ x - n) ^ (divisor f S₀R) n) w)) •
      h w =
    h w

Tactic:
mul_mul_mul_comm,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
⊢ (((∏ i ∈ t₂, meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
          ∏ n ∈ t₂, meromorphicTrailingCoeffAt (canonicalFactor R n ^ (-(divisor f B₀R) n)) w) *
        ((∏ i ∈ t₁, meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) *
          ∏ n ∈ t₁, meromorphicTrailingCoeffAt ((fun x ↦ x - n) ^ (divisor f S₀R) n) w)) •
      h w =
    h w
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
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
⊢ ∀ x ∈ t₂,
    meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ (divisor f B₀R) x *
        meromorphicTrailingCoeffAt (canonicalFactor R x ^ (-(divisor f B₀R) x)) w =
      1

Tactic:
intro x

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
x : ℂ
⊢ x ∈ t₂ →
    meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ (divisor f B₀R) x *
        meromorphicTrailingCoeffAt (canonicalFactor R x ^ (-(divisor f B₀R) x)) w =
      1
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
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
⊢ ∀ x ∈ t₁,
    meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ^ (-divisor f S₀R) x *
        meromorphicTrailingCoeffAt ((fun x_1 ↦ x_1 - x) ^ (divisor f S₀R) x) w =
      1

Tactic:
intro x

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
x : ℂ
⊢ x ∈ t₁ →
    meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ^ (-divisor f S₀R) x *
        meromorphicTrailingCoeffAt ((fun x_1 ↦ x_1 - x) ^ (divisor f S₀R) x) w =
      1
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
h₃x : ¬(divisor f (ball 0 R)) w = 0
h₁x : w ∈ ball 0 R
⊢ False

Tactic:
exact h₃x (by simp [(D.meromorphicOn.mono_set ball_subset_closedBall).divisor_apply h₁x, h₂w])

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

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
⊢ ∀ x ∈ re ⁻¹' Ioo 0 1, ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖

Tactic:
intro x

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
x : ℂ
⊢ x ∈ re ⁻¹' Ioo 0 1 → ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f (↑x + ↑c.im * I)
I₂ : E := I • ∫ (y : ℝ) in c.im..w.im, f (↑w.re + ↑y * I)
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f (↑x + ↑c.im * I)
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f

Tactic:
set I₄ := I • ∫ y in c.im..z.im, f (z.re + y * I)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f (↑x + ↑c.im * I)
I₂ : E := I • ∫ (y : ℝ) in c.im..w.im, f (↑w.re + ↑y * I)
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f (↑x + ↑c.im * I)
I₄ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑z.re + ↑y * I)
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ * ((ε + sSupNormIm f 0) ^ (1 - z.re)) ^ (-1) * ((ε + sSupNormIm f 1) ^ z.re) ^ (-1) ≤ 1

Tactic:
simp only [← Real.rpow_mul (le_of_lt (sSupNormIm_eps_pos f hε _)),
    mul_neg, mul_one, neg_sub, mul_assoc]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ * ((ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)) ≤ 1
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ ∀ x ∈ Ioi 0,
    (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
      ‖↑(x + sSupNormIm f 0) ^ (1 - z) * ↑(x + sSupNormIm f 1) ^ z‖

Tactic:
intro x

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
⊢ x ∈ Ioi 0 →
    (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
      ‖↑(x + sSupNormIm f 0) ^ (1 - z) * ↑(x + sSupNormIm f 1) ^ z‖
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

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

Tactic:
div_eq_inv_mul

Goal state after:
f : ℝ → ℝ
a b : ℝ
⊢ (b - a)⁻¹ * ∫ (x : ℝ) in a..b, f x = (b - a)⁻¹ * ∫ (x : ℝ) in a..b, f x
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
⊢ s ⊆ Ι a b

Tactic:
intro x

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
x : ℝ
⊢ x ∈ s → x ∈ Ι a b
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:
intro x

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)
x : ℂ
⊢ x ∈ ball z R → (⇑reCLM ∘ F) x = f x
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: case right.hg
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
⊢ DifferentiableOn ℝ f (ball z R)

Tactic:
exact fun y hy ↦ (ContDiffAt.differentiableAt (hf y hy).1 two_ne_zero).differentiableWithinAt

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 : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F✝
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + |R|) ⊆ {x | HarmonicAt (⇑g ∘ f) x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + |R|))
h₂F : Set.EqOn (fun z ↦ (F z).re) (⇑g ∘ f) (ball c (e + |R|))
⊢ DifferentiableOn ℂ F (closure (ball c |R|))

Tactic:
intro x

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✝
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + |R|) ⊆ {x | HarmonicAt (⇑g ∘ f) x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + |R|))
h₂F : Set.EqOn (fun z ↦ (F z).re) (⇑g ∘ f) (ball c (e + |R|))
x : ℂ
⊢ x ∈ closure (ball c |R|) → DifferentiableWithinAt ℂ F (closure (ball c |R|)) x
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
s : Set ℝ
c : ℂ
hf : ContinuousOn f {z | ‖z - c‖ ∈ s}
hs : ∀ r ∈ s, 0 ≤ r
⊢ ContinuousOn (Real.circleAverage f c) s

Tactic:
by
  rw [continuousOn_iff_continuous_domRestrict] at *
  apply (intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' _ _ _).const_smul
  have (x : s × ℝ) : circleMap c x.1 x.2 ∈ {z | ‖z - c‖ ∈ s} := by
    simp [abs_of_nonneg (hs x.1 (Subtype.coe_prop x.1))]
  apply hf.comp (f := (fun x ↦ ⟨circleMap c x.1 x.2, this x⟩))
  fun_prop

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

Goal state before:
pp: f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
ε : ℝ
h₁ε : ε > 0
h₂ε : ball x ε ⊆ {x | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball x ε)
h₂F : EqOn (fun z ↦ (F z).re) f (ball x ε)
⊢ AnalyticAt ℝ f x

Tactic:
analyticAt_congr (Filter.eventually_of_mem (ball_mem_nhds x h₁ε) (fun y hy ↦ h₂F.symm hy))

Goal state after:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
ε : ℝ
h₁ε : ε > 0
h₂ε : ball x ε ⊆ {x | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball x ε)
h₂F : EqOn (fun z ↦ (F z).re) f (ball x ε)
⊢ AnalyticAt ℝ (fun y ↦ (F y).re) x
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
g : StrongDual ℝ F
hR : ¬R = 0
⊢ {z | ‖z - c‖ ∈ Set.Ioc 0 |R|} ⊆ closure (ball c |R|)

Tactic:
intro x

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
hR : ¬R = 0
x : ℂ
⊢ x ∈ {z | ‖z - c‖ ∈ Set.Ioc 0 |R|} → x ∈ closure (ball c |R|)
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))
⊢ DifferentiableOn ℂ F (closure (ball c R))

Tactic:
intro x

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))
x : ℂ
⊢ x ∈ closure (ball c R) → DifferentiableWithinAt ℂ F (closure (ball c R)) x
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))
⊢ Set.EqOn (re ∘ herglotzRieszKernel c w • f) (⇑reCLM ∘ fun z ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c R)

Tactic:
intro x

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))
x : ℂ
⊢ x ∈ sphere c R →
    (re ∘ herglotzRieszKernel c w • f) x = (⇑reCLM ∘ fun z ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z) x
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
h₁w : ¬‖w - c‖ = 0
⊢ 0 < ‖w - c‖

Tactic:
simpa using h₁w

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

Goal state before:
pp: ⊢ ∀ (x : ℝ), ContinuousAt (fun x ↦ x * log x) x

Tactic:
intro x

Goal state after:
x : ℝ
⊢ ContinuousAt (fun x ↦ x * log x) x
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: ⊢ Set.EqOn (deriv fun x ↦ x * log x) (fun x ↦ log x + 1) (Set.Ioi 0)

Tactic:
intro x

Goal state after:
x : ℝ
⊢ x ∈ Set.Ioi 0 → deriv (fun x ↦ x * log x) x = (fun x ↦ log x + 1) x
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: case right
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y | y ≠ 0}) ∈ 𝓝 z
⊢ Set.EqOn (⇑reCLM ∘ (log ∘ ⇑conjCLE ∘ g + log ∘ g)) (⇑reCLM ∘ (⇑conjCLE ∘ log ∘ g + log ∘ g))
    (g ⁻¹' (slitPlane ∩ {0}ᶜ))

Tactic:
intro x

Goal state after:
case right
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y | y ≠ 0}) ∈ 𝓝 z
x : ℂ
⊢ x ∈ g ⁻¹' (slitPlane ∩ {0}ᶜ) →
    (⇑reCLM ∘ (log ∘ ⇑conjCLE ∘ g + log ∘ g)) x = (⇑reCLM ∘ (⇑conjCLE ∘ log ∘ g + log ∘ g)) x
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: ⊢ ∀ x ∈ interior (Set.Ici 0), 0 < deriv^[2] (fun x ↦ x * log x) x

Tactic:
intro x

Goal state after:
x : ℝ
⊢ x ∈ interior (Set.Ici 0) → 0 < deriv^[2] (fun x ↦ x * log x) x