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 : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ f =ᶠ[codiscreteWithin (closedBall 0 R)]
    (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (-(divisor f (ball 0 R)) i)) •
      (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f

Tactic:
finprod_eq_prod_of_mulSupport_subset_of_finite _ (by aesop) η₀

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ f =ᶠ[codiscreteWithin (closedBall 0 R)]
    (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (-(divisor f (ball 0 R)) i)) •
      (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (divisor f (ball 0 R)) i) • f
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := ⋯
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := ⋯
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (-(divisor f (ball 0 R)) i)) • φ =ᶠ[codiscreteWithin (closedBall 0 R)]
    (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g

Tactic:
finprod_eq_prod_of_mulSupport_subset_of_finite _ (by aesop) η₀

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (-(divisor f (ball 0 R)) i)) • φ =ᶠ[codiscreteWithin (closedBall 0 R)]
    (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (-(divisor f (ball 0 R)) i)) • g
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)

Tactic:
by
  have minor₁ : ‖map 1‖ ≠ 0 := by
    simpa only [ContinuousLinearMap.ext_ring_iff, Ne, norm_eq_zero] using! nonzero
  refine ⟨‖map 1‖, minor₁, ⟨‖map 1‖⁻¹ • ((map : ℂ →ₗ[ℂ] E) : ℂ →ₗ[ℝ] E), ?_⟩, ?_⟩
  · intro x
    simp only [LinearMap.smul_apply]
    have : x = x • (1 : ℂ) := by rw [smul_eq_mul, mul_one]
    nth_rw 1 [this]
    rw [LinearMap.coe_restrictScalars]
    simp only [map.coe_coe, map.map_smul, norm_smul, norm_inv, norm_norm]
    field
  · ext1
    simp [minor₁]

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

Goal state before:
pp: ⊢ 2.7182818283 < 2244083 / 825552 - 1 / 10 ^ 10

Tactic:
by norm_num

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

Goal state before:
pp: ⊢ 1 / 10 ^ 10 + 2244083 / 825552 < 2.7182818286

Tactic:
by norm_num

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

Goal state before:
pp: ⊢ 2 < 2.7182818283

Tactic:
by norm_num

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

Goal state before:
pp: ⊢ 2.7182818286 < 3

Tactic:
by norm_num

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

Goal state before:
pp: ⊢ 0 < 0.3678794412

Tactic:
by norm_num

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

Goal state before:
pp: ⊢ 0.3678794412⁻¹ < 2244083 / 825552 - 1 / 10 ^ 10

Tactic:
by norm_num

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

Goal state before:
pp: ⊢ 0.3678794412 < 1 / 2

Tactic:
by norm_num

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

Goal state before:
pp: ⊢ 1 / 10 ^ 10 + 287209 / 414355 < 0.6931471808

Tactic:
by norm_num

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

Goal state before:
pp: t : |2 / 3| = 2 / 3
⊢ |2 / 3| < 1

Tactic:
by norm_num

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

Goal state before:
pp: ⊢ 1 / 10 ^ 10 + 109861228867 / 100000000000 < 1.0986122888

Tactic:
by norm_num

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

Goal state before:
pp: t : |4 / 5| = 4 / 5
⊢ |4 / 5| < 1

Tactic:
by norm_num

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

Goal state before:
pp: ⊢ 1 / 10 ^ 10 + 160943791243 / 100000000000 < 1.6094379126

Tactic:
by norm_num

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
X✝ Y✝ Z✝ : FundamentalGroupoid X
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ↑(p ⁻¹' {X✝.as})
⊢ (ConcreteCategory.hom (↾cov.monodromy (x✝² ≫ x✝¹))).toFun x✝ =
    (ConcreteCategory.hom (↾cov.monodromy x✝² ≫ ↾cov.monodromy x✝¹)).toFun x✝

Tactic:
simpa using! cov.monodromy_trans_apply _ _ _

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

Goal state before:
pp: case hb
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ Differentiable ℂ fun z ↦ (↑ε + ↑(sSupNormIm f 1)) ^ (-z)

Tactic:
apply Differentiable.const_cpow (Differentiable.neg differentiable_id)
    apply Or.inl
    rw [← ofReal_add, ofReal_ne_zero]
    exact (ne_of_gt (sSupNormIm_eps_pos f hε 1))

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
p : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
g : G
x y : X
γ : Path.Homotopic.Quotient x y
e : ↑(p ⁻¹' {x})
Γ : Path.Homotopic.Quotient ↑e ↑(⋯.monodromy γ e) := ⋯.liftPathQuotient γ e
g' : C(E, E) := { toFun := fun x ↦ g • x, continuous_toFun := ⋯ }
p' : C(E, X) := { toFun := p, continuous_toFun := ⋯ }
a✝ : E
⊢ (p'.comp g') a✝ = p' a✝

Tactic:
simp [g', p', hp.map_smul]

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case e'_1.e'_3
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
p : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
g : G
x y : X
γ : Path.Homotopic.Quotient x y
e : ↑(p ⁻¹' {x})
Γ : Path.Homotopic.Quotient ↑e ↑(⋯.monodromy γ e) := ⋯.liftPathQuotient γ e
g' : C(E, E) := { toFun := fun x ↦ g • x, continuous_toFun := ⋯ }
p' : C(E, X) := { toFun := p, continuous_toFun := ⋯ }
hgp : p'.comp g' = p'
⊢ p' (g' ↑e) = { toFun := p, continuous_toFun := ⋯ } ↑e

Tactic:
simp [g', p', hp.map_smul]

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case e'_1.e'_4
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
p : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
g : G
x y : X
γ : Path.Homotopic.Quotient x y
e : ↑(p ⁻¹' {x})
Γ : Path.Homotopic.Quotient ↑e ↑(⋯.monodromy γ e) := ⋯.liftPathQuotient γ e
g' : C(E, E) := { toFun := fun x ↦ g • x, continuous_toFun := ⋯ }
p' : C(E, X) := { toFun := p, continuous_toFun := ⋯ }
hgp : p'.comp g' = p'
⊢ p' (g' ↑(⋯.monodromy γ e)) = { toFun := p, continuous_toFun := ⋯ } ↑(⋯.monodromy γ e)

Tactic:
simp [g', p', hp.map_smul]

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
p : E → X
G : Type u_4
inst✝² : Group G
inst✝¹ : MulAction G E
hp : IsQuotientCoveringMap p G
x : X
e : ↑(p ⁻¹' {x})
inst✝ : PathConnectedSpace E
g : Gᵐᵒᵖ
e' : ↑(p ⁻¹' {x}) := ⟨MulOpposite.unop g • ↑e, ⋯⟩
he' : e' = ⟨MulOpposite.unop g • ↑e, ⋯⟩
Γ : Path ↑e ↑e' := { toFun := ⇑(PathConnectedSpace.somePath ↑e ↑e'), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
⊢ x = p ↑e

Tactic:
simpa using e.property.symm

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
z : ℂ
⊢ interpStrip (scale f l u) ((z - ↑l) / (↑u - ↑l)) = interpStrip' f l u z

Tactic:
simp only [interpStrip, interpStrip']
  simp_rw [sSupNormIm_scale_left f hul, sSupNormIm_scale_right f hul]

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

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ (a - b)⁻¹ • ∫ (x : ℝ) in Ioc b a, f x = -((b - a)⁻¹ • ∫ (x : ℝ) in Ioc b a, f x ∂volume)

Tactic:
← neg_smul,

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ (a - b)⁻¹ • ∫ (x : ℝ) in Ioc b a, f x = -(b - a)⁻¹ • ∫ (x : ℝ) in Ioc b a, f x ∂volume
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: case neg
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
hR : ¬R = 0
H : ContinuousOn (circleAverage (⇑g ∘ f) c) (Set.Ioc 0 |R|)
r : ℝ
hr : r ∈ Set.Ioo 0 |R|
⊢ circleAverage (⇑g ∘ f) c r = (fun x ↦ g (f c)) r

Tactic:
apply HarmonicOnNhd.circleAverage_eq

Goal state after:
case neg
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
hR : ¬R = 0
H : ContinuousOn (circleAverage (⇑g ∘ f) c) (Set.Ioc 0 |R|)
r : ℝ
hr : r ∈ Set.Ioo 0 |R|
⊢ HarmonicOnNhd (⇑g ∘ f) (closedBall c |r|)
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: a b : ℂ
⊢ ((a.re + b.re) * (a.re - b.re) + (a.im + b.im) * (a.im - b.im)) / ‖a - b‖ ^ 2 =
    (a.re * a.re + a.im * a.im - (b.re * b.re + b.im * b.im)) / ‖a - b‖ ^ 2

Tactic:
by
      congr! 1; ring

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

Goal state before:
pp: x : ℝ
h0 : 0 ≤ x
⊢ x - 1 ≤ x * log x

Tactic:
by
  rcases eq_or_ne x 1 with rfl | h1
  · simp
  · exact le_of_lt (self_sub_one_lt_mul_log h0 h1)

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

Goal state before:
pp: x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
⊢ x.negMulLog < 1 - x

Tactic:
unfold negMulLog
  linarith [self_sub_one_lt_mul_log h0 h1]

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

Goal state before:
pp: ⊢ ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 0

Tactic:
simp only [← hasDerivAt_deriv_iff, hasDerivAt_iff_tendsto_slope_zero, zero_add, log_zero,
    inv_zero, sub_zero, smul_eq_mul, ← mul_inv, mul_comm _ (log _)]

Goal state after:
⊢ ¬Tendsto (fun t ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (fun x ↦ (log x)⁻¹) 0))
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case refine_1
s t : ℝ
ht : 0 < t
h : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 t) volume
⊢ -1 < s

Tactic:
contrapose! h

Goal state after:
case refine_1
s t : ℝ
ht : 0 < t
h : s ≤ -1
⊢ ¬IntegrableOn (fun x ↦ x ^ s) (Ioo 0 t) volume
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
z : ℂ
hz : z.re ≤ 0
⊢ |x₀ - z.re| = |(z - ↑x₀).re|

Tactic:
rw [sub_re, ofReal_re, _root_.abs_sub_comm]

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

Goal state before:
pp: case hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : ↑[[a, b]]), meromorphicOrderAt f ↑u ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : ↑[[a, b]]), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin [[a, b]]] (∏ᶠ (u : ℝ), (fun x ↦ x - u) ^ (divisor f [[a, b]]) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    (∑ᶠ (u : ℝ), fun x ↦ ↑((divisor f [[a, b]]) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
⊢ IntervalIntegrable (fun x ↦ log ‖g x‖) volume a b

Tactic:
· apply ContinuousOn.intervalIntegrable
      apply h₁g.continuousOn.norm.log
      simp_all

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 : ℝ
⊢ expR 0 * ‖f (↑y * I)‖ ≤ C

Tactic:
Real.exp_zero,

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 : ℝ
⊢ 1 * ‖f (↑y * I)‖ ≤ C
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

Tactic:
simp only [mul_comm Complex.I, Complex.exp_mul_I, Complex.cos_neg, Complex.sin_neg,
      add_sub_add_left_eq_sub, Complex.div_I, Complex.ofReal_sin]

Goal state after:
r : ℝ
⊢ -((Complex.sin ↑r * Complex.I - -Complex.sin ↑r * Complex.I) * Complex.I) = 2 * Complex.sin ↑r
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: 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
⊢ EqOn f 0 {z | 0 ≤ z.re}

Tactic:
suffices ∀ z : ℂ, 0 < z.re → f z = 0 by
    simpa only [closure_setOfPred_lt_re] using!
      EqOn.of_subset_closure this hd.continuousOn continuousOn_const subset_closure Subset.rfl

Goal state after:
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
⊢ ∀ (z : ℂ), 0 < z.re → f z = 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: ⊢ 4 = 2 * 2

Tactic:
by norm_num

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
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 : ℝ
⊢ expR 0 ^ n * ‖f (↑y * I)‖ ≤ C

Tactic:
Real.exp_zero,

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 : ℝ
⊢ 1 ^ n * ‖f (↑y * I)‖ ≤ C
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * ↑π * I / ↑h)) z
diff_ne : q * (2 * ↑π * I / ↑h) ≠ 0
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * ↑π * I / ↑h)) z qdiff diff_ne
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Tactic:
have diff_L : DifferentiableAt ℂ L q :=
    (qdiff.to_localInverse diff_ne).hasStrictFDerivAt.differentiableAt

Goal state after:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * ↑π * I / ↑h)) z
diff_ne : q * (2 * ↑π * I / ↑h) ≠ 0
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * ↑π * I / ↑h)) z qdiff diff_ne
diff_L : DifferentiableAt ℂ L q
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
a : ℂ
⊢ cuspFunction h (a • f) = a • cuspFunction h f

