mathlib-initiative/mathlib-tactics huggingface dataset:
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
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
η₀ : ∀ x ∈ t₁, ‖w - x‖ ^ (-divisor f S₀R) x ≠ 0
η₁ : ∀ x ∈ t₂, ‖canonicalFactor R x w‖ ^ (divisor f B₀R) x ≠ 0
⊢ log
      (‖(∏ i ∈ t₂, canonicalFactor R i w ^ (divisor f B₀R) i) * ∏ i ∈ t₁, (w - i) ^ (-divisor f S₀R) i‖ *
        ‖meromorphicTrailingCoeffAt f w‖) =
    ∑ i ∈ t₂, log (‖canonicalFactor R i w‖ ^ (divisor f B₀R) i) + ∑ i ∈ t₁, log (‖w - i‖ ^ (-divisor f S₀R) i) +
      log ‖meromorphicTrailingCoeffAt f w‖

Tactic:
norm_mul,

Goal state after:
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
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
η₀ : ∀ x ∈ t₁, ‖w - x‖ ^ (-divisor f S₀R) x ≠ 0
η₁ : ∀ x ∈ t₂, ‖canonicalFactor R x w‖ ^ (divisor f B₀R) x ≠ 0
⊢ log
      (‖∏ i ∈ t₂, canonicalFactor R i w ^ (divisor f B₀R) i‖ * ‖∏ i ∈ t₁, (w - i) ^ (-divisor f S₀R) i‖ *
        ‖meromorphicTrailingCoeffAt f w‖) =
    ∑ i ∈ t₂, log (‖canonicalFactor R i w‖ ^ (divisor f B₀R) i) + ∑ i ∈ t₁, log (‖w - i‖ ^ (-divisor f S₀R) i) +
      log ‖meromorphicTrailingCoeffAt f w‖
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
w : ℂ
hw : w.im ∈ closedBall a b
⊢ |(aff w).im| ≤ d * b

Tactic:
mem_closedBall,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
w : ℂ
hw : dist w.im a ≤ b
⊢ |(aff w).im| ≤ d * b
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
y : ℂ
yRe : y.re ∈ s
yIm : y.im = z.im
⊢ √((y.re - z.re) ^ 2 + 0 ^ 2) < r₁

Tactic:
zero_pow two_ne_zero,

Goal state after:
c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
y : ℂ
yRe : y.re ∈ s
yIm : y.im = z.im
⊢ √((y.re - z.re) ^ 2 + 0) < r₁
Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
⊢ ∑ m, ∑ n, (∑ i, ⟪w m, v i⟫_ℝ * ⟪w n, v i⟫_ℝ) • w m ⊗ₜ[ℝ] w n =
    ∑ i, (∑ m, ⟪w m, v i⟫_ℝ • w m) ⊗ₜ[ℝ] ∑ n, ⟪w n, v i⟫_ℝ • w n

Tactic:
simp only [sum_tmul, tmul_sum, smul_tmul_smul, Finset.sum_comm (γ := ι), Finset.sum_smul]
    rw [Finset.sum_comm]

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
R : Type u_4
V : Type u_5
E : Type u_6
F : Type u_7
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst✝¹⁴ : LineDeriv E V₁ V₂
inst✝¹³ : LineDeriv E V₂ V₃
inst✝¹² : AddCommGroup V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : AddCommGroup V₃
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
inst✝⁶ : Module R V₂
inst✝⁵ : Module R V₃
inst✝⁴ : LineDerivAdd E V₂ V₃
inst✝³ : LineDerivAdd E V₁ V₂
inst✝² : LineDerivSMul R E V₂ V₃
inst✝¹ : LineDerivLeftSMul R E V₁ V₂
inst✝ : LineDerivLeftSMul R E V₂ V₃
f : V₁
⊢ ∀ (c : R) (m n : E), ∂_{m} (∂_{c • n} f) = c • ∂_{m} (∂_{n} f)

Tactic:
simp [lineDerivOp_left_smul, lineDerivOp_smul]

Goal state after:
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
this :
  ∀ 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‖
⊢ Tendsto (fun x ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 ‖↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z‖)

Tactic:
norm_mul,

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
this :
  ∀ 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‖
⊢ Tendsto (fun x ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 (‖↑(sSupNormIm f 0) ^ (1 - z)‖ * ‖↑(sSupNormIm f 1) ^ z‖))
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) • f z)

Tactic:
smul_sub,

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₂ - I • (↑w.im - ↑z.im) • f z)
Module: Mathlib.Analysis.Complex.MeanValue

Goal state before:
pp: case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hR : ¬R = 0
⊢ circleAverage f c R = f c

Tactic:
rw [← circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable hs h₁f h₂f (by aesop)]
    apply circleAverage_congr_sphere fun z hz ↦ ?_
    have : z - c ≠ 0 := by grind [ne_of_mem_sphere]
    simp_all

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

Goal state before:
pp: f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun x ↦ c) (Ioo r R)
⊢ ∃ l ∈ Iio R, Ioo l R ⊆ Ioc r R

Tactic:
use r

Goal state after:
case h
f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun x ↦ c) (Ioo r R)
⊢ r ∈ Iio R ∧ Ioo r R ⊆ Ioc r R
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a : E
c : ℂ
R : ℝ
⊢ circleAverage (fun x ↦ a) c R = a

Tactic:
simp only [circleAverage, intervalIntegral.integral_const, ← smul_assoc, sub_zero, smul_eq_mul]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a : E
c : ℂ
R : ℝ
⊢ ((2 * π)⁻¹ * (2 * π)) • a = a
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
key : (-(↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I)))).re ≤ R * r
⊢ 1 *
      (‖↑R * cexp (↑θ * I)‖ ^ 2 + ‖↑r * cexp (↑φ * I)‖ ^ 2 -
        2 * (↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I))).re) ≤
    (R + r) * (R + r)

Tactic:
simpa using calc
    R ^ 2 + r ^ 2 - 2 * (R * cexp (θ * I) * (starRingEnd ℂ) (r * cexp (φ * I))).re
    _ ≤ R ^ 2 + r ^ 2 + 2 * (R * r) := by rw [sub_eq_add_neg, ← mul_neg, ← neg_re]; gcongr
    _ = (R + r) * (R + r) := by ring

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

Goal state before:
pp: case neg
x : ℝ
hx : ¬x = 0
⊢ |sin x| ≤ 1 * |x|

Tactic:
one_mul

Goal state after:
case neg
x : ℝ
hx : ¬x = 0
⊢ |sin x| ≤ |x|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

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

Tactic:
abs_of_nonneg hx.le,

Goal state after:
case inr.inr
x : ℝ
hx : 0 < x
⊢ sin x / x ≤ x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
x : ℝ
hx : x ∈ Ioo c 0
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = ‖(-↑x) ^ r * Complex.exp (↑π * Complex.I * r)‖

Tactic:
norm_mul,

Goal state after:
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
x : ℝ
hx : x ∈ Ioo c 0
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = ‖(-↑x) ^ r‖ * ‖Complex.exp (↑π * Complex.I * r)‖
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
x : ℝ
hx : x ∈ Ioo c 0
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = 1 * ‖Complex.exp (↑π * Complex.I * r)‖

Tactic:
one_mul

Goal state after:
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
x : ℝ
hx : x ∈ Ioo c 0
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = ‖Complex.exp (↑π * Complex.I * r)‖
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
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ MapsTo (fun z ↦ z + c) (ball 0 R) (ball c R)

Tactic:
by intro; aesop

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

Goal state before:
pp: case neg
x y : ℝ
ha : ¬x = 0
hb : ¬y = 0
⊢ log⁺ (x * y) ≤ log⁺ x + log⁺ y

Tactic:
unfold posLog

Goal state after:
case neg
x y : ℝ
ha : ¬x = 0
hb : ¬y = 0
⊢ max 0 (log (x * y)) ≤ max 0 (log x) + max 0 (log y)
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
hg : CircleIntegrable f 0 R
hw : w ∈ ball 0 R
hR : 0 < R
d : ℝ
hd : d > 0
hsub : ball w d ⊆ ball 0 R
hdist : ∀ x ∈ ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap 0 R θ - x‖
hgm : AEStronglyMeasurable (fun θ ↦ f (circleMap 0 R θ)) (volume.restrict (uIoc 0 (2 * π)))
θ : ℝ
a✝ : θ ∈ uIoc 0 (2 * π)
x : ℂ
hx : x ∈ ball w d
h₁ : ‖2‖ = 2
⊢ ‖2 * circleMap 0 R θ‖ / ‖(circleMap 0 R θ - x) ^ 2‖ * ‖f (circleMap 0 R θ)‖ ≤
    2 * R * (d ^ 2)⁻¹ * ‖f (circleMap 0 R θ)‖

Tactic:
norm_mul,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
hg : CircleIntegrable f 0 R
hw : w ∈ ball 0 R
hR : 0 < R
d : ℝ
hd : d > 0
hsub : ball w d ⊆ ball 0 R
hdist : ∀ x ∈ ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap 0 R θ - x‖
hgm : AEStronglyMeasurable (fun θ ↦ f (circleMap 0 R θ)) (volume.restrict (uIoc 0 (2 * π)))
θ : ℝ
a✝ : θ ∈ uIoc 0 (2 * π)
x : ℂ
hx : x ∈ ball w d
h₁ : ‖2‖ = 2
⊢ ‖2‖ * ‖circleMap 0 R θ‖ / ‖(circleMap 0 R θ - x) ^ 2‖ * ‖f (circleMap 0 R θ)‖ ≤
    2 * R * (d ^ 2)⁻¹ * ‖f (circleMap 0 R θ)‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℤ
h : 0 ≤ n ∨ n ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)

Tactic:
replace h : -1 < (n : ℝ) ∨ (n : ℝ) ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]] := mod_cast h

Goal state after:
a b : ℝ
n : ℤ
h : -1 < ↑n ∨ ↑n ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)

Tactic:
by
  simpa only [← Int.natCast_succ, zpow_natCast] using! integral_zpow (Or.inl n.cast_nonneg)

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

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

Tactic:
exact fun _ _ => differentiableAt_exp

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

Goal state before:
pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z ↦ cexp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
y : ℝ
⊢ 1 * ‖f (↑y * I)‖ ≤ C

Tactic:
one_mul

Goal state after:
case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z ↦ cexp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
y : ℝ
⊢ ‖f (↑y * I)‖ ≤ C
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
this : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (sphere 0 |1|)
z : ℂ
hz : ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0
⊢ log ‖↑R * (z + ↑R⁻¹ * (c - a))‖ = log ‖R‖ + log ‖z + ↑R⁻¹ * (c - a)‖

Tactic:
norm_mul,

Goal state after:
a c : ℂ
R : ℝ
hR : R ≠ 0
this : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (sphere 0 |1|)
z : ℂ
hz : ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0
⊢ log (‖↑R‖ * ‖z + ↑R⁻¹ * (c - a)‖) = log ‖R‖ + log ‖z + ↑R⁻¹ * (c - a)‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case neg
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
⊢ |R|⁻¹ * ‖c - a‖ ≤ 1

Tactic:
mem_closedBall,

Goal state after:
case neg
a c : ℂ
R : ℝ
hu : dist a c ≤ |R|
hR : ¬R = 0
⊢ |R|⁻¹ * ‖c - a‖ ≤ 1
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
y : ℝ
⊢ 1 * ‖f (↑y * I)‖ ≤ C

Tactic:
one_mul

Goal state after:
case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
y : ℝ
⊢ ‖f (↑y * I)‖ ≤ C
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
⊢ update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h)) (𝕢 h z) = f (invQParam h (𝕢 h z))

Tactic:
update_of_ne,

Goal state after:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
⊢ (f ∘ invQParam h) (𝕢 h z) = f (invQParam h (𝕢 h z))

case h
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
⊢ 𝕢 h z ≠ 0
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: case mapsTo
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
⊢ MapsTo (fun z ↦ ↑ε / (f z - x)) U (ball 0 1)

pp: case injOn
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
⊢ InjOn (fun z ↦ ↑ε / (f z - x)) U

pp: case deriv
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
⊢ ∀ z ∈ U, deriv (fun z ↦ ↑ε / (f z - x)) z ≠ 0

Tactic:
case mapsTo =>
    intro z hz
    rw [mem_ball_zero_iff, norm_div, norm_real, Real.norm_of_nonneg hε₀.le, div_lt_one₀]
    · simpa [dist_eq_norm] using hε z hz
    · simpa [sub_eq_zero] using hfx z hz

Goal state after:
case injOn
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
⊢ InjOn (fun z ↦ ↑ε / (f z - x)) U

case deriv
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
⊢ ∀ z ∈ U, deriv (fun z ↦ ↑ε / (f z - x)) z ≠ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
h : 0 < (↑g).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : ↑(↑g 1 0) * (↑z * ↑z) + (↑(↑g 1 1) - ↑(↑g 0 0)) * ↑z + -↑(↑g 0 1) = 0
hc : ↑g 1 0 ≠ 0
hge : 0 ≤ (↑g).discr
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = ↑√(↑g).discr * ↑√(↑g).discr
⊢ False

Tactic:
quadratic_eq_zero_iff (mod_cast hc) hd

Goal state after:
g : GL (Fin 2) ℝ
h : 0 < (↑g).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz :
  ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) + ↑√(↑g).discr) / (2 * ↑(↑g 1 0)) ∨
    ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - ↑√(↑g).discr) / (2 * ↑(↑g 1 0))
hc : ↑g 1 0 ≠ 0
hge : 0 ≤ (↑g).discr
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = ↑√(↑g).discr * ↑√(↑g).discr
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case refine_2
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
ha : a = 0
⊢ (↑(g ^ 2)).det = 0

Tactic:
rw [← hg] at hmsq

Goal state after:
case refine_2
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = m
hm0 : m ≠ 0
hmsq : ↑g ^ 2 = 0
ha : a = 0
⊢ (↑(g ^ 2)).det = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
⊢ ‖↑(r / ‖↑τ‖ - 1) * ↑τ‖ < ε

Tactic:
norm_mul,

Goal state after:
τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
⊢ ‖↑(r / ‖↑τ‖ - 1)‖ * ‖↑τ‖ < ε
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: case right
τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
this : ↑r / ↑‖↑τ‖ * ↑τ ∈ Metric.ball (↑τ) ε
ξ : ℍ
hξs : ξ ∈ s
hξτ : ↑ξ = ↑r / ↑‖↑τ‖ * ↑τ
⊢ ‖↑r / ↑‖↑τ‖ * ↑τ‖ = r

Tactic:
norm_mul,

Goal state after:
case right
τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
this : ↑r / ↑‖↑τ‖ * ↑τ ∈ Metric.ball (↑τ) ε
ξ : ℍ
hξs : ξ ∈ s
hξτ : ↑ξ = ↑r / ↑‖↑τ‖ * ↑τ
⊢ ‖↑r / ↑‖↑τ‖‖ * ‖↑τ‖ = r
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M✝ : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l✝ + 1
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M✝ k
M : Matrix { a // (a = k) = False } { a // (a = k) = False } S[X]
⊢ Fintype.card { a // (a = k) = False } = l✝

Tactic:
grind [Fintype.card_subtype_compl, Fintype.card_unique]

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
classical
  nontriviality R
  nontriviality A
  have := Module.nontrivial S A
  let ⟨ιS, bS⟩ := Module.Free.exists_basis (R := R) (M := S)
  let ⟨ιA, bA⟩ := Module.Free.exists_basis (R := S) (M := A)
  have := bS.index_nonempty
  have := bA.index_nonempty
  cases fintypeOrInfinite ιS; swap
  · rw [Algebra.norm_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis bS),
      det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis (bS.smulTower bA))]
  cases fintypeOrInfinite ιA; swap
  · rw [det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis bA), map_one,
      det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis (bS.smulTower bA))]
  rw [Algebra.norm_eq_matrix_det bS, ← AlgHom.coe_toRingHom, ← det_toMatrix bA, det_det,
    ← det_toMatrix (bS.smulTower' bA), restrictScalars_toMatrix, RingHom.coe_coe]

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

Goal state before:
pp: case convert_2
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
hτ : ∀ᶠ (x : ℂ) in 𝓝 ↑τ, x ∈ {↑τ}ᶜ → (f ∘ ↑ofComplex) x ≠ 0
⊢ ∀ᶠ (x : ℍ) in 𝓝[≠] τ, f x ≠ 0

Tactic:
← isOpenEmbedding_coe.map_nhds_eq,

Goal state after:
case convert_2
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
hτ : ∀ᶠ (x : ℂ) in map UpperHalfPlane.coe (𝓝 τ), x ∈ {↑τ}ᶜ → (f ∘ ↑ofComplex) x ≠ 0
⊢ ∀ᶠ (x : ℍ) in 𝓝[≠] τ, f x ≠ 0