mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
⊢ HasDerivWithinAt f (sInf (slope f x '' {y | y ∈ S ∧ x < y})) (Ioi x) x

Tactic:
have hxs' := hxs
  rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hxs'
  obtain ⟨a, b, hxab, habs⟩ := hxs'
  simp_rw [hasDerivWithinAt_iff_tendsto_slope]
  simp only [mem_Ioi, lt_self_iff_false, not_false_eq_true, sdiff_singleton_eq_self]
  have h : Ioo x b ⊆ {y | y ∈ S ∧ x < y} := fun z hz ↦ ⟨habs ⟨hxab.1.trans hz.1, hz.2⟩, hz.1⟩
  have h_Ioo : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' Ioo x b))) :=
    ((monotoneOn_slope_gt hfc (habs hxab)).mono h).tendsto_nhdsWithin_Ioo_right
      (by simpa using hxab.2) ((bddBelow_slope_lt_of_mem_interior hfc hxs).mono (image_mono h))
  suffices sInf (slope f x '' Ioo x b) = sInf (slope f x '' {y ∈ S | x < y}) by rwa [← this]
  apply (monotoneOn_slope_gt hfc (habs hxab)).csInf_eq_of_subset_of_forall_exists_le
    (bddBelow_slope_lt_of_mem_interior hfc hxs) h ?_
  rintro y ⟨hyS, hxy⟩
  obtain ⟨z, hxz, hzy⟩ := exists_between (lt_min hxab.2 hxy)
  exact ⟨z, ⟨hxz, hzy.trans_le (min_le_left _ _)⟩, hzy.le.trans (min_le_right _ _)⟩

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

Goal state before:
pp: x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y))

Tactic:
rw [← arctan_tan (x := _ + _)]
  · congr
    conv_rhs => rw [← tan_arctan x, ← tan_arctan y]
    exact tan_add' ⟨arctan_ne_mul_pi_div_two, arctan_ne_mul_pi_div_two⟩
  · rw [neg_lt, neg_add, ← arctan_neg, ← arctan_neg]
    rw [← neg_mul_neg] at h
    exact arctan_add_arctan_lt_pi_div_two h
  · exact arctan_add_arctan_lt_pi_div_two h

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case refine_2.refine_1
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hzs : z ∈ S
hzx : z < x
⊢ (slope f x '' {y | y ∈ S ∧ x < y}).Nonempty

Tactic:
rw [image_nonempty]
    obtain ⟨z, hxz, hzb⟩ := exists_between hxab.2
    exact ⟨z, habs ⟨hxab.1.trans hxz, hzb⟩, hxz⟩

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ derivWithin f S x < derivWithin f S y

Tactic:
exact (hfc.derivWithin_lt_slope hx hy hxy (hfd x hx)).trans
    (hfc.slope_lt_derivWithin hx hy hxy (hfd y hy))

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

Goal state before:

Tactic:
‖f z‖ ≤ ‖f z - f 0‖ + ‖f 0‖ := norm_le_norm_sub_add _ _
    _ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖) + ‖f 0‖ := by gcongr
    _ = 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖) := by field_simp; ring

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ ∀ᶠ (x : 𝕜) in 𝓝ˢ U, f =ᶠ[𝓝[≠] x] g

Tactic:
eventually_nhdsSet_iff_exists

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ ∃ t, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ U ⊆ t ∧ ∀ x ∈ t, f =ᶠ[𝓝[≠] x] g
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
⊢ meromorphicOrderAt ((fun x_1 ↦ x_1 - x) ^ n) x = ↑n

Tactic:
convert! meromorphicOrderAt_zpow_id_sub_const

Goal state after:
case e'_2.e'_6
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
⊢ (fun x_1 ↦ x_1 - x) ^ n = (fun x_1 ↦ x_1 - x) ^ ↑n
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case mp
g : ℂ →L[ℝ] ℂ
⊢ IsConformalMap g → ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = g ∘SL ↑conjCLE) ∧ g ≠ 0

pp: case mpr
g : ℂ →L[ℝ] ℂ
⊢ ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = g ∘SL ↑conjCLE) ∧ g ≠ 0 → IsConformalMap g

Tactic:
· exact fun h => ⟨h.is_complex_or_conj_linear, h.ne_zero⟩

Goal state after:
case mpr
g : ℂ →L[ℝ] ℂ
⊢ ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = g ∘SL ↑conjCLE) ∧ g ≠ 0 → IsConformalMap g
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
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
⊢ ((∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
        ∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) •
      meromorphicTrailingCoeffAt f w =
    ((∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
        ∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) •
      meromorphicTrailingCoeffAt
        (((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f B₀R) u)) * ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor f S₀R) v) •
          h)
        w

Tactic:
meromorphicTrailingCoeffAt_congr_nhdsNE
        ((D.meromorphicOn w hw).eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin_preperfect
        (by fun_prop) hw ?η₁ D.eventuallyEq)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
⊢ ((∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
        ∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) •
      meromorphicTrailingCoeffAt
        (((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) *
            ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor f (sphere 0 R)) v) •
          h)
        w =
    ((∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
        ∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) •
      meromorphicTrailingCoeffAt
        (((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f B₀R) u)) * ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor f S₀R) v) •
          h)
        w

case η₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
⊢ Preperfect (closedBall 0 R)
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
hn : ↑n ≠ 0
hmero : MeromorphicAt f x
g : 𝕜 → E
hga : AnalyticAt 𝕜 g x
hg0 : g x ≠ 0
hg : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z
z : 𝕜
hgz : AnalyticAt 𝕜 g z
hmem : z ∈ {x}ᶜ
hz : deriv f z = deriv (fun z ↦ (z - x) ^ n • g z) z
⊢ deriv f z = (z - x) ^ (n - 1) • (↑n • g z + (z - x) • deriv g z)

Tactic:
have hzx : z - x ≠ 0 := by simpa [sub_eq_zero] using hmem

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
hn : ↑n ≠ 0
hmero : MeromorphicAt f x
g : 𝕜 → E
hga : AnalyticAt 𝕜 g x
hg0 : g x ≠ 0
hg : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z
z : 𝕜
hgz : AnalyticAt 𝕜 g z
hmem : z ∈ {x}ᶜ
hz : deriv f z = deriv (fun z ↦ (z - x) ^ n • g z) z
hzx : z - x ≠ 0
⊢ deriv f z = (z - x) ^ (n - 1) • (↑n • g z + (z - x) • deriv g z)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ re ⁻¹' {0, 1}
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1

Tactic:
rcases hz with hz0 | hz1

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz0 : z.re = 0
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz1 : z.re ∈ {1}
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
this :
  ∀ x ∈ Ioi 0,
    (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
      ‖↑(x + sSupNormIm f 0) ^ (1 - z) * ↑(x + sSupNormIm f 1) ^ z‖
⊢ Tendsto (fun x ↦ (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0) (𝓝 (sSupNormIm f 1 ^ z.re))

Tactic:
· apply Tendsto.rpow_const
          · nth_rw 2 [← zero_add (sSupNormIm f 1)]
            exact Tendsto.add_const (sSupNormIm f 1) (tendsto_nhdsWithin_of_tendsto_nhds
              (Continuous.tendsto continuous_id' _))
          · right; simp only [le_of_lt hz.1]

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

Goal state before:
pp: l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ z.re * (u - l) < u - l

Tactic:
nth_rewrite 2 [← one_mul (u - l)]

Goal state after:
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ z.re * (u - l) < 1 * (u - l)
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
⊢ ⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x

Tactic:
· rw [setAverage_eq, uIoc_of_ge h.le, Real.volume_real_Ioc_of_le h.le, integral_of_ge h.le,
      smul_neg, ← neg_smul, ← inv_neg, neg_sub]

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

Goal state before:
pp: case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
inst✝ : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
⊢ ∀ z ∈ univ, HasDerivAt (fun x ↦ wedgeIntegral 0 x f) (f z) z

Tactic:
intro z _

Goal state after:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
inst✝ : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
z : ℂ
a✝ : z ∈ univ
⊢ HasDerivAt (fun x ↦ wedgeIntegral 0 x f) (f z) z
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
⊢ circleAverage (poissonKernel c w • f) c R = f w

Tactic:
by
  rw [← hf.circleAverage_re_herglotzRieszKernel_smul hw]
  apply circleAverage_congr_sphere
    (fun _ _ ↦ by simp_rw [← poissonKernel_eq_re_herglotzRieszKernel])

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ circleAverage (poissonKernel c w • f) c R = f w

Tactic:
by
  rw [← hf.circleAverage_re_herglotzRieszKernel_smul hw]
  apply circleAverage_congr_sphere
    (fun _ _ ↦ by simp_rw [← poissonKernel_eq_re_herglotzRieszKernel])

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

Goal state before:
pp: case pos
x : ℝ
hx : x = 0
⊢ deriv (deriv fun x ↦ x * log x) x = x⁻¹

pp: case neg
x : ℝ
hx : ¬x = 0
⊢ deriv (deriv fun x ↦ x * log x) x = x⁻¹

Tactic:
· rw [hx, inv_zero]
    exact deriv_zero_of_not_differentiableAt
      (fun h ↦ not_continuousAt_deriv_mul_log_zero h.continuousAt)

Goal state after:
case neg
x : ℝ
hx : ¬x = 0
⊢ deriv (deriv fun x ↦ x * log x) x = x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: case mpr
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ negMulLog x

Tactic:
have : x ∈ ({0} : Set ℝ)ᶜ := by
      simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true]

Goal state after:
case mpr
x : ℝ
hx : x ≠ 0
this : x ∈ {0}ᶜ
⊢ DifferentiableAt ℝ negMulLog x
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: H : ContinuousAt (fun x ↦ (log x)⁻¹) (-1)
⊢ ContinuousAt (fun x ↦ (log x)⁻¹) 1

Tactic:
simpa only [log_neg_eq_log] using H.comp' continuousAt_neg

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

Goal state before:
pp: H : ContinuousAt (fun x ↦ log (log x)) (-1)
⊢ ContinuousAt (fun x ↦ log (log x)) 1

Tactic:
simpa only [log_neg_eq_log] using H.comp' continuousAt_neg

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

Goal state before:
pp: case refine_2
s : ℂ
t : ℝ
ht : 0 < t
h : -1 < s.re
⊢ IntervalIntegrable (fun x ↦ ↑x ^ s) volume 0 t

Tactic:
exact intervalIntegrable_cpow' h (a := 0) (b := t)

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

Goal state before:
pp: x : ℝ
n : ℕ
⊢ log⁺ (↑n * x) ≤ log ↑n + log⁺ x

Tactic:
rw [← log_of_nat_eq_posLog]

Goal state after:
x : ℝ
n : ℕ
⊢ log⁺ (↑n * x) ≤ log⁺ ↑n + log⁺ x
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

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

Tactic:
rw [← intervalIntegral.integral_add_adjacent_intervals (a := 0) (b := π / 2) (c := π)
    (by apply intervalIntegrable_log_sin) (by apply intervalIntegrable_log_sin)]

Goal state after:
⊢ (∫ (x : ℝ) in 0..π / 2, log (sin x)) + ∫ (x : ℝ) in π / 2..π, log (sin x) = 2 * ∫ (x : ℝ) in 0..π / 2, log (sin x)
Module: Mathlib.Analysis.Complex.RiemannMapping

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

Tactic:
refine ⟨?mapsTo, ?injOn, ?deriv⟩

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

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

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

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * log R + log ‖g c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * log R +
      (log ‖meromorphicTrailingCoeffAt f c‖ - ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * log ‖c - u‖)

Tactic:
have t₀ : c ∈ CB := by simp [CB]
      have t₁ : AccPt c (𝓟 CB) := by
        apply accPt_iff_frequently_nhdsNE.mpr
        apply compl_notMem
        apply mem_nhdsWithin.mpr
        use ball c |R|
        simpa [hR] using! fun _ ⟨h, _⟩ ↦ ball_subset_closedBall h
      simp [MeromorphicOn.log_norm_meromorphicTrailingCoeffAt_extract_zeros_poles h₃f t₀ t₁
        (h₁f c t₀) (h₁g c t₀) (h₂g ⟨c, t₀⟩) h₃g]

Goal state after:
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
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, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Tactic:
rcases exists_bounded_mem_Icc_of_closed_of_le hc₁ hc₂ hd hf3.le with ⟨g, hg₁, hg₂, hgf⟩

Goal state after:
case 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)
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: ⊢ FaithfulSMul PGL(2, ℝ) ℍ

Tactic:
faithfulSMul_iff

Goal state after:
⊢ ∀ (g : PGL(2, ℝ)), (∀ (a : ℍ), g • a = a) → g = 1
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mp.f
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
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
hg11 : ↑g 1 1 = 1
⊢ ∃ x, x ≠ 0 ∧ g = upperRightHom x

Tactic:
simp only [Units.ext_iff]

Goal state after:
case mp.f
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
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
hg11 : ↑g 1 1 = 1
⊢ ∃ x, x ≠ 0 ∧ ↑g = ↑(upperRightHom x)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mp.g
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
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
hg11 : ↑g 1 1 = -1
⊢ ∃ x, x ≠ 0 ∧ g = -upperRightHom x

Tactic:
simp only [Units.ext_iff]

Goal state after:
case mp.g
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
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
hg11 : ↑g 1 1 = -1
⊢ ∃ x, x ≠ 0 ∧ ↑g = ↑(-upperRightHom x)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ dist ↑z ↑(w.center r) ^ 2 = 2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2

Tactic:
have H : 2 * z.im * w.im ≠ 0 := by positivity

Goal state after:
z w : ℍ
r : ℝ
H : 2 * z.im * w.im ≠ 0
⊢ dist ↑z ↑(w.center r) ^ 2 = 2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n) sinh = sinh

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add]

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n) cosh = cosh

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add]

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

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ ProperSpace ℍ

Tactic:
refine ⟨fun z r => ?_⟩
  rw [isEmbedding_coe.isCompact_iff (f := ((↑) : ℍ → ℂ)), image_coe_closedBall]
  apply isCompact_closedBall

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
⊢ induced pure Ultrafilter.topologicalSpace = ⊥

Tactic:
by
  apply eq_bot_of_singletons_open
  intro x
  use { u : Ultrafilter α | {x} ∈ u }, ultrafilter_isOpen_basic _
  simp

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

Goal state before:
pp: z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
h₂ : ‖↑y₁ * ↑y₂‖ ≠ 0
⊢ 2 *
      arsinh
        (dist ↑y₁ ↑y₂ / (‖↑y₁‖ * ‖↑y₂‖) /
          (2 * √({ coe := -(↑y₁)⁻¹, coe_im_pos := ⋯ }.im * { coe := -(↑y₂)⁻¹, coe_im_pos := ⋯ }.im))) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))

Tactic:
mk_im,

Goal state after:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
h₂ : ‖↑y₁ * ↑y₂‖ ≠ 0
⊢ 2 * arsinh (dist ↑y₁ ↑y₂ / (‖↑y₁‖ * ‖↑y₂‖) / (2 * √((-(↑y₁)⁻¹).im * (-(↑y₂)⁻¹).im))) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
F G : Ultrafilter α
x : α
hF : map g ↑F ≤ 𝓝 (g x)
hG : map g ↑G ≤ 𝓝 (g x)
⊢ Ultrafilter.extend g G = g x

Tactic:
rwa [ultrafilter_extend_eq_iff, G.coe_map]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁ * f₂) ⊤ = circleAverage (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0

Tactic:
by
      simp [proximity]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
h_bound_nonneg : 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
⊢ ∀ (x : ℝ), (fun α ↦ (cartanKernel f R α β)⁺) x ≤ (fun x ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) x

Tactic:
intro α

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
h_bound_nonneg : 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
α : ℝ
⊢ (fun α ↦ (cartanKernel f R α β)⁺) α ≤ (fun x ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) α