Tactic:
simp only [cuspFunction] at *
  ext y
  obtain rfl | hy := eq_or_ne y 0
  · simpa using! (Tendsto.const_mul _ (by simpa using! hfcts)).limUnder_eq
  · simp [hy]

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
hzP : ¬eval z P = 0
⊢ ∑ x ∈ s, weight x • (z - x) = (starRingEnd ℂ) (∑ x ∈ s, rootMultiplicity x P • (1 / (z - x)))

Tactic:
simp only [map_sum, weight, derivRootWeight, if_neg hzP]

Goal state after:
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
hzP : ¬eval z P = 0
⊢ ∑ x ∈ s, (↑(rootMultiplicity x P) / ‖z - x‖ ^ 2) • (z - x) =
    ∑ x ∈ s, (starRingEnd ℂ) (rootMultiplicity x P • (1 / (z - x)))
Module: Mathlib.Analysis.Complex.SqrtDeriv

Goal state before:
pp: z : ℂ
hz : 0 ≤ z.re ∨ z.im ≠ 0
⊢ 0 < 2⁻¹.re

Tactic:
by norm_num

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
h : SummableLocallyUniformlyOn f s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
⊢ DifferentiableOn ℂ (fun z ↦ ∑' (n : ι), f n z) s

Tactic:
obtain ⟨g, hg⟩ := h
  have hc := (hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn.mp hg).differentiableOn ?_ hs
  · apply hc.congr
    apply hg.tsum_eqOn
  · filter_upwards with t r hr using
      DifferentiableWithinAt.fun_sum fun a ha ↦ (hf2 a r hr).differentiableWithinAt

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

Goal state before:
pp: case refine_2
𝕜 : 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
⊢ ContinuousOn g (closure (Metric.closedBall 0 1)ᶜ)

Tactic:
· refine continuousOn_id.norm.inv₀ ?_ |>.smul continuousOn_id
    simp only [closure_compl, interior_closedBall (0 : E) one_ne_zero, mem_compl_iff,
      Metric.mem_ball, dist_zero_right, not_lt, id_eq, ne_eq, norm_eq_zero]
    exact fun x hx ↦ norm_pos_iff.mp <| one_pos.trans_le hx

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

Goal state before:
pp: ⊢ 0 < 2⁻¹

Tactic:
by norm_num

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
⊢ 4 = 2 * 2

Tactic:
by norm_num

Goal state after:
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 / ↑‖↑τ‖ * ↑τ - ↑τ‖ < ε

Tactic:
show r / ‖(τ : ℂ)‖ * (τ : ℂ) - τ = ↑(r / ‖(τ : ℂ)‖ - 1) * (τ : ℂ) by simp; ring,

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.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
he : IsClosedEmbedding e
⊢ ∃ g, (∀ (y : Y), g y ∈ Icc a b) ∧ ⇑g ∘ e = ⇑f

Tactic:
rcases exists_extension_norm_eq_of_isClosedEmbedding (f - const X ((a + b) / 2)) he with
    ⟨g, hgf, hge⟩
  refine ⟨const Y ((a + b) / 2) + g, fun y => ?_, ?_⟩
  · suffices ‖f - const X ((a + b) / 2)‖ ≤ (b - a) / 2 by
      simpa [Real.Icc_eq_closedBall, add_mem_closedBall_iff_norm] using
        (norm_coe_le_norm g y).trans (hgf.trans_le this)
    refine (norm_le <| div_nonneg (sub_nonneg.2 hle) zero_le_two).2 fun x => ?_
    simpa only [Real.Icc_eq_closedBall] using! hf x
  · ext x
    have : g (e x) = f x - (a + b) / 2 := congr_fun hge x
    simp [this]

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

Goal state before:
pp: a b : SL(2, ℤ)
⊢ coe a = coe b ↔ a = b

Tactic:
refine ⟨fun h ↦ a.ext b fun i j ↦ ?_, congr_arg _⟩
  simp only [Subtype.ext_iff, GeneralLinearGroup.ext_iff] at h
  simpa [coe] using h i j

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}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ ∃ᶠ (z : ℂ) in 𝓝[≠] ↑τ, (f ∘ ↑ofComplex) z = 0

Tactic:
contrapose! hτ

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 𝓝[≠] ↑τ, (f ∘ ↑ofComplex) x ≠ 0
⊢ ∀ᶠ (x : ℍ) in 𝓝[≠] τ, f x ≠ 0
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ c
⊢ dist c c * dist b d ≤ dist c b * dist c d + dist b c * dist c d

Tactic:
rw [dist_self, zero_mul]
    positivity

Goal state after: