mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ MapsTo (fun z ↦ ↑l + z • (↑u - ↑l)) (verticalStrip 0 1) (verticalStrip l u)

Tactic:
MapsTo

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ ∀ ⦃x : ℂ⦄, x ∈ verticalStrip 0 1 → ↑l + x • (↑u - ↑l) ∈ verticalStrip l u
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
⊢ HarmonicAt f₁ x ↔ HarmonicAt f₂ x

Tactic:
constructor <;> intro hf

Goal state after:
case mp
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
hf : HarmonicAt f₁ x
⊢ HarmonicAt f₂ x

case mpr
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
hf : HarmonicAt f₂ x
⊢ HarmonicAt f₁ x
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
⊢ ContDiffWithinAt ℝ 2 f₁ s y →
    ContDiffWithinAt ℝ 2 f₂ s y → y ∈ insert x s → (Δ[s] f₁ + f₂) y = ((Δ[s] f₁) + Δ[s] f₂) y

Tactic:
h₁y

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
⊢ ContDiffWithinAt ℝ 2 f₂ s y → y ∈ insert x s → (Δ[s] f₁ + f₂) y = ((Δ[s] f₁) + Δ[s] f₂) y
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
⊢ ContDiffWithinAt ℝ 2 f₁ s y →
    ContDiffWithinAt ℝ 2 f₂ s y → y ∈ insert x s → (Δ[s] f₁ - f₂) y = ((Δ[s] f₁) - Δ[s] f₂) y

Tactic:
h₁y

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
⊢ ContDiffWithinAt ℝ 2 f₂ s y → y ∈ insert x s → (Δ[s] f₁ - f₂) y = ((Δ[s] f₁) - Δ[s] f₂) y
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
s : Set E
v : 𝕜
hf : ContDiffWithinAt ℝ 2 f s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ (Δ[s] v • f) x = v • (Δ[s] f) x

Tactic:
simp [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs hx,
    iteratedFDerivWithin_const_smul_apply hf hs hx,
    Finset.smul_sum]

Goal state after:
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)
⊢ z.wedgeIntegral w f - (w - z) • f z =
    ((fun w ↦ (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - (w - z).re • f z) +
        I • fun w ↦ (∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) - (w - z).im • f z)
      w

Tactic:
set I₂ := ∫ y in z.im..w.im, f (w.re + y * I)

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)
⊢ z.wedgeIntegral w f - (w - z) • f z =
    ((fun w ↦ (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - (w - z).re • f z) +
        I • fun w ↦ (∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) - (w - z).im • f z)
      w
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: case right.hf'
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = ↑(f z) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
x : ℂ
hx : x ∈ ball z R
y : ℂ
hy : y ∈ ball z R
⊢ fderivWithin ℝ (⇑reCLM ∘ F) (ball z R) y = fderivWithin ℝ f (ball z R) y

Tactic:
have h₄F := (hF.2 y hy).differentiableAt

Goal state after:
case right.hf'
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = ↑(f z) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
x : ℂ
hx : x ∈ ball z R
y : ℂ
hy : y ∈ ball z R
h₄F : DifferentiableAt ℂ F y
⊢ fderivWithin ℝ (⇑reCLM ∘ F) (ball z R) y = fderivWithin ℝ f (ball z R) y
Module: Mathlib.Analysis.Complex.MeanValue

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
⊢ circleAverage (fun z ↦ ((z - c) / (z - w)) • f z) c R = f w

Tactic:
by
  rw [← circleAverage_abs_radius]
  rcases le_or_gt |R| 0 with hR | hR
  · simp_all [ball_eq_empty.2 hR]
  calc circleAverage (fun z ↦ ((z - c) * (z - w)⁻¹) • f z) c |R|
  _ = (2 * π * I)⁻¹ • (∮ z in C(c, |R|), (z - w)⁻¹ • f z) := by
    simp only [circleAverage_eq_circleIntegral hR.ne', mul_inv_rev, inv_I, neg_mul, neg_smul,
      neg_inj, ne_eq, mul_eq_zero, I_ne_zero, inv_eq_zero, ofReal_eq_zero, pi_ne_zero,
      OfNat.ofNat_ne_zero, or_self, not_false_eq_true, smul_right_inj]
    apply circleIntegral.integral_congr hR.le
    intro z hz
    match_scalars
    have : z - c ≠ 0 := by grind [ne_of_mem_sphere]
    grind
  _ = f w := by
    rw [circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw h₁f h₂f]
    match_scalars
    simp [field]

Goal state after:
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 : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ({z | ‖z - c‖ ∈ s}.domRestrict f)
hs : ∀ r ∈ s, 0 ≤ r
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s.domRestrict (Real.circleAverage f c))

Tactic:
apply (intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' _ _ _).const_smul

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
s : Set ℝ
c : ℂ
hf : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ({z | ‖z - c‖ ∈ s}.domRestrict f)
hs : ∀ r ∈ s, 0 ≤ r
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry fun x θ ↦ f (circleMap c (↑x) θ))
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℂ
f : ℂ → E
hf : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Real.circleAverage f c)

Tactic:
apply (intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' _ _ _).const_smul

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℂ
f : ℂ → E
hf : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry fun R θ ↦ f (circleMap c R θ))
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: ⊢ Tendsto (fun x ↦ derivWithin (fun x ↦ x * log x) (Set.Ioi x) x) atTop atTop

Tactic:
by
  refine (tendsto_congr' ?_).mpr (tendsto_log_atTop.atTop_add (tendsto_const_nhds (x := 1)))
  rw [EventuallyEq, eventually_atTop]
  exact ⟨1, fun _ hx ↦ rightDeriv_mul_log (zero_lt_one.trans_le hx).ne'⟩

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
⊢ HarmonicAt (fun x ↦ Real.log ‖f x‖) z

Tactic:
have : (Real.log ‖f ·‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
    funext z
    simp only [Pi.smul_apply, Function.comp_apply, smul_eq_mul]
    rw [Complex.norm_def, Real.log_sqrt]
    · linarith
    exact (f z).normSq_nonneg

Goal state after:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun x ↦ Real.log ‖f x‖) = 2⁻¹ • Real.log ∘ ⇑normSq ∘ f
⊢ HarmonicAt (fun x ↦ Real.log ‖f x‖) z
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: H : Tendsto (fun t ↦ (log t * t)⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds (deriv (fun x ↦ (log x)⁻¹) 0))
x : ℝ
x✝ : x ∈ Set.Ioo (-1) 0
hx₁ : -1 < x
hx₂ : x < 0
⊢ log x < 0

Tactic:
apply log_neg_eq_log x ▸ log_neg <;> grind

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

Goal state before:
pp: a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun t ↦ ‖↑t ^ r‖) volume 0 c

pp: a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ AEStronglyMeasurable (fun x ↦ ↑x ^ r) (volume.restrict (Ι 0 c))

Tactic:
· rw [intervalIntegrable_iff]
      apply IntegrableOn.congr_fun
      · rw [← intervalIntegrable_iff]; exact intervalIntegral.intervalIntegrable_rpow' h
      · intro x hx
        rw [uIoc_of_le hc] at hx
        dsimp only
        rw [Complex.norm_cpow_eq_rpow_re_of_pos hx.1]
      · exact measurableSet_uIoc

Goal state after:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ AEStronglyMeasurable (fun x ↦ ↑x ^ r) (volume.restrict (Ι 0 c))
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

Goal state before:
pp: t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
t₁ : cos ⁻¹' {0}ᶜ ∈ codiscrete ℝ
y : ℝ
⊢ y ∈ sin ⁻¹' {0}ᶜ → y ∈ cos ⁻¹' {0}ᶜ → log (sin y) = log (sin (2 * y)) - log 2 - log (cos y)

Tactic:
h₁y

Goal state after:
t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
t₁ : cos ⁻¹' {0}ᶜ ∈ codiscrete ℝ
y : ℝ
h₁y : y ∈ sin ⁻¹' {0}ᶜ
⊢ y ∈ cos ⁻¹' {0}ᶜ → log (sin y) = log (sin (2 * y)) - log 2 - log (cos y)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: ⊢ ∫ (x : ℝ) in 0..2 * π, log (4 * sin (x / 2) ^ 2) / 2 = 0

Tactic:
by
  calc ∫ x in 0..(2 * π), log (4 * sin (x / 2) ^ 2) / 2
  _ = ∫ (x : ℝ) in 0..π, log (4 * sin x ^ 2) := by
    have {x : ℝ} : x / 2 = 2⁻¹ * x := by ring
    rw [intervalIntegral.integral_div, this, inv_mul_integral_comp_div
      (f := fun x ↦ log (4 * sin x ^ 2))]
    simp
  _ = ∫ (x : ℝ) in 0..π, log 4 + 2 * log (sin x) := by
    apply integral_congr_codiscreteWithin
    apply codiscreteWithin_mono (by tauto : Ι 0 π ⊆ Set.univ)
    have : AnalyticOnNhd ℝ (4 * sin · ^ 2) Set.univ := fun _ _ ↦ by fun_prop
    have := this.preimage_zero_mem_codiscrete (x := π / 2)
    simp only [sin_pi_div_two, one_pow, mul_one, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
      Set.preimage_compl, forall_const] at this
    filter_upwards [this] with a ha
    simp only [Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff, mul_eq_zero,
      OfNat.ofNat_ne_zero, ne_eq, not_false_eq_true, pow_eq_zero_iff, false_or] at ha
    rw [log_mul (by simp) (by simp_all), log_pow, Nat.cast_ofNat]
  _ = (∫ (x : ℝ) in 0..π, log 4) + 2 * ∫ (x : ℝ) in 0..π, log (sin x) := by
    rw [integral_add _root_.intervalIntegrable_const
      (by apply intervalIntegrable_log_sin.const_mul 2), intervalIntegral.integral_const_mul]
  _ = 0 := by
    simp only [intervalIntegral.integral_const, sub_zero, smul_eq_mul, integral_log_sin_zero_pi,
      (by norm_num : (4 : ℝ) = 2 * 2), log_mul two_ne_zero two_ne_zero]
    ring

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

Goal state before:
pp: case hint
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun y ↦ ↑y * (1 + ↑y ^ 2) ^ t

Tactic:
refine continuous_ofReal.mul ?_

Goal state after:
case hint
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun y ↦ (1 + ↑y ^ 2) ^ t
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case e'_2
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ↑(∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t) = ∫ (x : ℝ) in ?convert_1..?convert_2, ↑x * (1 + ↑x ^ 2) ^ ↑t

Tactic:
rw [← intervalIntegral.integral_ofReal]
    congr with x : 1
    rw [ofReal_mul, this x t]

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfd : DiffContOnCl ℂ f {z | 0 < z.re}
hgd : DiffContOnCl ℂ g {z | 0 < z.re}
hfexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hgexp : ∃ c < 2, ∃ B, g =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x - g ↑x‖
Cf : ℝ
hCf : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ Cf
Cg : ℝ
hCg : ∀ (x : ℝ), ‖g (↑x * I)‖ ≤ Cg
⊢ ∃ C, ∀ (x : ℝ), ‖(f - g) (↑x * I)‖ ≤ C

Tactic:
exact ⟨Cf + Cg, fun x => norm_sub_le_of_le (hCf x) (hCg x)⟩

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfd : DiffContOnCl ℂ f {z | 0 < z.re}
hgd : DiffContOnCl ℂ g {z | 0 < z.re}
hfexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hgexp : ∃ c < 2, ∃ B, g =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x - g ↑x‖
hfim : ∃ C, ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hgim : ∃ C, ∀ (x : ℝ), ‖g (↑x * I)‖ ≤ C
⊢ EqOn f g {z | 0 ≤ z.re}

Tactic:
by
  suffices EqOn (f - g) 0 {z : ℂ | 0 ≤ z.re} by
    simpa only [EqOn, Pi.sub_apply, Pi.zero_apply, sub_eq_zero] using this
  refine eq_zero_on_right_half_plane_of_superexponential_decay (hfd.sub hgd) ?_ hre ?_
  · exact isBigO_sub_exp_rpow hfexp hgexp
  · rcases hfim with ⟨Cf, hCf⟩; rcases hgim with ⟨Cg, hCg⟩
    exact ⟨Cf + Cg, fun x => norm_sub_le_of_le (hCf x) (hCg x)⟩

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

Goal state before:
pp: case h
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := ⋯
hr : 0 < r
h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
h6 : DiffContOnCl ℂ f (ball z₀ r)
h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀
h8 : (sphere z₀ r).Nonempty
h9 : ContinuousOn (fun x ↦ ‖f x - f z₀‖) (sphere z₀ r)
x : ℂ
hx : x ∈ sphere z₀ r
hfx : IsMinOn (fun x ↦ ‖f x - f z₀‖) (sphere z₀ r) x
⊢ r ≤ R

Tactic:
exact inf_le_right

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

Goal state before:
pp: h : ℝ
z : ℂ
⊢ 𝕢 h z ≠ 0

Tactic:
simp [qParam, exp_ne_zero]

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

Goal state before:
pp: case hws
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ 0 < ∑ i ∈ P.roots.toFinset, P.derivRootWeight z i

Tactic:
apply sum_derivRootWeight_pos h₀

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

Goal state before:
pp: f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ 0 ≤ f z

Tactic:
refine hf.differentiableOn.nonneg_of_iteratedDeriv_nonneg (r := (z - c).re + 1) h hz ?_

Goal state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ z ∈ Metric.ball c ((z - c).re + 1)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
⊢ circleAverage (∑ᶠ (u : ℂ), fun x ↦ ↑(D u) * log ‖x - u‖) c R =
    circleAverage (∑ u ∈ h.toFinset, fun x ↦ ↑(D u) * log ‖x - u‖) c R

Tactic:
finsum_eq_sum_of_support_subset

Goal state after:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
⊢ circleAverage (∑ i ∈ ?s, fun x ↦ ↑(D i) * log ‖x - i‖) c R =
    circleAverage (∑ u ∈ h.toFinset, fun x ↦ ↑(D u) * log ‖x - u‖) c R

case s
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
⊢ Finset ℂ

case h
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
⊢ (Function.support fun u x ↦ ↑(D u) * log ‖x - u‖) ⊆ ↑?s
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
⊢ ∑ u ∈ h.toFinset, ↑(D u) * log R = ∑ᶠ (u : ℂ), ↑(D u) * log R

Tactic:
finsum_eq_sum_of_support_subset

Goal state after:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
⊢ ∑ u ∈ h.toFinset, ↑(D u) * log R = ∑ i ∈ ?s, ↑(D i) * log R

case s
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
⊢ Finset ℂ

case h
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
⊢ (Function.support fun u ↦ ↑(D u) * log R) ⊆ ↑?s
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: z : ℂ
hz : z ≠ 0
⊢ z.sqrt = cexp (log z / 2)

Tactic:
by
  simp [sqrt, cpow_def, hz, div_eq_mul_inv]

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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
x✝ : SpecialLinearGroup n R
⊢ x✝ ∈ toPGL.ker ↔ x✝ ∈ Subgroup.center (SpecialLinearGroup n R)

Tactic:
simp [toGL_mem_center_iff]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z w : ℍ
⊢ g • z = w ↔ num g ↑z = (σ g) ↑w * denom g ↑z

Tactic:
rw [← (σ g).injective.eq_iff]
  simp [UpperHalfPlane.ext_iff, coe_smul, div_eq_iff]

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

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℂ
hz : z.im ≠ 0
⊢ denom (g * h) z = denom g (num h z / denom h z) * denom h z

Tactic:
change _ = (_ * (_ / _) + _) * _
  field_simp [denom_ne_zero_of_im h hz]
  simp only [denom, Units.val_mul, mul_apply, Fin.sum_univ_succ, Finset.univ_unique,
    Fin.default_eq_zero, Finset.sum_singleton, Fin.succ_zero_eq_one, Complex.ofReal_add,
    Complex.ofReal_mul, num]
  ring

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

Goal state before:
pp: K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
⊢ g.IsParabolic ↔ (∃ x, x ≠ 0 ∧ g = upperRightHom x) ∨ ∃ x, x ≠ 0 ∧ g = -upperRightHom x

Tactic:
isParabolic_iff_of_upperTriangular hg10

Goal state after:
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
⊢ ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 ≠ 0 ↔ (∃ x, x ≠ 0 ∧ g = upperRightHom x) ∨ ∃ x, x ≠ 0 ∧ g = -upperRightHom x
Module: Mathlib.Topology.TietzeExtension

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

Tactic:
rcases ha.exists_between hay with ⟨_, ⟨x, rfl⟩, _, hxy⟩

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

Goal state before:
pp: case inr.inr.inl.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hyb : (g - dg) y < b
xu : X
hyxu : (g - dg) y < f xu
right✝ : f xu ≤ b
hc : c < g y
h✝ : a ∉ range ⇑f
hay : a < (g - dg) y
⊢ ∃ x₁ x₂, (g - dg) y ∈ Icc (f x₁) (f x₂)

Tactic:
rcases ha.exists_between hay with ⟨_, ⟨x, rfl⟩, _, hxy⟩

Goal state after:
case inr.inr.inl.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hyb : (g - dg) y < b
xu : X
hyxu : (g - dg) y < f xu
right✝ : f xu ≤ b
hc : c < g y
h✝ : a ∉ range ⇑f
hay : a < (g - dg) y
x : X
left✝ : a ≤ f x
hxy : f x < (g - dg) y
⊢ ∃ x₁ x₂, (g - dg) y ∈ Icc (f x₁) (f x₂)