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
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hB : ‖f z‖ ≤ B
hset : z ∈ verticalClosedStrip 0 1
⊢ ‖↑(ε + sSupNormIm f 1) ^ (-z)‖ ≤ max 1 ((ε + sSupNormIm f 1) ^ (-1))

Tactic:
· by_cases hM1_one : 1 ≤ ε + sSupNormIm f 1
    -- `1 ≤ sSupNormIm f 1`
    · apply le_trans _ (le_max_left _ _)
      simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 1),
        neg_re, Real.rpow_le_one_of_one_le_of_nonpos
        hM1_one (Right.neg_nonpos_iff.mpr hset.1)]
    -- `0 < sSupNormIm f 1 < 1`
    · rw [not_le] at hM1_one; apply le_trans _ (le_max_right _ _)
      simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 1),
        neg_re, Real.rpow_le_rpow_of_exponent_ge (sSupNormIm_eps_pos f hε 1)
        (le_of_lt hM1_one) (neg_le_neg_iff.mpr hset.2)]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ∃ c < Real.pi / (1 - 0),
    ∃ B,
      (fun x ↦ invInterpStrip f x ε • f x) =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z ↦
        Real.exp (B * Real.exp (c * |z.im|))

Tactic:
use 0

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < Real.pi / (1 - 0) ∧
    ∃ B,
      (fun x ↦ invInterpStrip f x ε • f x) =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z ↦
        Real.exp (B * Real.exp (0 * |z.im|))
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
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
g : G
x : X
e : ↑(p ⁻¹' {x})
γ✝ γ γ' : FundamentalGroup X x
⊢ ↑(⋯.monodromy γ (⋯.monodromy γ' e)) = (hp.fiberEquivGroup e) (⋯.monodromy γ' e) • ↑(⋯.monodromy γ e)

Tactic:
← hp.toPermFiber_apply_apply_coe

Goal state after:
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hp : IsQuotientCoveringMap p G
g : G
x : X
e : ↑(p ⁻¹' {x})
γ✝ γ γ' : FundamentalGroup X x
⊢ ↑(⋯.monodromy γ (⋯.monodromy γ' e)) =
    ↑(((hp.toPermFiber x) ((hp.fiberEquivGroup e) (⋯.monodromy γ' e))) (⋯.monodromy γ e))
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c : ℂ
r a₁ a₂ b : ℝ
ha₁ : ↑a₁ + ↑b * I ∈ ball c r
ha₂ : ↑a₂ + ↑b * I ∈ ball c r
⊢ (fun x ↦ ↑x + ↑b * I) '' [[a₁, a₂]] ⊆ ball c r

Tactic:
convert Convex.rectangle_subset (convex_ball c r) ha₁ ha₂ ?_ ?_ <;>
  simp [horizontalSegment_eq a₁ a₂ b, ha₁, ha₂, Rectangle]

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init m 0 = m 0
⊢ tail m (last n) = m (last n.succ)

Tactic:
simp only [tail_def, succ_last]

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

Goal state before:
pp: case hg.h
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‖
⊢ sSupNormIm f 1 ≠ 0 ∨ 0 ≤ z.re

Tactic:
· right; simp only [le_of_lt hz.1]

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

Goal state before:
pp: 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
r₁ : ℝ := r - dist z c
r₁_pos : 0 < r₁
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
zRe_mem_s : z.re ∈ s
f_contOn : ContinuousOn (fun x ↦ f (↑x + ↑z.im * I)) s
int1 : IntervalIntegrable (fun x ↦ f (↑x + ↑z.im * I)) volume z.re z.re
⊢ (fun x ↦ (∫ (t : ℝ) in z.re..x, f (↑t + ↑z.im * I)) - (x - z.re) • f z) =o[𝓝 z.re] fun x ↦ x - z.re

Tactic:
have int2 : StronglyMeasurableAtFilter (fun (x : ℝ) ↦ f (x + z.im * I)) (𝓝 z.re) :=
    f_contOn.stronglyMeasurableAtFilter isOpen_Ioo _ zRe_mem_s

Goal state after:
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
r₁ : ℝ := r - dist z c
r₁_pos : 0 < r₁
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
zRe_mem_s : z.re ∈ s
f_contOn : ContinuousOn (fun x ↦ f (↑x + ↑z.im * I)) s
int1 : IntervalIntegrable (fun x ↦ f (↑x + ↑z.im * I)) volume z.re z.re
int2 : StronglyMeasurableAtFilter (fun x ↦ f (↑x + ↑z.im * I)) (𝓝 z.re) volume
⊢ (fun x ↦ (∫ (t : ℝ) in z.re..x, f (↑t + ↑z.im * I)) - (x - z.re) • f z) =o[𝓝 z.re] fun x ↦ x - z.re
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: case neg
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
⊢ ∃ F, AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun z ↦ (F z).re) f (ball z R)

Tactic:
have h₁F : DifferentiableOn ℂ F (ball z R) :=
    fun x hx ↦ (hF.2 x hx).differentiableAt.differentiableWithinAt

Goal state after:
case neg
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)
⊢ ∃ F, AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun z ↦ (F z).re) f (ball z R)
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 (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ ContinuousWithinAt f (Ioi 0 ×ℂ Ioi 0) 0

Tactic:
refine (hd.continuousOn _ ?_).mono subset_closure

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
⊢ 0 ∈ closure (Ioi 0 ×ℂ Ioi 0)
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: case e_a.e_f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ (fun θ ↦ (fun z ↦ f (z + c)) (0 + ↑R * cexp (↑θ * I))) = fun θ ↦ f (c + ↑R * cexp (↑θ * I))

Tactic:
ext θ

Goal state after:
case e_a.e_f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R θ : ℝ
⊢ (fun z ↦ f (z + c)) (0 + ↑R * cexp (↑θ * I)) = f (c + ↑R * cexp (↑θ * I))
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
hR : 0 ≤ R
⊢ circleAverage f c |R| = circleAverage f c R

Tactic:
rw [abs_of_nonneg hR]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) = a

Tactic:
conv =>
    left; arg 2; arg 1
    intro θ
    rw [hf (circleMap c R θ) (circleMap_mem_sphere' c R θ)]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
⊢ (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, a = a
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
h_subst : (R ^ 2 - r ^ 2) / (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)) ≤ (R + r) / (R - r)
this :
  R * R * normSq (cexp (↑θ * I)) + r * r * normSq (cexp (↑φ * I)) -
      2 * (R * Real.cos θ * (r * Real.cos φ) + R * Real.sin θ * (r * Real.sin φ)) =
    R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)
⊢ (‖↑R * cexp (↑θ * I)‖ ^ 2 - ‖↑r * cexp (↑φ * I)‖ ^ 2) / ‖↑R * cexp (↑θ * I) - ↑r * cexp (↑φ * I)‖ ^ 2 =
    (R ^ 2 - r ^ 2) / (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ))

Tactic:
by
    rw [← this]; simp [← normSq_eq_norm_sq, Complex.normSq_sub]

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

Goal state before:
pp: θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ (R - r) / (R + r) ≤ (R + r) * (R - r) / ‖↑R * cexp (↑θ * I) - ↑r * cexp (↑φ * I)‖ ^ 2

Tactic:
field_simp [sub_pos.mpr h₂]

Goal state after:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 1 / (R + r) ≤ (R + r) / ‖↑R * cexp (↑θ * I) - ↑r * cexp (I * ↑φ)‖ ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
⊢ 0 ≤ x.negMulLog

Tactic:
by
  simpa only [negMulLog_eq_neg, neg_nonneg] using mul_log_nonpos h1 h2

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

Goal state before:
pp: ⊢ DifferentiableOn ℝ negMulLog {0}ᶜ

Tactic:
by
  simpa only [negMulLog_eq_neg] using! differentiableOn_mul_log.neg

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

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

Tactic:
rw [intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)), sub_self,
    (by linarith : π - π / 2 = π / 2)]

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

Goal state before:
pp: a b : ℝ
ha : 1 < a
hb : 1 < b
this : ContinuousOn (fun x ↦ -x⁻¹ * (log x)⁻¹ ^ 2) [[a, b]]
⊢ ContinuousOn (deriv fun t ↦ (log t)⁻¹) [[a, b]]

Tactic:
by
    convert this using 2 with x
    simp [field]

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

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ circleAverage (fun x ↦ log ‖x - a‖) c R = circleAverage (fun z ↦ log ‖↑R * (z + ↑R⁻¹ * (c - a))‖) 0 1

Tactic:
rw [circleAverage_eq_circleAverage_zero_one]
    congr
    ext z
    congr
    rw [Complex.ofReal_inv R]
    field [Complex.ofReal_ne_zero.mpr hR]

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
h : ∃ z₀ ∈ U, ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀
⊢ (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)

Tactic:
obtain ⟨z₀, hz₀, h⟩ := h
    exact Or.inl ⟨g z₀, hg.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const hU hz₀ h⟩

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

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
⊢ Irreducible p

Tactic:
refine hp.irreducible_of_coprime fun q hq hq' => ?_

Goal state after:
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
⊢ IsUnit q
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
⊢ f x ≤ f y

Tactic:
have xs : x ∈ s := A _ hx hxc.le
    rcases lt_or_ge y c with (hyc | hcy)
    · exact h₁ xs (A _ hy hyc.le) hxy
    · exact (h₁ xs hs.1 hxc.le).trans (h₂ ht.1 (B _ hy hcy) hcy)

Goal state after:
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
⊢ TietzeExtension ↑(Metric.closedBall 0 1)

Tactic:
have : IsScalarTower ℝ 𝕜 E := Real.isScalarTower

Goal state after:
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝ : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
⊢ TietzeExtension ↑(Metric.closedBall 0 1)
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.refine_1
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‖ ≤ ‖f‖ / 3

Tactic:
refine (norm_le <| div_nonneg hf.le h3.le).mpr fun y => ?_

Goal state after:
case inr.refine_1
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)
y : Y
⊢ ‖g y‖ ≤ ‖f‖ / 3
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case a
g : GL (Fin 2) ℝ
h : (↑g).det < 0
z : ℍ
hz : g • z = z
⊢ (↑g).trace + ((σ g) ↑z * denom g ↑z).im / z.im - (0 + (num g ↑z).im / z.im) = 0

Tactic:
{ simp [σ, h.not_gt, num, denom, z.im_ne_zero, Matrix.trace_fin_two, field] }

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
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
⊢ ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0 = ↑g 1 1 ^ 2

Tactic:
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
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
⊢ ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * 0 = ↑g 1 1 ^ 2
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:
← hsub,

Goal state after:
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 - (c - f x)
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:
← hsub,

Goal state after:
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 - (c - a)
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 : ∃ᶠ (τ : ℍ) in 𝓝[≠] I, ∏ i ∈ s, f i τ = 0
⊢ ∃ i ∈ s, f i = 0

Tactic:
simp only [Finset.prod_eq_zero_iff, Finset.frequently_exists] at this

Goal state after:
ι : 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
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: case e'_9.e'_3
x : ℝ
⊢ √(1 + x ^ 2) = cosh (↑sinhHomeomorph.toOpenPartialHomeomorph.symm x)

Tactic:
exact (cosh_arsinh _).symm

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

Goal state before:
pp: ⊢ sinh ~[𝓝 0] id

Tactic:
by simpa using! (hasDerivAt_sinh 0).isLittleO

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

Goal state before:
pp: case refine_2
x : ℝ
hx : x ∈ interior (Ici 0)
⊢ 0 < deriv (fun x ↦ sinh x - x) x

Tactic:
rw [interior_Ici, mem_Ioi] at hx
    rw [deriv_fun_sub, deriv_sinh, deriv_id'', sub_pos, one_lt_cosh]
    exacts [hx.ne', differentiableAt_sinh, differentiableAt_id]

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: case mpr
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Mono (↾⇑(ConcreteCategory.hom f)) → Mono f

Tactic:
apply (forget (CompHausLike P)).mono_of_mono_map

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

Goal state before:
pp: case refine_1
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s ↦ {u | s ∈ u}) a
ub : u ∈ (fun s ↦ {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s ↦ {u | s ∈ u}) (a ∩ b)
⊢ v ∈ (fun s ↦ {u | s ∈ u}) a

Tactic:
apply mem_of_superset hv

Goal state after:
case refine_1
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s ↦ {u | s ∈ u}) a
ub : u ∈ (fun s ↦ {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s ↦ {u | s ∈ u}) (a ∩ b)
⊢ a ∩ b ⊆ a
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: case refine_2
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s ↦ {u | s ∈ u}) a
ub : u ∈ (fun s ↦ {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s ↦ {u | s ∈ u}) (a ∩ b)
⊢ v ∈ (fun s ↦ {u | s ∈ u}) b

Tactic:
apply mem_of_superset hv

Goal state after:
case refine_2
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s ↦ {u | s ∈ u}) a
ub : u ∈ (fun s ↦ {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s ↦ {u | s ∈ u}) (a ∩ b)
⊢ a ∩ b ⊆ b
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ Tendsto preStoneCechUnit (↑g) (𝓝 (preStoneCechUnit x))

Tactic:
have : (g.map pure).toFilter ≤ 𝓝 g := by
      rw [ultrafilter_converges_iff, ← bind_pure g]
      rfl
    have : (map preStoneCechUnit g : Filter (PreStoneCech α)) ≤ 𝓝 (Quot.mk _ g) :=
      (map_mono this).trans (continuous_quot_mk.tendsto _)
    convert! this
    exact Quot.sound ⟨x, pure_le_nhds x, gx⟩

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

Goal state before:
pp: case neg
z w : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z ↦ ModularGroup.S • z
hc : ¬↑g 1 0 = 0
⊢ Isometry fun x ↦ g • x

Tactic:
obtain ⟨u, v, w, h⟩ := exists_SL2_smul_eq_of_apply_zero_one_ne_zero g hc

Goal state after:
case neg
z w✝ : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z ↦ ModularGroup.S • z
hc : ¬↑g 1 0 = 0
u : { x // 0 < x }
v w : ℝ
h : (fun x ↦ g • x) = (fun x ↦ w +ᵥ x) ∘ (fun x ↦ ModularGroup.S • x) ∘ (fun x ↦ v +ᵥ x) ∘ fun x ↦ u • x
⊢ Isometry fun x ↦ g • x
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case infty.coe
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝ : X
⊢ ∞ ⤳ ↑x✝ ∨ Disjoint (𝓝 ∞) (𝓝 ↑x✝)

Tactic:
exact .inr (key _).symm

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
this : divisor f (closedBall 0 |R|) = (toClosedBall R) (divisor f Set.univ)
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall 0 |R|)) u) * log (R * ‖0 - u‖⁻¹) + ↑((divisor f (closedBall 0 |R|)) 0) * log R +
        log ‖meromorphicTrailingCoeffAt f 0‖ -
      { toFun := fun D r ↦ ∑ᶠ (z : ℂ), ↑(((toClosedBall r) D) z) * log (r * ‖z‖⁻¹) + ↑(D 0) * log r, map_zero' := ⋯,
          map_add' := ⋯ }
        (divisor f Set.univ) R =
    log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
simp [this, toClosedBall, restrictMonoidHom, restrict_apply]

Goal state after: