mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
r : ℝ
z : ℂ
hz : z ∈ sphere c |r|
⊢ MeromorphicAt (fun x ↦ x - a) z

Tactic:
fun_prop

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

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
x : ℂ
hx : x ∈ closedBall 0 |1|
this : ‖x * a‖ < 1
⊢ AnalyticAt ℂ (fun x ↦ 1 - x * a) x

Tactic:
fun_prop

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

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

Tactic:
fun_prop

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

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

Tactic:
simp_rw [mul_comm _ Complex.I]
    rw [integral_exp_mul_complex]
    · simp
    · simp

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

Goal state before:
pp: x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.univ
⊢ AnalyticAt ℝ (fun x ↦ 4 * sin x ^ 2) x✝¹

Tactic:
fun_prop

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

Goal state before:
pp: b : ℝ
ht : 0 < b
⊢ ContinuousAt (fun x ↦ x * log x - x) b

Tactic:
fun_prop

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ Continuous fun y ↦ Complex.cos (z * ↑y)

Tactic:
fun_prop

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

Goal state before:
pp: case refine_1
a b : ℝ
⊢ Continuous fun x ↦ 1 + x ^ 2

Tactic:
fun_prop

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

Goal state before:
pp: a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : x ∈ closedBall 0 |1|
⊢ AnalyticAt ℂ (fun x ↦ x - a) x

Tactic:
fun_prop

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

Goal state before:
pp: a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun x ↦ 1 + ↑x ^ 2

Tactic:
fun_prop

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

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
x✝¹ : ℂ
x✝ : x✝¹ ∈ sphere 0 |1|
⊢ MeromorphicAt (fun z ↦ z + ↑R⁻¹ * (c - a)) x✝¹

Tactic:
fun_prop

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

Goal state before:
pp: w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
θ : ℝ
⊢ ContinuousAt (circleMap 0 r) θ

Tactic:
fun_prop

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

Goal state before:
pp: case hf
a b : ℝ
n : ℕ
C : ℝ := ⋯
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ Continuous fun x ↦ sin x ^ n

Tactic:
fun_prop

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

Goal state before:
pp: case hg
a b : ℝ
n : ℕ
C : ℝ := ⋯
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ Continuous fun x ↦ sin x ^ (n + 2)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SeminormedRing β
l : Filter α
f g : α → β
hf : l.BoundedAtFilter f
hg : l.BoundedAtFilter g
⊢ l.BoundedAtFilter (f * g)

Tactic:
by
  refine (hf.mul hg).trans ?_
  convert! Asymptotics.isBigO_refl (E := ℝ) _ l
  simp

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

Goal state before:
pp: r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
⊢ √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖

Tactic:
have h_cos_law (r₁ : ℝ) :
      ‖circleMap 0 r₁ θ - ρ‖ ^ 2 = r₁ ^ 2 + R ^ 2 - 2 * r₁ * R * Real.cos (θ - Complex.arg ρ) := by
    rw [← ofReal_inj, ← normSq_eq_norm_sq, normSq_sub ]
    suffices (circleMap 0 r₁ θ * (conj) ρ).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg) by
      simp [normSq_eq_norm_sq, hρ, -mul_re, this, mul_assoc]
    conv_lhs => rw [← norm_mul_exp_arg_mul_I ρ, ← circleMap_zero, conj_circleMap_zero,
      circleMap_zero_mul, circleMap_zero_re, ← sub_eq_add_neg]

Goal state after:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
h_cos_law : ∀ (r₁ : ℝ), ‖circleMap 0 r₁ θ - ρ‖ ^ 2 = r₁ ^ 2 + R ^ 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
⊢ √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case refine_1
a b : ℝ
n : ℕ
C : ℝ := ⋯
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
⊢ Continuous fun x ↦ ↑(n + 1) * cos x * sin x ^ n

Tactic:
fun_prop

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

Goal state before:
pp: case refine_2
a b : ℝ
n : ℕ
C : ℝ := ⋯
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
⊢ Continuous sin

Tactic:
fun_prop

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

Goal state before:
pp: h : ℝ
⊢ Continuous fun z ↦ cexp (2 * ↑π * I * z / ↑h)

Tactic:
fun_prop

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

Goal state before:
pp: h : ℝ
⊢ Continuous (𝕢 h)

Tactic:
by
  unfold qParam
  fun_prop

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

Goal state before:
pp: w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
⊢ |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| * |log ‖circleMap 0 r θ - ρ‖| ≤
    (R + ‖w‖) / (r₀ - ‖w‖) * (|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|)

Tactic:
have h_norm_sub₁ := const_mul_norm_sub_circleMap_le_norm_sub_circleMap hρ hr₀ hR hr₀r hrR θ

Goal state after:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
⊢ |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| * |log ‖circleMap 0 r θ - ρ‖| ≤
    (R + ‖w‖) / (r₀ - ‖w‖) * (|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|)
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
⊢ Differentiable ℂ fun z ↦ cexp (2 * ↑π * I * z / ↑h)

Tactic:
fun_prop

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

Goal state before:
pp: h : ℝ
⊢ Differentiable ℂ (𝕢 h)

Tactic:
by
  unfold qParam
  fun_prop

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

Goal state before:
pp: h : ℝ
m : WithTop ℕ∞
⊢ ContDiff ℂ m fun z ↦ cexp (2 * ↑π * I * z / ↑h)

Tactic:
fun_prop

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

Goal state before:
pp: h : ℝ
m : WithTop ℕ∞
⊢ ContDiff ℂ m (𝕢 h)

Tactic:
by
  unfold qParam
  fun_prop

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
z : E
h1 : AnalyticAt ℂ (gray z) 0
hz : z ∈ sphere 0 1
hrz : ¬∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
h7 : 𝓝 (g z₀) ≤ (map g ∘ map (ray z)) (𝓝 0)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun t ↦ z₀ + t • z

Tactic:
fun_prop

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ Continuous fun z ↦ ⟨↑z ^ n, ⋯⟩

Tactic:
fun_prop

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

Goal state before:
pp: case hf
a b : ℝ
n : ℕ
C : ℝ := ⋯
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ Continuous fun x ↦ cos x ^ n

Tactic:
fun_prop

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

Goal state before:
pp: case hg
a b : ℝ
n : ℕ
C : ℝ := ⋯
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ Continuous fun x ↦ cos x ^ (n + 2)

Tactic:
fun_prop

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

Goal state before:
pp: case refine_1
a b : ℝ
n : ℕ
C : ℝ := ⋯
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
⊢ Continuous fun x ↦ -↑(n + 1) * sin x * cos x ^ n

Tactic:
fun_prop

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

Goal state before:
pp: case refine_2
a b : ℝ
n : ℕ
C : ℝ := ⋯
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
⊢ Continuous cos

Tactic:
fun_prop

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

Goal state before:
pp: a b : ℝ
m n : ℕ
⊢ Continuous fun u ↦ u ^ m * (1 - u ^ 2) ^ n

Tactic:
fun_prop

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

Goal state before:
pp: a b : ℝ
m n : ℕ
⊢ Continuous fun u ↦ u ^ n * (1 - u ^ 2) ^ m

Tactic:
fun_prop

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

Goal state before:
pp: ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ :=
  fun θ ↦ (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
x✝ : ℂ
⊢ x✝ ∈ sphere 0 |R| → MeromorphicAt (fun z ↦ z - ρ) x✝

Tactic:
fun_prop

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

Goal state before:
pp: c z : ℂ
f : ℂ → ℂ
hf : Differentiable ℂ f
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Tactic:
convert! taylorSeries_eq_of_entire hf c z using 3 with n
  rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]

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

Goal state before:
pp: a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
⊢ Continuous fun x ↦ cos (2 * x) ^ 2

Tactic:
fun_prop

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

Goal state before:
pp: ⊢ Continuous fun x ↦ √(1 - x ^ 2)

Tactic:
fun_prop

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
z : ℂ
hz : z ∈ ball 0 (r n)
⊢ AnalyticAt ℂ (fun x ↦ x - ρ) z

Tactic:
fun_prop

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
x : ℂ
hx : x ∈ closure (ball 0 (r n))
this : ‖x - ρ‖ ≠ 0
⊢ ContinuousWithinAt (fun x ↦ log ‖x - ρ‖) (closure (ball 0 (r n))) x

Tactic:
fun_prop

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

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∑ᶠ (i : ℂ), (↑((divisor f CB) i) * log R - ↑((divisor f CB) i) * log ‖c - i‖) + log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * (log R - log ‖c - u‖) + log ‖meromorphicTrailingCoeffAt f c‖

pp: case hf
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ Function.HasFiniteSupport fun u ↦ ↑((divisor f CB) u) * log R

pp: case hg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ Function.HasFiniteSupport fun u ↦ ↑((divisor f CB) u) * log ‖c - u‖

Tactic:
· simp_rw [← mul_sub]

Goal state after:
case hf
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ Function.HasFiniteSupport fun u ↦ ↑((divisor f CB) u) * log R

case hg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ Function.HasFiniteSupport fun u ↦ ↑((divisor f CB) u) * log ‖c - u‖
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : ¬im I = 1
⊢ I = 0

Tactic:
grind [I_eq_zero_or_im_I_eq_one]

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

Goal state before:
pp: case pos
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
x : ℂ
h : x ∈ CB
⊢ (divisor f CB) x = 0 x

Tactic:
simp_all [CB]

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

Goal state before:
pp: case neg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
x : ℂ
h : x ∉ CB
⊢ (divisor f CB) x = 0 x

Tactic:
simp_all [CB]

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : ¬im I = 1
⊢ ↑√(re I) = ↑√2⁻¹ * (1 - I) * I

Tactic:
grind [I_eq_zero_or_im_I_eq_one]

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : ¬im I = 1
⊢ ↑√(re (-I)) = ↑√2⁻¹ * (1 + I) * -I

Tactic:
grind [I_eq_zero_or_im_I_eq_one]

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

Goal state before:
pp: 𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝¹ : NormedSpace ℝ E
this✝ : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
this : Continuous ((Metric.closedBall 0 1).piecewise id g)
⊢ Continuous Subtype.val

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
e' : X₁ ≃ₜ ↑(Set.range e) := ⋯.toHomeomorph
g : C(X, Y)
hg : restrict (Set.range e) g = f.comp ↑e'.symm
⊢ g.comp { toFun := e, continuous_toFun := ⋯ } = f

Tactic:
by ext x; simpa using! congr($(hg) ⟨e' x, x, rfl⟩)

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed[inst✝²] s
Y : Type v
inst✝ : TopologicalSpace Y
f : C(↑s, Y)
t : Set Y
hf : ∀ (x : ↑s), f x ∈ t
ht : TietzeExtension ↑t
g : C(X, ↑t)
hg : restrict s g = { toFun := Set.codRestrict (⇑f) t hf, continuous_toFun := ⋯ }
⊢ Continuous[instTopologicalSpaceSubtype, inst✝] Subtype.val

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X₁ : Type u₁
inst✝³ : TopologicalSpace X₁
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
e : X₁ → X
he : IsClosedEmbedding e
Y : Type v
inst✝ : TopologicalSpace Y
f : C(X₁, Y)
t : Set Y
hf : ∀ (x : X₁), f x ∈ t
ht : TietzeExtension ↑t
g : C(X, ↑t)
hg : g.comp { toFun := e, continuous_toFun := ⋯ } = { toFun := Set.codRestrict (⇑f) t hf, continuous_toFun := ⋯ }
⊢ Continuous[instTopologicalSpaceSubtype, inst✝] Subtype.val

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
h : ↑(cd 0) * z + ↑(cd 1) = 0
⊢ cd = 0

Tactic:
have : cd 0 = 0 := by
    -- we will need this twice
    apply_fun Complex.im at h
    simpa only [Complex.add_im, Complex.mul_im, Complex.ofReal_im, zero_mul, add_zero,
      Complex.zero_im, mul_eq_zero, hz, or_false] using! h

Goal state after:
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
h : ↑(cd 0) * z + ↑(cd 1) = 0
this : cd 0 = 0
⊢ cd = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: ⊢ IsOpen (range UpperHalfPlane.coe)

Tactic:
simp [isOpen_upperHalfPlaneSet]

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: ⊢ Continuous fun t ↦ Complex.I * ↑t

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: ⊢ GeneralLinearGroup.det J = -1

Tactic:
by ext; simp [J]

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
ha' : ¬∃ x, f x = a
hd : Disjoint (range e ∪ ⇑g ⁻¹' Ici c) (⇑g ⁻¹' {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Ici c)
dga : EqOn (⇑dg) (Function.const Y (c - a)) (⇑g ⁻¹' {a})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (c - a)
hgf : ∀ (x : X), (g + dg) (e x) = f x
⊢ ∃ g, (∀ (y : Y), ∃ x, g y ∈ Icc (f x) b) ∧ ⇑g ∘ e = ⇑f

Tactic:
refine ⟨g + dg, fun y => ?_, funext hgf⟩

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
ha' : ¬∃ x, f x = a
hd : Disjoint (range e ∪ ⇑g ⁻¹' Ici c) (⇑g ⁻¹' {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Ici c)
dga : EqOn (⇑dg) (Function.const Y (c - a)) (⇑g ⁻¹' {a})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (c - a)
hgf : ∀ (x : X), (g + dg) (e x) = f x
y : Y
⊢ ∃ x, (g + dg) y ∈ Icc (f x) b
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) ((M * auxMat M k).map ⇑f)).det

Tactic:
← f.mapMatrix_apply,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp m m n n R) (f.mapMatrix M)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (f.mapMatrix (M * auxMat M k))).det
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
⊢ Continuous[inst✝², _] (Subtype.val ∘ ⇑h ∘ ⇑f)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
⊢ Continuous toReal

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ ContinuousAt (dist c) c

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ dist ↑z ↑(w.center r) = √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2)

Tactic:
← sqrt_sq dist_nonneg,

Goal state after:
z w : ℍ
r : ℝ
⊢ √(dist ↑z ↑(w.center r) ^ 2) = √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2)
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
α : Type u_4
inst✝ : TopologicalSpace α
f : α → GL n R
hf : Continuous[inst✝, Units.instTopologicalSpaceUnits] f
i : n
⊢ Continuous[instTopologicalSpaceMatrix, Pi.topologicalSpace] fun A ↦ A i

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
α : Type u_4
inst✝ : TopologicalSpace α
f : α → GL n R
hf : Continuous[inst✝, Units.instTopologicalSpaceUnits] f
i : n
⊢ Continuous[inst✝, instTopologicalSpaceMatrix] fun x ↦ ↑(f x)

Tactic:
fun_prop

Goal state after: