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

Goal state before:
pp: case insert
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
x : 𝕜
σ : ι
s₁ : Finset ι
hσ : σ ∉ s₁
hind :
  (∀ σ ∈ s₁, MeromorphicAt (f σ) x) →
    meromorphicTrailingCoeffAt (∏ n ∈ s₁, f n) x = ∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x
h : ∀ σ_1 ∈ insert σ s₁, MeromorphicAt (f σ_1) x
this : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x
⊢ meromorphicTrailingCoeffAt (f σ * ∏ x ∈ s₁, f x) x =
    meromorphicTrailingCoeffAt (f σ) x * ∏ x_1 ∈ s₁, meromorphicTrailingCoeffAt (f x_1) x

Tactic:
(h σ (Finset.mem_insert_self σ s₁)).meromorphicTrailingCoeffAt_mul
      (MeromorphicAt.prod this),

Goal state after:
case insert
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
x : 𝕜
σ : ι
s₁ : Finset ι
hσ : σ ∉ s₁
hind :
  (∀ σ ∈ s₁, MeromorphicAt (f σ) x) →
    meromorphicTrailingCoeffAt (∏ n ∈ s₁, f n) x = ∏ n ∈ s₁, meromorphicTrailingCoeffAt (f n) x
h : ∀ σ_1 ∈ insert σ s₁, MeromorphicAt (f σ_1) x
this : ∀ σ₀ ∈ s₁, MeromorphicAt (f σ₀) x
⊢ meromorphicTrailingCoeffAt (f σ) x * meromorphicTrailingCoeffAt (∏ i ∈ s₁, f i) x =
    meromorphicTrailingCoeffAt (f σ) x * ∏ x_1 ∈ s₁, meromorphicTrailingCoeffAt (f x_1) x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x ≠ 0
⊢ ∀ (x_1 : E), ¬x_1 = 0 → ¬Tendsto f (𝓝[≠] x) (𝓝 x_1)

Tactic:
intro c c_ne hc

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x ≠ 0
c : E
c_ne : ¬c = 0
hc : Tendsto f (𝓝[≠] x) (𝓝 c)
⊢ False
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case neg.h₂g
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
⊢ 1 ≠ 0

pp: case neg.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
⊢ 1 =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ 0 • 1

Tactic:
· simp

Goal state after:
case neg.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
this : f⁻¹ * f =ᶠ[𝓝[≠] x] 1
⊢ 1 =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ 0 • 1
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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
h₁f₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = 0
⊢ ∀ (a : 𝕜), f₁ a = f₂ a → f₁ a = 0 → f₂ a = 0

Tactic:
by grind

Goal state after:
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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : MeromorphicAt f₁ x
n : ℤ
h₁f₁ : meromorphicOrderAt f₁ x = ↑n
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n • g z
⊢ ∀ (a : 𝕜), f₁ a = f₂ a → f₁ a = (a - x) ^ n • g a → f₂ a = (a - x) ^ n • g a

Tactic:
by grind

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

Goal state before:
pp: case refine_2
R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ ↑R ^ 2 - (starRingEnd ℂ) w * w ≠ 0

Tactic:
rw [← normSq_eq_conj_mul_self, normSq_eq_norm_sq w, sub_ne_zero, ne_eq, ← ofReal_pow,
        ofReal_inj, sq_eq_sq₀ (pos_of_mem_ball h).le (norm_nonneg w)]
      rw [mem_ball_iff_norm, sub_zero] at h
      grind

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

Goal state before:
pp: R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
this : ‖(starRingEnd ℂ) w * z‖ < ‖↑R ^ 2‖
⊢ ↑R ^ 2 - (starRingEnd ℂ) w * z ≠ 0

Tactic:
by grind

Goal state after:
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
⊢ log ‖meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) x‖ = ∑ᶠ (u : 𝕜), ↑(d u) * log ‖x - u‖

