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
⊢ ∑ 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‖ =
    ∑ i ∈ t₂, ↑((divisor f B₀R) i) * log ‖canonicalFactor R i w‖ - ∑ i ∈ t₁, ↑((divisor f S₀R) i) * log ‖w - i‖ +
      log ‖meromorphicTrailingCoeffAt f w‖

Tactic:
sub_eq_add_neg,

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
⊢ ∑ 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‖ =
    ∑ i ∈ t₂, ↑((divisor f B₀R) i) * log ‖canonicalFactor R i w‖ + -∑ i ∈ t₁, ↑((divisor f S₀R) i) * log ‖w - i‖ +
      log ‖meromorphicTrailingCoeffAt f w‖
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init m 0 = m 0
hmtail : tail m (last n) = m (last n.succ)
⊢ ∂_{m 0} (∂^{tail m} f) = ∂_{m 0} (∂^{init (tail m)} (∂_{tail m (last n)} f))

Tactic:
congr 1
        exact IH _

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

Goal state before:
pp: l u : ℝ
hul : l < u
z : ℂ
⊢ z.re * (↑(u - l)).re / ((u - l) * (u - l)) + z.im * (↑(u - l)).im / ((u - l) * (u - l)) - l / (u - l) =
    (z.re - l) / (u - l)

Tactic:
Complex.ofReal_re,

Goal state after:
l u : ℝ
hul : l < u
z : ℂ
⊢ z.re * (u - l) / ((u - l) * (u - l)) + z.im * (↑(u - l)).im / ((u - l) * (u - l)) - l / (u - l) = (z.re - l) / (u - l)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
l u : ℝ
hul : l < u
f : ℂ → E
z : ℂ
hz : z ∈ verticalClosedStrip l u
hd : DiffContOnCl ℂ f (verticalStrip l u)
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
hgoal :
  ‖f (↑l + (z / (↑u - ↑l) - ↑l / (↑u - ↑l)) * (↑u - ↑l))‖ ≤ ‖interpStrip (scale f l u) (z / (↑u - ↑l) - ↑l / (↑u - ↑l))‖
⊢ ‖f z‖ ≤ ‖interpStrip' f l u z‖

Tactic:
fun_arg_eq hul,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
l u : ℝ
hul : l < u
f : ℂ → E
z : ℂ
hz : z ∈ verticalClosedStrip l u
hd : DiffContOnCl ℂ f (verticalStrip l u)
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
hgoal : ‖f z‖ ≤ ‖interpStrip (scale f l u) (z / (↑u - ↑l) - ↑l / (↑u - ↑l))‖
⊢ ‖f z‖ ≤ ‖interpStrip' f l u z‖
Module: Mathlib.Analysis.Complex.Hadamard

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

Tactic:
fun_arg_eq hul,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b l u : ℝ
hul : l < u
hz : z ∈ verticalClosedStrip l u
hd : DiffContOnCl ℂ f (verticalStrip l u)
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
hgoal : ‖f z‖ ≤ a ^ (1 - ((z / (↑u - ↑l)).re - (↑l / (↑u - ↑l)).re)) * b ^ ((z / (↑u - ↑l)).re - (↑l / (↑u - ↑l)).re)
⊢ ‖f z‖ ≤ a ^ (1 - (z.re - l) / (u - l)) * b ^ ((z.re - l) / (u - l))
Module: Mathlib.Analysis.Complex.Harmonic.Liouville

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
z w : ℂ
ℓ : StrongDual ℝ E
h₁ℓ : ‖ℓ‖ ≤ 1
h₂ℓ : ℓ (f z - f w) = ↑‖f z - f w‖
⊢ f z = f w

Tactic:
rw [map_sub, RCLike.ofReal_real_eq_id, id_eq] at h₂ℓ

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
z w : ℂ
ℓ : StrongDual ℝ E
h₁ℓ : ‖ℓ‖ ≤ 1
h₂ℓ : ℓ (f z) - ℓ (f w) = ‖f z - f w‖
⊢ f z = f w
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
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 : ℂ
⊢ DifferentiableOn ℝ f univ

Tactic:
exact hf.contDiffOn.differentiableOn two_ne_zero

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

Goal state before:
pp: case inr.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ✝ : ℂ
hζ✝ : ζ✝.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ✝).re
hz_im : 0 ≤ (cexp ζ✝).im
hzne : cexp ζ✝ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℂ
hζ : ζ.im = 0
⊢ ‖(f ∘ cexp) ζ‖ ≤ C

Tactic:
lift ζ to ℝ using hζ

Goal state after:
case inr.refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ✝ : ℂ
hζ : ζ✝.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ✝).re
hz_im : 0 ≤ (cexp ζ✝).im
hzne : cexp ζ✝ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℝ
⊢ ‖(f ∘ cexp) ↑ζ‖ ≤ C
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℂ
R : ℝ
ι : Type u_4
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ circleAverage (fun z ↦ ∑ i ∈ s, f i z) c R = ∑ i ∈ s, circleAverage (f i) c R

Tactic:
convert! circleAverage_sum h

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℂ
R : ℝ
ι : Type u_4
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
x✝ : ℂ
⊢ ∑ i ∈ s, f i x✝ = (∑ i ∈ s, f i) x✝
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
⊢ R ^ 2 + r ^ 2 - 2 * (↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I))).re ≤ R ^ 2 + r ^ 2 + 2 * (R * r)

Tactic:
sub_eq_add_neg,

Goal state after:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
key : (-(↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I)))).re ≤ R * r
⊢ R ^ 2 + r ^ 2 + -(2 * (↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I))).re) ≤ R ^ 2 + r ^ 2 + 2 * (R * r)
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: case right.e_6.h
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 : ℂ
hx : x ∈ g ⁻¹' (slitPlane ∩ {0}ᶜ)
⊢ (g x).arg ≠ Real.pi

Tactic:
simp [Complex.slitPlane_arg_ne_pi hx.1]

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

Goal state before:
pp: case inl
x : ℝ
hx : x < 0
⊢ 0 < -x

Tactic:
simpa using hx

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'
hfc : ContinuousOn (fun x ↦ f ↑x) (Ici 0)
x₀ : ℝ
hx₀ : 0 ≤ x₀
hne : f ↑x₀ ≠ 0
hlt : ‖0‖ < ‖f ↑x₀‖
this : ∀ᶠ (x : ℝ) in cocompact ℝ ⊓ 𝓟 (Ici 0), ‖f ↑x‖ ≤ ‖f ↑x₀‖
⊢ ∃ x, 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x‖

Tactic:
by
      simpa only [exists_prop] using! hfc.norm.exists_isMaxOn' isClosed_Ici hx₀ this

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

Goal state before:
pp: case inl
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ r + 1 ≠ 0

Tactic:
apply_fun Complex.re

Goal state after:
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ (r + 1).re ≠ Complex.re 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

Goal state before:
pp: x : ℝ
| log (sin x)

Tactic:
rw [← sin_pi_sub]

Goal state after:
x : ℝ
| log (sin (π - x))
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
⊢ ∫ (x : ℝ) in a..b, rexp x = rexp b - rexp a

Tactic:
rw [integral_deriv_eq_sub']
  · simp
  · exact fun _ _ => differentiableAt_exp
  · exact continuousOn_exp

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:
by
  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]
  have : (r₀ / R) * ‖circleMap 0 R θ - ρ‖ ^ 2 ≤ ‖circleMap 0 r θ - ρ‖ ^ 2 := by
    rw [div_mul_eq_mul_div, div_le_iff₀ hR]
    nlinarith [h_cos_law r, h_cos_law R, mul_le_mul_of_nonneg_left hr₀r hR.le,
      mul_le_mul_of_nonneg_left hrR hR.le, neg_one_le_cos, cos_le_one]
  grw [← sqrt_sq (norm_nonneg _), ← sqrt_mul (by positivity), this, sqrt_sq (norm_nonneg _)]

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

Goal state before:
pp: case inr
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
this :
  ∀ {U : Set ℂ} (hUo : IsOpen U) (hUc : IsSimplyConnected U) (hU : U ≠ univ),
    0 ∉ U → ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
hU₀ : ¬0 ∉ U
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
rw [ne_univ_iff_exists_notMem] at hU

Goal state after:
case inr
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU✝ : U ≠ univ
hU : ∃ a, a ∉ U
this :
  ∀ {U : Set ℂ} (hUo : IsOpen U) (hUc : IsSimplyConnected U) (hU : U ≠ univ),
    0 ∉ U → ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
hU₀ : ¬0 ∉ U
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: case h
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
x : ℂ
hx : x ∈ U
⊢ ∀ᶠ (x : ℂ) in 𝓝 (-f x), x ∉ f '' U

Tactic:
have : f '' U ∈ 𝓝 (f x) := by
      rw [← (hdf x hx).map_nhds_eq (by simpa using hf₀ x hx)]
      exact Filter.image_mem_map <| hUo.mem_nhds hx

Goal state after:
case h
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
⊢ ∀ᶠ (x : ℂ) in 𝓝 (-f x), x ∉ f '' U
Module: Mathlib.Analysis.Complex.SqrtDeriv

Goal state before:
pp: z : ℂ
hz : z ∈ slitPlane
⊢ 2⁻¹ * z ^ (2⁻¹ - 1) = z ^ (-1 / 2) / 2

Tactic:
show (2 : ℂ)⁻¹ - 1 = -1 / 2 by norm_num,

Goal state after:
z : ℂ
hz : z ∈ slitPlane
⊢ 2⁻¹ * z ^ (-1 / 2) = z ^ (-1 / 2) / 2
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: case inl.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hxc : x < c
xs : x ∈ s
hcy : c ≤ y
⊢ f x < f y

Tactic:
exact (h₁ xs hs.1 hxc).trans_le (h₂.monotoneOn ht.1 (B _ hy hcy) hcy)

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

Goal state before:
pp: case h₂f.h.h
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
z : ℂ
hz : z ∈ sphere c |R|
this : ‖f z‖ ≤ M
⊢ Real.log ‖f z‖ ≤ Real.log M

Tactic:
obtain (h | h) := eq_zero_or_norm_pos (f z)

Goal state after:
case h₂f.h.h.inl
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
z : ℂ
hz : z ∈ sphere c |R|
this : ‖f z‖ ≤ M
h : f z = 0
⊢ Real.log ‖f z‖ ≤ Real.log M

case h₂f.h.h.inr
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
z : ℂ
hz : z ∈ sphere c |R|
this : ‖f z‖ ≤ M
h : 0 < ‖f z‖
⊢ Real.log ‖f z‖ ≤ Real.log M
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.refine_2.inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖
hle₁ : -‖f‖ / 3 ≤ f x
⊢ dist ((g.compContinuous e) x) (f x) ≤ 2 / 3 * ‖f‖

Tactic:
rcases le_total (f x) (‖f‖ / 3) with hle₂ | hle₂
      · simp only [neg_div] at *
        calc
          dist (g (e x)) (f x) ≤ |g (e x)| + |f x| := dist_le_norm_add_norm _ _
          _ ≤ ‖f‖ / 3 + ‖f‖ / 3 := (add_le_add (abs_le.2 <| hgf _) (abs_le.2 ⟨hle₁, hle₂⟩))
          _ = 2 / 3 * ‖f‖ := by linarith
      · calc
          |g (e x) - f x| = f x - ‖f‖ / 3 := by
            rw [hg₂ (mem_image_of_mem _ hle₂), abs_sub_comm, Function.const_apply,
              abs_of_nonneg (sub_nonneg.2 hle₂)]
          _ ≤ 2 / 3 * ‖f‖ := by linarith

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ (m - (scalar (Fin 2)) (m.trace / 2)) ^ 2 = (scalar (Fin 2)) (m.discr / 4)

Tactic:
simp only [scalar_apply, trace_fin_two, discr_fin_two, trace_fin_two,
    det_fin_two, sq, (by norm_num : (4 : K) = 2 * 2)]

Goal state after:
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) =
    diagonal fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
hm : m.IsParabolic
⊢ (m - (scalar (Fin 2)) m.parabolicEigenvalue) ^ 2 = 0

Tactic:
by
  simp [parabolicEigenvalue, -scalar_apply, sub_scalar_sq_eq_discr, hm.2]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
z : ℍ
⊢ g • z = { coe := num g ↑z / denom g ↑z, coe_im_pos := ⋯ }

Tactic:
by
  ext; simp [coe_smul_of_det_pos hg]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : g.IsParabolic
⊢ (↑g).parabolicEigenvalue ≠ 0

Tactic:
have : g.val.trace ^ 2 = 4 * g.val.det := by simpa [sub_eq_zero, discr_fin_two] using hg.2
  rw [parabolicEigenvalue, div_ne_zero_iff, eq_true_intro (two_ne_zero' K), and_true,
    Ne, ← sq_eq_zero_iff, this, show (4 : K) = 2 ^ 2 by norm_num, mul_eq_zero,
    sq_eq_zero_iff, not_or]
  exact ⟨NeZero.ne _, g.det_ne_zero⟩

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

Goal state before:
pp: z : ℍ
N : ℕ
hn : 0 < N
⊢ ∃ n, ModularGroup.T ^ (↑N * n) • z ∈ verticalStrip (↑N) z.im

Tactic:
by
  let n := Int.floor (z.re / N)
  use -n
  rw [modular_T_zpow_smul z (N * -n)]
  refine ⟨?_, by simp⟩
  have h : (N * (-n : ℝ) +ᵥ z).re = -N * Int.floor (z.re / N) + z.re := by
    simp only [n, mul_neg, vadd_re, neg_mul]
  norm_cast at *
  rw [h, add_comm]
  simp only [neg_mul, Int.cast_neg, Int.cast_mul, Int.cast_natCast]
  have hnn : (0 : ℝ) < (N : ℝ) := by norm_cast at *
  have h2 : z.re + -(N * n) = z.re - n * N := by ring
  rw [h2, abs_eq_self.2 (Int.sub_floor_div_mul_nonneg (z.re : ℝ) hnn)]
  apply (Int.sub_floor_div_mul_lt (z.re : ℝ) hnn).le

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
hg : (↑g).IsParabolic
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
⊢ (↑(g ^ n)).IsParabolic

Tactic:
isParabolic_iff_exists

Goal state after:
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
hg : ∃ a n, ↑g = (Matrix.scalar (Fin 2)) a + n ∧ n ≠ 0 ∧ n ^ 2 = 0
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
⊢ ∃ a n_1, ↑(g ^ n) = (Matrix.scalar (Fin 2)) a + n_1 ∧ n_1 ≠ 0 ∧ n_1 ^ 2 = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs : s ∈ 𝓝 τ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
⊢ U ∈ 𝓝 ‖↑τ‖

Tactic:
simp_rw [← isOpenEmbedding_coe.image_mem_nhds, Metric.mem_nhds_iff] at hs ⊢

Goal state after:
τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
hs : ∃ ε > 0, Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
⊢ ∃ ε > 0, Metric.ball ‖↑τ‖ ε ⊆ U
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr.inl
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
hx : x ≠ 0
h_det : det (upperRightHom x) = 1 ∨ det (upperRightHom x) = -1
hg10 : ↑(upperRightHom x) 1 0 = 0
⊢ ↑(upperRightHom x) 0 0 = ↑(upperRightHom x) 1 1 ∧ ↑(upperRightHom x) 0 1 ≠ 0

Tactic:
simpa using hx

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr.inr
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
hx : x ≠ 0
h_det : det (-upperRightHom x) = 1 ∨ det (-upperRightHom x) = -1
hg10 : ↑(-upperRightHom x) 1 0 = 0
⊢ ↑(-upperRightHom x) 0 0 = ↑(-upperRightHom x) 1 1 ∧ ↑(-upperRightHom x) 0 1 ≠ 0

Tactic:
simpa using hx

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

Goal state before:
pp: case neg.h
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ ¬Module.Finite K ↥K⟮x⟯

Tactic:
refine fun H ↦ hx ?_

Goal state after:
case neg.h
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
H : Module.Finite K ↥K⟮x⟯
⊢ IsIntegral K x
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ (algebraMap K E) ((norm K) x) = ∏ σ, σ x

Tactic:
rw [norm_eq_norm_adjoin K x, map_pow, ← adjoin.powerBasis_gen hx,
    norm_eq_prod_embeddings_gen E (adjoin.powerBasis hx) (IsAlgClosed.splits _)]

Goal state after:
L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ (∏ σ, σ (adjoin.powerBasis hx).gen) ^ finrank (↥K⟮x⟯) L = ∏ σ, σ x

L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ IsSeparable K (adjoin.powerBasis hx).gen
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ rexp (dist z w / 2) = (dist ↑z ↑w + dist (↑z) ((starRingEnd ℂ) ↑w)) / (2 * √(z.im * w.im))

Tactic:
by
  rw [← sinh_add_cosh, sinh_half_dist, cosh_half_dist, add_div]

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

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
⊢ R ^ 2 / (dist x c * (R ^ 2 / dist y c)) * dist x (inversion c R y) * dist x c = dist x (inversion c R y) * dist y c

Tactic:
field [dist_ne_zero.2 hx]

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
⊢ Tendsto (inversion c R) (𝓝[≠] c) (Bornology.cobounded P)

Tactic:
by
  rw [← tendsto_dist_left_atTop_iff c]
  have hdist : Tendsto (dist c) (𝓝[≠] c) (𝓝[>] (0 : ℝ)) := by
    rw [tendsto_nhdsWithin_iff]
    refine ⟨tendsto_nhdsWithin_of_tendsto_nhds ?_, eventually_nhdsWithin_of_forall ?_⟩
    · rw [← dist_self c]
      exact ContinuousAt.tendsto <| by fun_prop
    · aesop
  have hratio : Tendsto (fun x : P ↦ dist c (inversion c R x)) (𝓝[≠] c) atTop := by
    simp_rw [dist_center_inversion, div_eq_mul_inv]
    exact hdist.inv_tendsto_nhdsGT_zero.const_mul_atTop <| by rwa [sq_pos_iff]
  simpa using hratio

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

Goal state before:
pp: case e'_9
x : ℂ
⊢ (cexp x + cexp (-x)) * 2⁻¹ = (cexp x - -cexp (-x)) * 2⁻¹

Tactic:
sub_eq_add_neg,

Goal state after:
case e'_9
x : ℂ
⊢ (cexp x + cexp (-x)) * 2⁻¹ = (cexp x + - -cexp (-x)) * 2⁻¹
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z : ℍ
r : ℝ
⊢ dist (↑(z.center r)).im (↑z).im = z.im * (Real.cosh r - 1)

Tactic:
Real.dist_eq,

Goal state after:
z : ℍ
r : ℝ
⊢ |(↑(z.center r)).im - (↑z).im| = z.im * (Real.cosh r - 1)