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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
x : 𝕜
hx : x ∈ U
⊢ toMeromorphicNFOn f U x = f x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
x : 𝕜
hx : x ∉ U
⊢ toMeromorphicNFOn f U x = f x

Tactic:
· simp only [toMeromorphicNFOn, h.meromorphicOn, ↓reduceDIte, hx]
      rw [toMeromorphicNFAt_eq_self.2 (h hx)]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
x : 𝕜
hx : x ∉ U
⊢ toMeromorphicNFOn f U x = f x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inr.inl
𝕜 : 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)
ho : meromorphicOrderAt f x < 0
⊢ False

pp: case inr.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)
ho : 0 < meromorphicOrderAt f x
⊢ False

Tactic:
· apply not_tendsto_atTop_of_tendsto_nhds hc.norm
    rw [tendsto_norm_atTop_iff_cobounded]
    exact tendsto_cobounded_of_meromorphicOrderAt_neg ho

Goal state after:
case inr.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)
ho : 0 < meromorphicOrderAt f x
⊢ False
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inr.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
hc : Tendsto f (𝓝[≠] x) (𝓝 0)
ho : meromorphicOrderAt f x < 0
⊢ False

Tactic:
· apply not_tendsto_atTop_of_tendsto_nhds hc.norm
    rw [tendsto_norm_atTop_iff_cobounded]
    exact tendsto_cobounded_of_meromorphicOrderAt_neg ho

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

Goal state before:
pp: R : ℝ
w : ℂ
⊢ Meromorphic (canonicalFactor R w)

Tactic:
by
  intro x
  unfold canonicalFactor
  fun_prop

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 : 𝕜 → E
x : 𝕜
h : MeromorphicAt f x
h' : ContinuousAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
this : 0 ≤ meromorphicOrderAt f x
n : ℕ
ho : meromorphicOrderAt f x = ↑↑n
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ ↑n • g z
⊢ (fun x_1 ↦ (x_1 - x) ^ n • g x_1) =ᶠ[𝓝[≠] x] f

Tactic:
filter_upwards [hg] with z hz using by simpa using hz.symm

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
ι : Type u_5
s : Finset ι
f : ι → 𝕜 → 𝕜'
hf : ∀ i ∈ s, MeromorphicAt (f i) x
⊢ meromorphicOrderAt (∏ i ∈ s, f i) x = ∑ i ∈ s, meromorphicOrderAt (f i) x

Tactic:
by
  classical
  induction s using Finset.induction with
  | empty =>
    rw [Finset.prod_empty, Finset.sum_empty, ← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]
    · exact ⟨1, analyticAt_const, by simp⟩
    · apply MeromorphicAt.const
  | insert a s ha hs =>
    rw [Finset.sum_insert ha, Finset.prod_insert ha, meromorphicOrderAt_mul
      (hf a (Finset.mem_insert_self a s))
      (MeromorphicAt.prod (fun i hi ↦ hf i (Finset.mem_insert_of_mem hi)))]
    congr
    rw [hs (fun i hi ↦ hf i (Finset.mem_insert_of_mem hi))]

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

Goal state before:
pp: e : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ e 1 / ↑‖e 1‖ ∈ Submonoid.unitSphere ℂ

Tactic:
by simp [Submonoid.unitSphere]

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

Goal state before:
pp: case left.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z = 0
⊢ ∃ t ⊆ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t

pp: case left.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
⊢ ∃ t ⊆ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t

Tactic:
· -- Case: f is locally zero in a punctured neighborhood of z
      rw [← meromorphicOrderAt_eq_top_iff] at h
      tauto

Goal state after:
case left.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
⊢ ∃ t ⊆ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hf : ¬MeromorphicAt f x
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x

Tactic:
· rw [meromorphicOrderAt_of_not_meromorphicAt hf, meromorphicOrderAt_of_not_meromorphicAt]
    rwa [meromorphicAt_smul_iff_of_ne_zero hg hg']

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

Goal state before:
pp: case neg.refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (fun z ↦ ↑(sSupNormIm f 0) ^ (1 - z)) z

pp: case neg.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (HPow.hPow ↑(sSupNormIm f 1)) z

Tactic:
· apply DifferentiableAt.const_cpow (DifferentiableAt.const_sub differentiableAt_id 1) _
      left; simp only [Ne, ofReal_eq_zero]; rwa [eq_comm]

Goal state after:
case neg.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (HPow.hPow ↑(sSupNormIm f 1)) z
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: case inl
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
h✝ : c.im < y ∧ y ≤ z.im
⊢ (y - c.im) ^ 2 ≤ (z.im - c.im) ^ 2

Tactic:
nlinarith

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

Goal state before:
pp: case inr
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
h✝ : z.im < y ∧ y ≤ c.im
⊢ (y - c.im) ^ 2 ≤ (z.im - c.im) ^ 2

Tactic:
nlinarith

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

Goal state before:
pp: case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ f (↑l + 1 * (z - ↑l)) = e

Tactic:
simp [hz₂]

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

Goal state before:
pp: case pos
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 : ℝ
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
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
R : ℝ
hzR : |z.re| < R
hR : ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C
hR₀ : 0 < R
hgd : Differentiable ℂ (g ε)
hd : DiffContOnCl ℂ (fun w ↦ g ε w • f w) (Ioo (-R) R ×ℂ Ioo (a - b) (a + b))
w : ℂ
hw : w ∈ Icc (-R) R ×ℂ {a - b, a + b} ∪ {-R, R} ×ℂ Icc (a - b) (a + b)
him : w.im = a - b ∨ w.im = a + b
⊢ ‖g ε w • f w‖ ≤ C

Tactic:
rw [norm_smul, ← one_mul C]
      gcongr
      exacts [hg₁ _ him, him.by_cases (hle_a _) (hle_b _)]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
f : E → F
x : E
v : 𝕜
hf : ContDiffAt ℝ 2 f x
⊢ Δ (v • f) x = v • Δ f x

Tactic:
by
  simp [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, iteratedFDeriv_const_smul_apply hf,
    Finset.smul_sum]

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 η : ℝ
t₀ : Function.Periodic (fun θ ↦ f (circleMap c R θ)) (2 * π)
⊢ circleAverage f c R = (2 * π)⁻¹ • ∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x)

Tactic:
have := t₀.intervalIntegral_add_eq 0 η

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R η : ℝ
t₀ : Function.Periodic (fun θ ↦ f (circleMap c R θ)) (2 * π)
this : ∫ (x : ℝ) in 0..0 + 2 * π, f (circleMap c R x) = ∫ (x : ℝ) in η..η + 2 * π, f (circleMap c R x)
⊢ circleAverage f c R = (2 * π)⁻¹ • ∫ (x : ℝ) in 0 + η..2 * π + η, f (circleMap c R x)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

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

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

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

Goal state before:
pp: case neg
x y : ℝ
hx : ¬x = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Tactic:
by_cases hy : y = 0

Goal state after:
case pos
x y : ℝ
hx : ¬x = 0
hy : y = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

case neg
x y : ℝ
hx : ¬x = 0
hy : ¬y = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: x : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
hx₂ : x ≠ -1
⊢ HasDerivAt (fun x ↦ (log x)⁻¹) (-x⁻¹ / log x ^ 2) x

Tactic:
simpa using (differentiableAt_inv_log hx₀ hx₁ hx₂).hasDerivAt

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:
simpa only [exists_prop] using! hfc.norm.exists_isMaxOn' isClosed_Ici hx₀ this

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

Goal state before:
pp: case neg.inl
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 < r.re
⊢ IntervalIntegrable (fun x ↦ ↑x ^ r) μ a b

Tactic:
exact (Complex.continuous_ofReal_cpow_const h').intervalIntegrable _ _

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

Goal state before:
pp: case funProp.discharger
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
x✝ : ℝ
⊢ 1 + x✝ ^ 2 ≠ 0

Tactic:
nlinarith

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

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

Tactic:
have :
    (∫ x in a..b, (x : ℂ) ^ (r : ℂ)) = ((b : ℂ) ^ (r + 1 : ℂ) - (a : ℂ) ^ (r + 1 : ℂ)) / (r + 1) :=
    integral_cpow h'

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

Goal state before:
pp: case hcont
a b : ℝ
⊢ ContinuousOn sin [[a, b]]

Tactic:
exact continuousOn_sin

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

Goal state before:
pp: case refine_2
a b x : ℝ
⊢ 1 + x ^ 2 ≠ 0

Tactic:
nlinarith

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

Goal state before:
pp: case convert_3
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ↑t ≠ -↑1

Tactic:
← ofReal_neg,

Goal state after:
case convert_3
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ↑t ≠ ↑(-1)
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
| cuspFunction h f 0

Tactic:
simp only [cuspFunction, update_self]

Goal state after:
h : ℝ
f : ℂ → ℂ
| (𝓝[≠] 0).limUnder (f ∘ invQParam h)
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ IsOpenQuotientMap fun x ↦ x ^ n

Tactic:
convert! Polynomial.isOpenQuotientMap_eval (.X ^ n) _

Goal state after:
n : ℕ
inst✝ : NeZero n
x✝ : ℂ
⊢ x✝ ^ n = Polynomial.eval x✝ (Polynomial.X ^ n)

n : ℕ
inst✝ : NeZero n
⊢ (Polynomial.X ^ n).natDegree ≠ 0
Module: Mathlib.Analysis.Complex.Positivity

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ ↑(z - c).re
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * ↑(z - c).re ^ n = f z
hz' : z - c = ↑(z - c).re
n : ℕ
⊢ 0 ≤ (↑↑n.factorial)⁻¹ * iteratedDeriv n f c * ↑((z - c).re ^ n)

Tactic:
← ofReal_inv,

Goal state after:
f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ ↑(z - c).re
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * ↑(z - c).re ^ n = f z
hz' : z - c = ↑(z - c).re
n : ℕ
⊢ 0 ≤ ↑(↑n.factorial)⁻¹ * iteratedDeriv n f c * ↑((z - c).re ^ n)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
this :
  (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) =
    Complex.re ∘ herglotzRieszKernel 0 (w - c) • fun x ↦ log ‖x - (ρ - c)‖
⊢ circleAverage (Complex.re ∘ herglotzRieszKernel 0 (w - c) • fun x ↦ log ‖x - (ρ - c)‖) 0 R = log ‖w - ρ‖

Tactic:
circleAverage_re_herglotzRieszKernel_mul_log₀ (by simp_all)
    (by simp_all [mem_ball_iff_norm.1 hw])

Goal state after:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
this :
  (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) =
    Complex.re ∘ herglotzRieszKernel 0 (w - c) • fun x ↦ log ‖x - (ρ - c)‖
⊢ log ‖w - c - (ρ - c)‖ = log ‖w - ρ‖
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
⊢ sqrt (-a) = I * sqrt a

Tactic:
by
  obtain (h | h) := I_eq_zero_or_im_I_eq_one (K := 𝕜)
  · simp [h, sqrt_eq_ite, Real.sqrt_eq_zero', nonneg_iff.mp ha]
  rw [sqrt_eq_ite, dif_pos h, RingEquiv.symm_apply_eq, map_neg,
    Complex.sqrt_neg_of_nonneg (by simpa)]
  simp [h, sqrt, map_mul]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
τ : ℍ
⊢ -(2 * π * τ.im / ↑n) < 0

Tactic:
neg_lt_zero,

Goal state after:
n : ℕ
inst✝ : NeZero n
τ : ℍ
⊢ 0 < 2 * π * τ.im / ↑n
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: Y : Type v
Z : Type w
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, Y)
g : C(X✝, Z)
hg : ContinuousMap.restrict s g = ι.comp f
⊢ ∃ g, ContinuousMap.restrict s g = f

Tactic:
use r.comp g

Goal state after:
case h
Y : Type v
Z : Type w
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, Y)
g : C(X✝, Z)
hg : ContinuousMap.restrict s g = ι.comp f
⊢ ContinuousMap.restrict s (r.comp g) = f
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Goal state before:
pp: case H
n : Type u_1
R : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Nonempty n
h : Function.Surjective ⇑toPGL
r : Rˣ
A : GL n R
hA : GeneralLinearGroup.det A = r
X : SpecialLinearGroup n R
hX : toPGL ↑X = mk A
⊢ ∃ k, k ^ Fintype.card n = r

Tactic:
obtain ⟨u, hu⟩ : ∃ u, toGL X * (GeneralLinearGroup.scalar n) u = A := by
    simpa [mk_eq_mk_iff] using hX

Goal state after:
case H
n : Type u_1
R : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Nonempty n
h : Function.Surjective ⇑toPGL
r : Rˣ
A : GL n R
hA : GeneralLinearGroup.det A = r
X : SpecialLinearGroup n R
hX : toPGL ↑X = mk A
u : Rˣ
hu : toGL X * (GeneralLinearGroup.scalar n) u = A
⊢ ∃ k, k ^ Fintype.card n = r
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case inl.inl
g g' : GL (Fin 2) ℝ
z : ℂ
h : (↑g).det < 0
h' : (↑g').det < 0
⊢ (if 0 < ↑(GeneralLinearGroup.det g) * ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ
      else Complex.conjCAE)
      z =
    (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
      ((if 0 < ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z)

Tactic:
simp [mul_pos_of_neg_of_neg h h', h.not_gt, h'.not_gt]

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

Goal state before:
pp: case mpr
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ (∃ a n, m = (scalar (Fin 2)) a + n ∧ n ≠ 0 ∧ n ^ 2 = 0) → m.IsParabolic

Tactic:
rintro ⟨a, n, hm, hn0, hnsq⟩
    constructor
    · refine fun ⟨b, hb⟩ ↦ hn0 ?_
      rw [← sub_eq_iff_eq_add'] at hm
      simpa only [← hm, ← hb, ← map_sub, ← map_pow, ← map_zero (scalar (Fin 2)), scalar_inj,
        sq_eq_zero_iff] using hnsq
    · suffices scalar (Fin 2) (m.discr / 4) = 0 by
        rw [← map_zero (scalar (Fin 2)), scalar_inj, div_eq_zero_iff] at this
        have : (4 : K) ≠ 0 := by simpa [show (4 : K) = 2 ^ 2 by norm_num] using NeZero.ne _
        tauto
      rw [← sub_scalar_sq_eq_discr, hm, trace_add, scalar_apply, trace_diagonal]
      simp [mul_div_cancel_left₀ _ (NeZero.ne (2 : K)),
        (Matrix.isNilpotent_trace_of_isNilpotent ⟨2, hnsq⟩).eq_zero, hnsq]

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).trace ^ 2 = 4 * (↑g).det

Tactic:
simpa [sub_eq_zero, discr_fin_two] using hg.2

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
c : ℝ := ↑g 1 0
d : ℝ := ↑g 1 1
⊢ (c * z.im) ^ 2 ≤ (c * z.im) ^ 2 + (c * z.re + d) ^ 2

Tactic:
nlinarith

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_1
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
hgf : ⇑g ∘ e = ⇑f
ha' : ¬∃ x, f x = a
⊢ Disjoint (range e) (⇑g ⁻¹' {a})

Tactic:
rw [Set.disjoint_left]

Goal state after:
case refine_1
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
hgf : ⇑g ∘ e = ⇑f
ha' : ¬∃ x, f x = a
⊢ ∀ ⦃a_1 : Y⦄, a_1 ∈ range e → a_1 ∉ ⇑g ⁻¹' {a}
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: i✝ j✝ : Fin 2
⊢ ↑(J ^ 2) i✝ j✝ = ↑1 i✝ j✝

Tactic:
simp [J, sq, Matrix.one_fin_two]

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

Goal state before:
pp: z : ℍ
⊢ denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) S)) ↑z = ↑z

Tactic:
by simp [S, denom_apply]

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

Goal state before:
pp: S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k : m
⊢ (auxMat M k).toSquareBlock (fun x ↦ x ≠ k) False = 1

Tactic:
ext ⟨i, hi⟩ ⟨j, hj⟩

Goal state after:
S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k i : m
hi : (i ≠ k) = False
j : m
hj : (j ≠ k) = False
⊢ (auxMat M k).toSquareBlock (fun x ↦ x ≠ k) False ⟨i, hi⟩ ⟨j, hj⟩ = 1 ⟨i, hi⟩ ⟨j, hj⟩
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ (M * auxMat M k).toSquareBlock (fun x ↦ x = k) True = M k k • 1

Tactic:
ext ⟨i, hi⟩ ⟨j, hj⟩

Goal state after:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i : m
hi : (i = k) = True
j : m
hj : (j = k) = True
⊢ (M * auxMat M k).toSquareBlock (fun x ↦ x = k) True ⟨i, hi⟩ ⟨j, hj⟩ = (M k k • 1) ⟨i, hi⟩ ⟨j, hj⟩