Tactic:
meromorphicTrailingCoeffAt_factorizedRational h,

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
⊢ log ‖∏ᶠ (u : 𝕜), (x - u) ^ update d x 0 u‖ = ∑ᶠ (u : 𝕜), ↑(d u) * log ‖x - u‖
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)
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
a x : ℂ
h₂f : ∀ (a : ℂ), ‖a‖ ≤ R → ¬meromorphicOrderAt f a = ⊤
hR : 0 < R
hφ : MeromorphicOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, ‖z‖ ≤ R → ¬meromorphicOrderAt g z = ⊤
ha : (divisor f (ball 0 R)) a = 0
h₂a : ‖a‖ ≤ R
hx : ¬(divisor f (ball 0 R)) x = 0
⊢ a ≠ x

Tactic:
by grind

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

Goal state before:
pp: case right
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
⊢ (f.toLinearIsometry z).re = z.re

Tactic:
rw [@LinearIsometry.re_apply_eq_re f.toLinearIsometry h]

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
⊢ f =ᶠ[codiscreteWithin (closedBall 0 R)]
    ((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) *
        ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor f (sphere 0 R)) v) •
      fun x ↦ meromorphicTrailingCoeffAt f 0

Tactic:
simp only [hR.symm, closedBall_zero]

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
⊢ f =ᶠ[codiscreteWithin {0}]
    ((∏ᶠ (u : ℂ), canonicalFactor 0 u ^ (-(divisor f (ball 0 R)) u)) *
        ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor f (sphere 0 R)) v) •
      fun x ↦ meromorphicTrailingCoeffAt f 0
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
⊢ a.re • ℓ ↑b.re + (a.im * b.re) • ℓ I + (a.re • b.im • ℓ I + (-a.im * b.im) • ℓ 1) =
    ↑a.re • ℓ ↑b.re + (↑a.im • I) • ℓ ↑b.re + (↑a.re • b.im • ℓ I + (↑a.im • I) • b.im • ℓ I)

Tactic:
have t₂ {r : ℝ} : ℓ (r : ℂ) = r • ℓ (1 : ℂ) := by simp [← ℓ.map_smul]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : ℓ I = I • ℓ 1
a b : ℂ
t₀ : (↑a.im • I) • ↑b.re = ↑(a.im * b.re) • I
t₁ : (↑a.im • I) • ↑b.im • I = ↑(-a.im * b.im) • 1
t₂ : ∀ {r : ℝ}, ℓ ↑r = r • ℓ 1
⊢ a.re • ℓ ↑b.re + (a.im * b.re) • ℓ I + (a.re • b.im • ℓ I + (-a.im * b.im) • ℓ 1) =
    ↑a.re • ℓ ↑b.re + (↑a.im • I) • ℓ ↑b.re + (↑a.re • b.im • ℓ I + (↑a.im • I) • b.im • ℓ I)
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case mp.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, meromorphicOrderAt f ↑u ≠ ⊤
this : PreconnectedSpace ↑U
h : {u | meromorphicOrderAt f ↑u = ⊤} = ∅
⊢ ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤

pp: case mp.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, meromorphicOrderAt f ↑u ≠ ⊤
this : PreconnectedSpace ↑U
h : {u | meromorphicOrderAt f ↑u = ⊤} = univ
⊢ ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤

Tactic:
· intro u
      have : u ∉ (∅ : Set U) := by exact fun a => a
      rw [← h] at this
      tauto

Goal state after:
case mp.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
h₂f : ∃ u, meromorphicOrderAt f ↑u ≠ ⊤
this : PreconnectedSpace ↑U
h : {u | meromorphicOrderAt f ↑u = ⊤} = univ
⊢ ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ DiffContOnCl ℂ (fun z ↦ invInterpStrip f z ε) (verticalStrip 0 1)

Tactic:
by
  apply Differentiable.diffContOnCl
  apply Differentiable.mul
  · apply Differentiable.const_cpow (Differentiable.sub_const differentiable_id 1) _
    left
    rw [← ofReal_add, ofReal_ne_zero]
    simp only [ne_eq, ne_of_gt (sSupNormIm_eps_pos f hε 0), not_false_eq_true]
  · apply Differentiable.const_cpow (Differentiable.neg differentiable_id)
    apply Or.inl
    rw [← ofReal_add, ofReal_ne_zero]
    exact (ne_of_gt (sSupNormIm_eps_pos f hε 1))

Goal state after:
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
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
hs : ∀ (a : A), f a ∈ s
⊢ ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f

Tactic:
by
  obtain ⟨f, rfl⟩ : ∃ f' : C(A, s), f = .comp ⟨Subtype.val, by fun_prop⟩ f' :=
    ⟨⟨fun a ↦ ⟨f a, hs a⟩, by fun_prop⟩, rfl⟩
  lift e₀ to p ⁻¹' s using by rw [Set.mem_preimage, he]; apply hs
  rcases cov.isCoveringMap_restrictPreimage.existsUnique_continuousMap_lifts f a₀ e₀
    (Subtype.ext he) with ⟨F, ⟨rfl, hF⟩, hF_unique⟩
  refine ⟨.comp ⟨Subtype.val, by fun_prop⟩ F, ⟨rfl, ?_⟩, ?_⟩
  · simp [← hF, Function.comp_def]
  · rintro F' ⟨hF'₁, hF'₂⟩
    simp only [ContinuousMap.coe_comp, ContinuousMap.coe_mk, funext_iff,
      Function.comp_apply] at hF'₂
    specialize hF_unique
      ⟨fun a ↦ ⟨F' a, by rw [Set.mem_preimage, hF'₂]; exact (f a).2⟩, by fun_prop⟩
      ⟨Subtype.ext hF'₁, ?_⟩
    · ext; simp [← hF'₂]
    · ext; simp [← hF_unique]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ ‖f z‖ ≤ a ^ (1 - z.re) * b ^ z.re

Tactic:
apply (norm_le_interpStrip_of_mem_verticalClosedStrip₀₁ f hz hd hB).trans (this.trans _)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re ≤ a ^ (1 - z.re) * b ^ z.re
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicAt f x
⊢ ∀ᶠ (y : E) in 𝓝 x, HarmonicAt f y

Tactic:
filter_upwards [h.1.eventually (by simp), h.2.eventually_nhds] with a h₁a h₂a

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicAt f x
a : E
h₁a : ContDiffAt ℝ 2 f a
h₂a : ∀ᶠ (x : E) in 𝓝 a, Δ f x = 0 x
⊢ HarmonicAt f a
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
e e₁ e₂ : E
⊢ (tensorIteratedFDerivTwo 𝕜 f e) (e₁ ⊗ₜ[𝕜] e₂) = ((bilinearIteratedFDerivTwo 𝕜 f e) e₁) e₂

Tactic:
tensorIteratedFDerivTwo,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
e e₁ e₂ : E
⊢ (lift (bilinearIteratedFDerivTwo 𝕜 f e)) (e₁ ⊗ₜ[𝕜] e₂) = ((bilinearIteratedFDerivTwo 𝕜 f e) e₁) e₂
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
h₁ : ContDiffAt ℝ 2 f₁ x
h₂ : ContDiffAt ℝ 2 f₂ x
⊢ Δ (f₁ + f₂) =ᶠ[𝓝 x] Δ f₁ + Δ f₂

Tactic:
filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp)] with x h₁x h₂x
  exact h₁x.laplacian_add h₂x

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

Goal state before:
pp: f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun z ↦ (F z).re) = f
this : ∀ (z w : ℂ), cexp (F z) = cexp (F w)
⊢ ∀ (z w : ℂ), f z = f w

Tactic:
by grind

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

Goal state before:
pp: case inr.refine_1.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
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 : ℝ
hc✝ : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hc : ContinuousWithinAt f (Ioi 0 ×ℂ Ioi 0) 0
w : ℂ
⊢ ‖1‖ ≤ ‖expR (max B 0 * expR (c * |w.re|))‖

Tactic:
norm_one,

Goal state after:
case inr.refine_1.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
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 : ℝ
hc✝ : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hc : ContinuousWithinAt f (Ioi 0 ×ℂ Ioi 0) 0
w : ℂ
⊢ 1 ≤ ‖expR (max B 0 * expR (c * |w.re|))‖
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ := ⋯
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = ↑(f 0) ∧ ∀ x ∈ univ, HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x✝ y : ℂ
hy : y ∈ univ
x : ℂ
⊢ (fderiv ℝ f y) (x.re • 1 + x.im • I) = (fderiv ℝ f y) x

Tactic:
· simp

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
| (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)

Tactic:
arg 2

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
| ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
h : ∀ x ∈ sphere c |R|, f₁ x ≤ f₂ x
⊢ circleAverage f₁ c R ≤ circleAverage f₂ c R

Tactic:
apply (mul_le_mul_iff_of_pos_left (by simp [pi_pos])).2

Goal state after:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
h : ∀ x ∈ sphere c |R|, f₁ x ≤ f₂ x
⊢ ∫ (θ : ℝ) in 0..2 * π, f₁ (circleMap c R θ) ≤ ∫ (θ : ℝ) in 0..2 * π, f₂ (circleMap c R θ)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: x y : ℝ
z : ℍ
⊢ (x + y) +ᵥ z = x +ᵥ y +ᵥ z

Tactic:
simp [HVAdd.hVAdd, add_assoc]

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
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)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
⊢ ‖f ↑(-x)‖ ≤ C

Tactic:
exact hre _ (neg_nonpos.2 hx)

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
⊢ circleAverage (poissonKernel c w • f) c R = circleAverage (re ∘ herglotzRieszKernel c w • f) c R

Tactic:
apply circleAverage_congr_sphere
    (fun _ _ ↦ by simp_rw [← poissonKernel_eq_re_herglotzRieszKernel])

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

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ circleAverage (poissonKernel c w • f) c R = circleAverage (re ∘ herglotzRieszKernel c w • f) c R

Tactic:
apply circleAverage_congr_sphere
    (fun _ _ ↦ by simp_rw [← poissonKernel_eq_re_herglotzRieszKernel])

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

Goal state before:
pp: case inl
h0 : 0 ≤ 1
⊢ 1 - 1 ≤ 1 * log 1

pp: case inr
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
⊢ x - 1 ≤ x * log x

Tactic:
· simp

Goal state after:
case inr
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
⊢ x - 1 ≤ x * log x
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: case inl
h0 : 0 ≤ 1
⊢ negMulLog 1 ≤ 1 - 1

pp: case inr
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
⊢ x.negMulLog ≤ 1 - x

Tactic:
· simp

Goal state after:
case inr
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
⊢ x.negMulLog ≤ 1 - x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: case inr.inl
⊢ sin 0 / 0 ≤ |0|⁻¹

pp: case inr.inr
x : ℝ
hx : 0 < x
⊢ sin x / x ≤ |x|⁻¹

Tactic:
· simp

Goal state after:
case inr.inr
x : ℝ
hx : 0 < x
⊢ sin x / x ≤ |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
this : ‖↑q * x‖ < ‖W‖
⊢ ↑q * x - W ≠ 0

Tactic:
by grind

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

Goal state before:
pp: H : Tendsto (fun t ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (fun x ↦ (log x)⁻¹) 0))
⊢ Set.Iio 0 ⊆ {0}ᶜ

Tactic:
by grind

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

Goal state before:
pp: ⊢ {-1, 0, 1}ᶜ ⊆ {0}ᶜ

Tactic:
by grind

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

Goal state before:
pp: ⊢ Set.Ioi 1 ⊆ {-1, 0, 1}ᶜ

Tactic:
by grind

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

Goal state before:
pp: x : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
hx₂ : x ≠ -1
⊢ x ≠ 0

Tactic:
by grind

Goal state after:
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 : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
⊢ Real.circleAverage (fun z ↦ ((z + w) / (z - w)).re • f z) 0 R =
    Real.circleAverage (fun z ↦ (z / (z - w) - q • z / (q • z - W)) • f z) 0 R

Tactic:
by
      apply circleAverage_congr_sphere fun z hz ↦ ?_
      have hzR : ‖z‖ = R := by simpa [abs_of_pos hR] using hz
      match_scalars
      simp only [q, W, real_smul, ofReal_div, coe_algebraMap, mul_one]
      rw [← norm_mul_exp_arg_mul_I w, ← norm_mul_exp_arg_mul_I z, hzR,
        ← circleAverage_re_smul_on_ball_zero_aux, norm_mul_exp_arg_mul_I w]
      field [hR.ne.symm]

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

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

Tactic:
rw [intervalIntegrable_iff]
      apply IntegrableOn.congr_fun
      · rw [← intervalIntegrable_iff]; exact intervalIntegral.intervalIntegrable_rpow' h
      · intro x hx
        rw [uIoc_of_le hc] at hx
        dsimp only
        rw [Complex.norm_cpow_eq_rpow_re_of_pos hx.1]
      · exact measurableSet_uIoc

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₀
z : ℂ
hz : z ∈ ball (↑x₀) (dist 0 ↑x₀)
⊢ z ∈ {z | 0 < z.re}

Tactic:
rw [mem_ball, dist_zero_left, dist_eq, Complex.norm_of_nonneg hx₀] at hz

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 : ℂ
hz : ‖z - ↑x₀‖ < x₀
⊢ z ∈ {z | 0 < z.re}
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

Goal state before:
pp: ⊢ (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - (π / 2 - 0) • log 2 - ∫ (x : ℝ) in 0..π / 2, log (cos x) =
    (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (cos x)

pp: ⊢ IntervalIntegrable (fun x ↦ log (sin (2 * x))) MeasureTheory.volume 0 (π / 2)

pp: ⊢ IntervalIntegrable (fun x ↦ log (sin (2 * x)) - log 2) MeasureTheory.volume 0 (π / 2)

pp: ⊢ IntervalIntegrable (fun x ↦ log (cos x)) MeasureTheory.volume 0 (π / 2)

Tactic:
· simp

Goal state after:
⊢ IntervalIntegrable (fun x ↦ log (sin (2 * x))) MeasureTheory.volume 0 (π / 2)

⊢ IntervalIntegrable (fun x ↦ log (sin (2 * x)) - log 2) MeasureTheory.volume 0 (π / 2)

⊢ IntervalIntegrable (fun x ↦ log (cos x)) MeasureTheory.volume 0 (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hderiv
a b : ℝ
⊢ deriv rexp = rexp

pp: case hdiff
a b : ℝ
⊢ ∀ x ∈ [[a, b]], DifferentiableAt ℝ rexp x

pp: case hcont
a b : ℝ
⊢ ContinuousOn rexp [[a, b]]

Tactic:
· simp

Goal state after:
case hdiff
a b : ℝ
⊢ ∀ x ∈ [[a, b]], DifferentiableAt ℝ rexp x

case hcont
a b : ℝ
⊢ ContinuousOn rexp [[a, b]]
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: r : ℝ
⊢ (Complex.exp (Complex.I * ↑r) - Complex.exp (Complex.I * ↑(-r))) / Complex.I =
    (Complex.exp (Complex.I * ↑r) - Complex.exp (Complex.I * -↑r)) / Complex.I

pp: r : ℝ
⊢ Complex.I ≠ 0

Tactic:
· simp

Goal state after:
r : ℝ
⊢ Complex.I ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: r : ℝ
⊢ Complex.I ≠ 0

Tactic:
· simp

Goal state after: