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

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

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

Tactic:
· norm_cast
        grind [Complex.div_re, Complex.normSq_ofReal, sub_re, ofReal_re, ofReal_im, mul_eq_zero]

Goal state after:
case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ f (↑l + (z - ↑l) / (↑u - ↑l) * (↑u - ↑l)) = e
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: 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 : ℝ
hd : d < π / 2 / b
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
A : ℝ
hA₀ : A > 0
hA :
  ∀ᶠ (b_1 : ℝ) in atTop,
    ∀ (a_1 : ℂ), |a_1.re| = b_1 → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
this : Tendsto (fun R ↦ expR (δ * expR (d * R) + B * expR (c * R) + Real.log A)) atTop (𝓝 0)
R : ℝ
hR : expR (δ * expR (d * R) + B * expR (c * R) + Real.log A) ≤ C
Hle : ∀ (a_1 : ℂ), |a_1.re| = R → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
⊢ ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C

Tactic:
w

Goal state after:
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 : ℝ
hd : d < π / 2 / b
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
A : ℝ
hA₀ : A > 0
hA :
  ∀ᶠ (b_1 : ℝ) in atTop,
    ∀ (a_1 : ℂ), |a_1.re| = b_1 → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
this : Tendsto (fun R ↦ expR (δ * expR (d * R) + B * expR (c * R) + Real.log A)) atTop (𝓝 0)
R : ℝ
hR : expR (δ * expR (d * R) + B * expR (c * R) + Real.log A) ≤ C
Hle : ∀ (a_1 : ℂ), |a_1.re| = R → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
w : ℂ
⊢ |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C
Module: Mathlib.Analysis.Complex.Harmonic.Liouville

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
z : ℂ
⊢ ∀ (w : ℂ), f z = f w

Tactic:
w

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
z w : ℂ
⊢ f z = f w
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:
continuousOn_iff_continuous_domRestrict

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] (s.domRestrict (Real.circleAverage f c))
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: case h₁f.hf
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ ContinuousOn (re ∘ herglotzRieszKernel c w • f) {z | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}

Tactic:
herglotzRieszKernel_fun_def

Goal state after:
case h₁f.hf
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ ContinuousOn ((re ∘ fun z ↦ (z - c + (w - c)) / (z - c - (w - c))) • f) {z | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
x : ℂ
h : ContDiffAt ℂ 2 f x
⊢ HarmonicAt f x

Tactic:
refine ⟨h.restrict_scalars ℝ, ?_⟩
  filter_upwards [h.restrictScalars_iteratedFDeriv_eventuallyEq (𝕜 := ℝ)] with a ha
  have : (iteratedFDeriv ℂ 2 f a) (I • ![1, 1])
      = (∏ i, I) • ((iteratedFDeriv ℂ 2 f a) ![1, 1]) :=
    (iteratedFDeriv ℂ 2 f a).map_smul_univ (fun _ ↦ I) ![1, 1]
  simp_all [laplacian_eq_iteratedFDeriv_complexPlane f, ← ha,
    ContinuousMultilinearMap.coe_restrictScalars]

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

Goal state before:
pp: x : ℝ
⊢ sin x / x ≤ |x|⁻¹

Tactic:
by
  rcases lt_trichotomy x 0 with hx | rfl | hx
  · rw [abs_of_nonpos hx.le, ← one_div, le_div_iff₀, div_eq_mul_inv]
    · ring_nf
      rw [mul_assoc, mul_inv_cancel₀ hx.ne, mul_one, neg_le]
      exact neg_one_le_sin x
    · simpa using hx
  · simp
  · rw [abs_of_nonneg hx.le, div_eq_mul_inv, mul_inv_le_iff₀ hx, inv_mul_cancel₀ hx.ne']
    exact sin_le_one x

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
hg : CircleIntegrable f 0 R
hw : w ∈ ball 0 R
hR : 0 < R
d : ℝ
hd : d > 0
hsub : ball w d ⊆ ball 0 R
hdist : ∀ x ∈ ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap 0 R θ - x‖
hgm : AEStronglyMeasurable (fun θ ↦ f (circleMap 0 R θ)) (volume.restrict (uIoc 0 (2 * π)))
h₁ : CircleIntegrable (herglotzRieszKernel 0 w • f) 0 R
⊢ IntervalIntegrable (fun θ ↦ herglotzRieszKernel 0 w (circleMap 0 R θ) • f (circleMap 0 R θ)) volume 0 (2 * π)

Tactic:
simpa only [CircleIntegrable, Pi.smul_apply'] using h₁

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
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‖
⊢ Tendsto (fun x ↦ cexp ↑(ε * x) • f ↑x) atTop (𝓝 0)

Tactic:
← ofReal_exp,

Goal state after:
case refine_2
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‖
⊢ Tendsto (fun x ↦ ↑(expR (ε * x)) • f ↑x) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case neg
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
⊢ |R|⁻¹ * ‖c - a‖ ≤ 1

Tactic:
rw [mem_closedBall, dist_eq_norm'] at hu

Goal state after:
case neg
a c : ℂ
R : ℝ
hu : ‖c - a‖ ≤ |R|
hR : ¬R = 0
⊢ |R|⁻¹ * ‖c - a‖ ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: n : ℕ
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * n + 1) = 2 * ∏ i ∈ Finset.range n, (2 * ↑i + 2) / (2 * ↑i + 3)

Tactic:
induction n with
  | zero => norm_num
  | succ k ih =>
    rw [prod_range_succ_comm, mul_left_comm, ← ih, mul_succ, integral_sin_pow]
    norm_cast
    field_simp
    simp

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_bd : I∞.BoundedAtFilter f
⊢ (𝓝[≠] 0).BoundedAtFilter (cuspFunction h f)

Tactic:
refine (h_bd.comp_tendsto <| invQParam_tendsto hh).congr' ?_ (by simp)

Goal state after:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_bd : I∞.BoundedAtFilter f
⊢ f ∘ invQParam h =ᶠ[𝓝[≠] 0] cuspFunction h f
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).re = c₀
h₁U : IsOpen U
h₂U : IsConnected U
⊢ ∃ c, ∀ x ∈ U, f x = ↑c₀ + ↑c * I

Tactic:
by
  obtain ⟨cc, hcc⟩ := eq_const_of_re_eq_const h₁f h₂f h₁U h₂U
  use cc.im
  simp_rw [Complex.ext_iff]
  aesop

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

Goal state before:
pp: 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 : ℂ
hz : z ∈ U
⊢ ∀ ⦃x₂ : ℂ⦄, x₂ ∈ U → (fun z ↦ ↑ε / (f z - x)) z = (fun z ↦ ↑ε / (f z - x)) x₂ → z = x₂

Tactic:
w

Goal state after:
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 : ℂ
hz : z ∈ U
w : ℂ
⊢ w ∈ U → (fun z ↦ ↑ε / (f z - x)) z = (fun z ↦ ↑ε / (f z - x)) w → z = w
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Exp

Goal state before:
pp: ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
⊢ π ≤ π * (2 * ξ.im)

Tactic:
le_mul_iff_one_le_right Real.pi_pos,

Goal state after:
ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
⊢ 1 ≤ 2 * ξ.im
Module: Mathlib.Analysis.Complex.Tietze

Goal state before:
pp: 𝕜 : 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
x : E
hx : x ∈ frontier (Metric.closedBall 0 1)
⊢ ‖x‖ = 1

Tactic:
simpa [frontier_closedBall (0 : E) one_ne_zero] using hx

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

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ num (g * h) u * (↑(↑g 1 0) * (num h u / denom h u) + ↑(↑g 1 1)) = num g (num h u / denom h u) * denom (g * h) u

Tactic:
mul_div,

Goal state after:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ num (g * h) u * (↑(↑g 1 0) * num h u / denom h u + ↑(↑g 1 1)) = num g (num h u / denom h u) * denom (g * h) u
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ num (g * h) u * (↑(↑g 1 0) * num h u + ↑(↑g 1 1) * denom h u) / denom h u =
    (↑(↑g 0 0) * (num h u / denom h u) + ↑(↑g 0 1)) * denom (g * h) u

Tactic:
mul_div,

Goal state after:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ num (g * h) u * (↑(↑g 1 0) * num h u + ↑(↑g 1 1) * denom h u) / denom h u =
    (↑(↑g 0 0) * num h u / denom h u + ↑(↑g 0 1)) * denom (g * h) u
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: ⊢ ContinuousOn (fun t ↦ ↑ofComplex (↑I * ↑t)) (Ioi 0)

Tactic:
simp only [ofComplex_apply_eq_ite, continuousOn_iff_continuous_domRestrict,
    continuous_induced_rng]

Goal state after:
⊢ Continuous
    (UpperHalfPlane.coe ∘
      (Ioi 0).domRestrict fun t ↦
        if hw : 0 < (↑I * ↑t).im then { coe := ↑I * ↑t, coe_im_pos := hw } else Classical.choice ⋯)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: z : ℍ
⊢ ModularGroup.S • z = { coe := (-↑z)⁻¹, coe_im_pos := ⋯ }

Tactic:
rw [specialLinearGroup_apply]

Goal state after:
z : ℍ
⊢ {
      coe :=
        (↑((algebraMap ℤ ℝ) (↑ModularGroup.S 0 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑ModularGroup.S 0 1))) /
          (↑((algebraMap ℤ ℝ) (↑ModularGroup.S 1 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑ModularGroup.S 1 1))),
      coe_im_pos := ⋯ } =
    { coe := (-↑z)⁻¹, coe_im_pos := ⋯ }
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
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 : Y), ∃ x, g y ∈ Icc (f x) b) ∧ ⇑g ∘ e = ⇑f

Tactic:
rcases exists_extension_forall_mem_Icc_of_isClosedEmbedding f hmem hle he with ⟨g, hg_mem, hgf⟩
    -- If `a ∈ range f`, then we are done.
    rcases em (∃ x, f x = a) with (⟨x, rfl⟩ | ha')
    · exact ⟨g, fun y => ⟨x, hg_mem _⟩, hgf⟩
    /- Otherwise, `g ⁻¹' {a}` is disjoint with `range e ∪ g ⁻¹' (Ici c)`, hence there exists a
        function `dg : Y → ℝ` such that `dg ∘ e = 0`, `dg y = 0` whenever `c ≤ g y`, `dg y = c - a`
        whenever `g y = a`, and `0 ≤ dg y ≤ c - a` for all `y`. -/
    have hd : Disjoint (range e ∪ g ⁻¹' Ici c) (g ⁻¹' {a}) := by
      refine disjoint_union_left.2 ⟨?_, Disjoint.preimage _ ?_⟩
      · rw [Set.disjoint_left]
        rintro _ ⟨x, rfl⟩ (rfl : g (e x) = a)
        exact ha' ⟨x, (congr_fun hgf x).symm⟩
      · exact Set.disjoint_singleton_right.2 hac.not_ge
    rcases exists_bounded_mem_Icc_of_closed_of_le
        (he.isClosed_range.union <| isClosed_Ici.preimage g.continuous)
        (isClosed_singleton.preimage g.continuous) hd (sub_nonneg.2 hac.le) with
      ⟨dg, dg0, dga, dgmem⟩
    replace hgf : ∀ x, (g + dg) (e x) = f x := by
      intro x
      simp [dg0 (Or.inl <| mem_range_self _), ← hgf]
    refine ⟨g + dg, fun y => ?_, funext hgf⟩
    have hay : a < (g + dg) y := by
      rcases (hg_mem y).1.eq_or_lt with (rfl | hlt)
      · refine (lt_add_iff_pos_right _).2 ?_
        calc
          0 < c - g y := sub_pos.2 hac
          _ = dg y := (dga rfl).symm
      · exact hlt.trans_le (le_add_of_nonneg_right (dgmem y).1)
    rcases ha.exists_between hay with ⟨_, ⟨x, rfl⟩, _, hxy⟩
    refine ⟨x, hxy.le, ?_⟩
    rcases le_total c (g y) with hc | hc
    · simp [dg0 (Or.inr hc), (hg_mem y).2]
    · calc
        g y + dg y ≤ c + (c - a) := add_le_add hc (dgmem _).2
        _ = b := by rw [hsub, add_sub_cancel]

Goal state after:
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
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
b : ℝ
hb : IsLUB (range ⇑f) b
g : Y →ᵇ ℝ
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
dg : Y →ᵇ ℝ
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
x : X
ha : IsGLB (range ⇑f) (f x)
hmem : ∀ (x_1 : X), f x_1 ∈ Icc (f x) b
hle : f x ≤ b
hlt : f x < b
c : ℝ := (f x + b) / 2
hac : f x < c
hcb : c < b
hsub : c - f x = b - c
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
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)
hc : c < g y
⊢ f x = c - (b - c)

Tactic:
by rw [← hsub, sub_sub_cancel]

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.inr.inl.inl
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
b : ℝ
hb : IsLUB (range ⇑f) b
g : Y →ᵇ ℝ
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
dg : Y →ᵇ ℝ
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
x : X
ha : IsGLB (range ⇑f) (f x)
hmem : ∀ (x_1 : X), f x_1 ∈ Icc (f x) b
hle : f x ≤ b
hlt : f x < b
c : ℝ := (f x + b) / 2
hac : f x < c
hcb : c < b
hsub : c - f x = b - c
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
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)
hc : c < g y
⊢ f x ≤ (g - dg) y

Tactic:
calc
        f x = c - (b - c) := by rw [← hsub, sub_sub_cancel]
        _ ≤ g y - dg y := sub_le_sub hc.le (dgmem _).2

Goal state after:
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
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
⊢ a = c - (b - c)

Tactic:
by rw [← hsub, sub_sub_cancel]

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

Goal state before:
pp: ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
h0 : ∏ i ∈ s, f i = 0
this : ∃ i ∈ s, ∃ᶠ (x : ℍ) in 𝓝[≠] I, f i x = 0
⊢ ∃ i ∈ s, f i = 0

Tactic:
exact this.imp fun i hi ↦ ⟨hi.1, eq_zero_of_frequently (hf i hi.1) hi.2⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ tanh (arsinh x) = x / √(1 + x ^ 2)

Tactic:
rw [tanh_eq_sinh_div_cosh, sinh_arsinh, cosh_arsinh]

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

Goal state before:
pp: α : Type u
s : Set α
⊢ IsClosed {u | s ∈ u}

Tactic:
by
  rw [← isOpen_compl_iff]
  convert! ultrafilter_isOpen_basic sᶜ using 1
  ext u
  exact Ultrafilter.compl_mem_iff_notMem.symm

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

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ ↑(Ultrafilter.map f b) ≤ 𝓟 univ

Tactic:
rw [le_principal_iff]

Goal state after:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ univ ∈ ↑(Ultrafilter.map f b)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
⊢ IsOpen[instTopologicalSpace] s ↔ IsClosed[inst✝] (some ⁻¹' s)ᶜ ∧ IsCompact (some ⁻¹' s)ᶜ

Tactic:
simp only [isOpen_iff_of_mem' h, isClosed_compl_iff, and_comm]

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous[t, _] f
this : Continuous[t, compactlyGenerated X] id
⊢ t ≤ compactlyGenerated X

Tactic:
by
      rwa [← continuous_id_iff_le]

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous[t, _] f
⊢ ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous[_, compactlyGenerated X] (id ∘ ⇑g)

Tactic:
intro S g

Goal state after:
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous[t, _] f
S : CompHaus
g : C(↑S.toTop, X)
⊢ Continuous[_, compactlyGenerated X] (id ∘ ⇑g)
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
⊢ (fun R ↦ circleAverage (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R) 0 1) R + logCounting f ⊤ R =
    circleAverage (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R + logCounting f ⊤ R) 0 1

Tactic:
circleAverage_fun_add (circleIntegrable_circleAverage_log_norm_sub h)
          (circleIntegrable_const (logCounting f ⊤ R) 0 1),

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
⊢ (fun R ↦ circleAverage (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R) 0 1) R + logCounting f ⊤ R =
    circleAverage (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R) 0 1 +
      circleAverage (fun x ↦ logCounting f ⊤ R) 0 1
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
⊢ ∃ b_1, b ≤ b_1 ∧ 1 < a * |logCounting D b_1|

Tactic:
let ℓ := 1 + max ‖e‖ (max |b| |c|)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
⊢ ∃ b_1, b ≤ b_1 ∧ 1 < a * |logCounting D b_1|
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case h₁.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
a✝ : a ≤ b
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹)) ⊆ ↑hs.toFinset

Tactic:
intro z
      simp only [support_mul, mem_inter_iff, mem_support, ne_eq, Int.cast_eq_zero, log_eq_zero,
        mul_eq_zero, inv_eq_zero, norm_eq_zero, not_or, Finite.coe_toFinset, and_imp, s]
      intro h₁ _ _ _ _
      have : z ∈ closedBall 0 |a| := mem_of_indicator_ne_zero h₁
      rw [toClosedBall_eval_within _ this] at h₁
      rwa [toClosedBall_eval_within]
      · simp_all only [abs_of_pos ha, mem_closedBall, dist_zero_right, abs_of_pos hb]
        linarith

Goal state after:
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this : DecidableEq ι
disj : Disjoint s (image (fun z ↦ ↑z) s')
⊢ #s' = #(s ∪ image (fun z ↦ ↑z) s') - #s

Tactic:
simp [disj, card_image_of_injective _ Subtype.coe_injective, Nat.add_sub_cancel_left]

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

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
l : List P
h : List.Wbtw R l
hl : ¬l = []
⊢ ∃ p₁ p₂ l', l'.SortedLE ∧ map (⇑(lineMap p₁ p₂)) l' = l

Tactic:
exact ⟨l.head hl, l.getLast hl, (exists_map_eq_of_sorted_nonempty_iff_wbtw hl).2 h⟩

Goal state after: