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

Goal state before:
pp: case inr.inr.inr.refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this : ∀ {C : ℝ}, (∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) → (∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) → 0 < C → ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
⊢ (↑a * I).im = a

Tactic:
rw [mul_I_im, ofReal_re]

Goal state after:
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 = l
hz₂ : f z = e
⊢ ((z - ↑l) / (↑u - ↑l)).re = 0

Tactic:
norm_cast
        rw [Complex.div_re, Complex.normSq_ofReal, Complex.ofReal_re]
        simp [hz₁]

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

Goal state before:
pp: case right
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
h : HarmonicAt f x
l : F →L[ℝ] G
⊢ Δ (⇑l ∘ f) =ᶠ[𝓝 x] 0

Tactic:
filter_upwards [h.1.laplacian_CLM_comp_left_nhds (l := l), h.2]
    simp_all

Goal state after:
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:
obtain ⟨ℓ, h₁ℓ, h₂ℓ⟩ := exists_dual_vector'' ℝ (f z - f 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 : ℂ
ℓ : StrongDual ℝ E
h₁ℓ : ‖ℓ‖ ≤ 1
h₂ℓ : ℓ (f z - f w) = ↑‖f z - f w‖
⊢ f z = f w
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: z : ℍ
n : ℤ
hn : n ≠ 0
w✝ : ℤ
hm : ↑w✝ = ↑n / ↑z
⊢ False

Tactic:
have : (n / (z : ℂ)).im ≠ 0 := by simp [div_im, z.ne_zero, hn, z.im_ne_zero]

Goal state after:
z : ℍ
n : ℤ
hn : n ≠ 0
w✝ : ℤ
hm : ↑w✝ = ↑n / ↑z
this : (↑n / ↑z).im ≠ 0
⊢ False
Module: Mathlib.Analysis.Complex.IsIntegral

Goal state before:
pp: ⊢ I ^ 2 + (algebraMap ℤ ℂ) 1 = 0

Tactic:
I_sq,

Goal state after:
⊢ -1 + (algebraMap ℤ ℂ) 1 = 0
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 t) volume
I : 0 < min 1 t
H' : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 (min 1 t)) volume
x : ℝ
hx : x ∈ Ioo 0 (min 1 t)
⊢ x⁻¹ ≤ x ^ s

Tactic:
← Real.rpow_neg_one x,

Goal state after:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 t) volume
I : 0 < min 1 t
H' : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 (min 1 t)) volume
x : ℝ
hx : x ∈ Ioo 0 (min 1 t)
⊢ x ^ (-1) ≤ x ^ s
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: a b : ℝ
r : ℂ
h : -1 < r.re
⊢ IntervalIntegrable (fun x ↦ ↑x ^ r) volume a b

Tactic:
suffices ∀ c : ℝ, IntervalIntegrable (fun x => (x : ℂ) ^ r) volume 0 c by
    exact IntervalIntegrable.trans (this a).symm (this b)
  have : ∀ c : ℝ, 0 ≤ c → IntervalIntegrable (fun x => (x : ℂ) ^ r) volume 0 c := by
    intro c hc
    rw [← IntervalIntegrable.intervalIntegrable_norm_iff]
    · 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
    · refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_uIoc
      refine continuousOn_of_forall_continuousAt fun x hx => ?_
      rw [uIoc_of_le hc] at hx
      refine (continuousAt_cpow_const (Or.inl ?_)).comp Complex.continuous_ofReal.continuousAt
      rw [Complex.ofReal_re]
      exact hx.1
  intro c; rcases le_total 0 c with (hc | hc)
  · exact this c hc
  · rw [IntervalIntegrable.iff_comp_neg, neg_zero]
    have m := (this (-c) (by linarith)).const_mul (Complex.exp (π * Complex.I * r))
    rw [intervalIntegrable_iff, uIoc_of_le (by linarith : 0 ≤ -c)] at m ⊢
    refine m.congr_fun (fun x hx => ?_) measurableSet_Ioc
    #adaptation_note /-- 2026-05-17(kmill) added `dsimp only` because a slightly different
    instantiation order leads to a term with a beta redex.
    https://github.com/leanprover/lean4/pull/13762
    This will be removed once app elaboration itself does beta reduction. -/
    dsimp only
    have : -x ≤ 0 := by linarith [hx.1]
    rw [Complex.ofReal_cpow_of_nonpos this, mul_comm]
    simp

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

Goal state before:
pp: R : ℝ
w c : ℂ
hw : w ∈ ball c R
this✝ : Disjoint {w} (ball c R)ᶜ
d : ℝ
hd : 0 < d
h_disj : Disjoint (ball w d) (thickening d (ball c R)ᶜ)
x : ℂ
hx : x ∈ ball w d
θ : ℝ
this : ∀ (x_1 : ℂ), R ≤ dist x_1 c → d ≤ dist x x_1
⊢ R ≤ dist (circleMap c R θ) c

Tactic:
simp [dist_eq_norm, le_abs_self]

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

Goal state before:
pp: ⊢ IntervalIntegrable (fun x ↦ log (sin (2 * x)) - log 2) MeasureTheory.volume 0 (π / 2)

Tactic:
apply IntervalIntegrable.sub _ intervalIntegrable_const

Goal state after:
⊢ IntervalIntegrable (fun x ↦ log (sin (2 * x))) MeasureTheory.volume 0 (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

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

Tactic:
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

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := ⋯
gray : E → ℂ → ℂ := ⋯
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
⊢ ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀

Tactic:
refine eventually_of_mem (ball_mem_nhds z₀ hr) fun z hz => ?_

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
z : E
hz : z ∈ ball z₀ r
⊢ g z = g z₀
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:
rw [finsum_eq_sum_of_support_subset]
    intro u
    contrapose
    aesop

Goal state after:
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
⊢ circleAverage (fun x ↦ log ‖f x‖) c R =
    circleAverage ((∑ᶠ (u : ℂ), fun x ↦ ↑((divisor f CB) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖) c R

Tactic:
by
      have h₄g := extract_zeros_poles_log h₂g h₃g
      rw [circleAverage_congr_codiscreteWithin (codiscreteWithin_mono sphere_subset_closedBall h₄g)
        hR]

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: α : ℝ
hα : α ≥ 0
ha : 0 ≤ ↑α
⊢ (↑α).sqrt = ↑√α

Tactic:
← re_add_im (α : ℂ).sqrt,

Goal state after:
α : ℝ
hα : α ≥ 0
ha : 0 ≤ ↑α
⊢ ↑(↑α).sqrt.re + ↑(↑α).sqrt.im * I = ↑√α
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X₁ : Type u₁
inst✝¹⁰ : TopologicalSpace X₁
X : Type u
inst✝⁹ : TopologicalSpace X
inst✝⁸ : NormalSpace X
s✝ : Set X
e : X₁ → X
Y✝ : Type v
inst✝⁷ : TopologicalSpace Y✝
inst✝⁶ : TietzeExtension Y✝
Y : Type v
Z : Type w
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : TietzeExtension Y
inst✝³ : TopologicalSpace Z
inst✝² : TietzeExtension Z
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, Y × Z)
g₁ : C(X✝, Y)
hg₁ : ContinuousMap.restrict s g₁ = ContinuousMap.fst.comp f
g₂ : C(X✝, Z)
hg₂ : ContinuousMap.restrict s g₂ = ContinuousMap.snd.comp f
⊢ ∃ g, ContinuousMap.restrict s g = f

Tactic:
exact ⟨g₁.prodMk g₂, by ext1 x; congrm(($(hg₁) x), $(hg₂) x)⟩

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:
← (σ g).injective.eq_iff

Goal state after:
g : GL (Fin 2) ℝ
z w : ℍ
⊢ g • z = w ↔ (σ g).toAlgEquiv (num g ↑z) = (σ g).toAlgEquiv ((σ g) ↑w * denom g ↑z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = (Complex.I * ↑√(-(↑g).discr)) ^ 2
h : ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0))
⊢ ((-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0))).im ≤ 0

Tactic:
simp [Complex.div_im, div_nonpos_iff, hc.le, mul_nonneg]

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

Goal state before:
pp: case refine_1.succ
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n✝ : ℕ
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
n : ℕ
hn : 1 ≤ n
IH : ((Matrix.scalar (Fin 2)) a + m) ^ n = (Matrix.scalar (Fin 2)) (a ^ n) + (↑n * a ^ (n - 1)) • m
⊢ (Matrix.scalar (Fin 2)) (a ^ n * a) +
      ((↑n * a ^ (n - 1)) • m * (Matrix.scalar (Fin 2)) a +
        ((Matrix.scalar (Fin 2)) (a ^ n) * m + (↑n * a ^ (n - 1)) • m * m)) =
    (Matrix.scalar (Fin 2)) (a ^ n * a) + (↑(n + 1) * a ^ n) • m

Tactic:
simp only [scalar_apply, ← smul_eq_mul_diagonal, ← mul_smul,
        ← smul_eq_diagonal_mul, smul_mul, ← sq, hmsq, smul_zero, add_zero, ← add_smul,
        Nat.cast_add_one, add_mul, one_mul]

Goal state after:
case refine_1.succ
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n✝ : ℕ
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
n : ℕ
hn : 1 ≤ n
IH : ((Matrix.scalar (Fin 2)) a + m) ^ n = (Matrix.scalar (Fin 2)) (a ^ n) + (↑n * a ^ (n - 1)) • m
⊢ (diagonal fun x ↦ a ^ n * a) + (a * (↑n * a ^ (n - 1)) + a ^ n) • m =
    (diagonal fun x ↦ a ^ n * a) + (↑n * a ^ n + a ^ n) • m
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: z : ℍ
n : ℤ
⊢ ↑(ModularGroup.T ^ n • z) = ↑z + ↑↑n

Tactic:
coe_specialLinearGroup_apply

Goal state after:
z : ℍ
n : ℤ
⊢ (↑((algebraMap ℤ ℝ) (↑(ModularGroup.T ^ n) 0 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑(ModularGroup.T ^ n) 0 1))) /
      (↑((algebraMap ℤ ℝ) (↑(ModularGroup.T ^ n) 1 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑(ModularGroup.T ^ n) 1 1))) =
    ↑z + ↑↑n
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⟩

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 →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
hgf : ⇑g ∘ e = ⇑f
⊢ ∃ g, (∀ (y : Y), ∃ x, g y ∈ Icc (f x) b) ∧ ⇑g ∘ e = ⇑f
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ (∑ j_1,
      M i j_1 * if j = k then if j_1 = k then 1 else 0 else if j_1 = k then -M k j else if j_1 = j then M k k else 0) =
    0

Tactic:
if_neg lt.2,

Goal state after:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ (∑ x, M i x * if x = k then -M k j else if x = j then M k k else 0) = 0
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case 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 dg : Y →ᵇ ℝ
hgf : ∀ (x : X), (g + dg) (e x) = f x
y : Y
ha : IsGLB (range ⇑f) (g y)
hmem : ∀ (x : X), f x ∈ Icc (g y) b
hle : g y ≤ b
hlt : g y < b
c : ℝ := (g y + b) / 2
hac : g y < c
hcb : c < b
hsub : c - g y = b - c
hg_mem : ∀ (y_1 : Y), g y_1 ∈ Icc (g y) b
ha' : ¬∃ x, f x = g y
hd : Disjoint (range e ∪ ⇑g ⁻¹' Ici c) (⇑g ⁻¹' {g y})
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Ici c)
dga : EqOn (⇑dg) (Function.const Y (c - g y)) (⇑g ⁻¹' {g y})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (c - g y)
⊢ g y < (g + dg) y

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
hlt : a < g y
⊢ a < (g + dg) y

Tactic:
· refine (lt_add_iff_pos_right _).2 ?_
        calc
          0 < c - g y := sub_pos.2 hac
          _ = dg y := (dga rfl).symm

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
hlt : a < g y
⊢ a < (g + dg) y
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : { x // x ∈ Ioo (-1) 1 }
hz : z ∈ Icc (h x) (h y)
⊢ ↑z ∈ t'

Tactic:
← h.image_Icc

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : { x // x ∈ Ioo (-1) 1 }
hz : z ∈ ⇑h '' Icc x y
⊢ ↑z ∈ t'
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
this : HasStrictDerivAt (num g / denom g) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ
⊢ HasStrictDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ

Tactic:
refine this.congr_of_eventuallyEq ?_

Goal state after:
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
this : HasStrictDerivAt (num g / denom g) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ
⊢ num g / denom g =ᶠ[𝓝 ↑τ] fun z ↦ ↑(g • ↑ofComplex z)
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
⊢ { toFun := Real.toNNReal, continuous_toFun := continuous_real_toNNReal }.comp
      { toFun := toReal, continuous_toFun := continuous_coe } =
    ContinuousMap.id ℝ≥0

Tactic:
by
    ext; simp

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ (∏ σ, σ (adjoin.powerBasis hx).gen) ^ finrank (↥K⟮x⟯) L = ∏ σ, σ x

Tactic:
exact (prod_embeddings_eq_finrank_pow L (L := K⟮x⟯) E (adjoin.powerBasis hx)).symm

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

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

Tactic:
by
  rw [← sqrt_sq (cosh_pos _).le, cosh_sq', sinh_arsinh]

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

Goal state before:
pp: a b c : ℍ
⊢ 0 < dist (↑b) ((starRingEnd ℂ) ↑b)

Tactic:
rw [dist_comm, dist_pos, Ne, Complex.conj_eq_iff_im]

Goal state after:
a b c : ℍ
⊢ ¬(↑b).im = 0
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 : ↑F ≤ 𝓝 x
hG : ↑G ≤ 𝓝 x
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G

Tactic:
replace hF := (map_mono hF).trans hg.continuousAt

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

Goal state before:
pp: case a
X : Type w
t : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
⊢ ∀ (a : CompHaus) (b : C(↑a.toTop, X)), Continuous[_, t] fun a_1 ↦ b a_1

Tactic:
exact fun S f ↦ f.2

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
⊢ Tendsto f (coclosedCompact X) (𝓝 y)

Tactic:
rw [coclosedCompact_eq_cocompact, hasBasis_cocompact.tendsto_left_iff]
    intro N hN
    obtain ⟨U, hU₁, hU₂, hU₃⟩ := mem_nhds_iff.mp hN
    refine ⟨f⁻¹' Uᶜ, ?_, by simpa using (mapsTo_preimage f U).mono_right hU₁⟩
    rw [hf.isCompact_iff, image_preimage_eq_iff.mpr (by simpa [hy])]
    exact (isClosed_compl_iff.mpr hU₂).isCompact

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

Goal state before:
pp: ⊢ ∀ (a : GL (Fin 2) ℝ) (b : ℍ), ContinuousAt (fun x ↦ (σ x.1) (num x.1 ↑x.2 / denom x.1 ↑x.2)) (a, b)

Tactic:
refine fun g τ ↦ .congr ?_ (f := fun x ↦ (σ g) (num x.1 x.2 / denom x.1 x.2))
    (by filter_upwards [(σ_eventuallyEq g).prod_inl_nhds _] using by simp +contextual)

Goal state after:
g : GL (Fin 2) ℝ
τ : ℍ
⊢ ContinuousAt (fun x ↦ (σ g) (num x.1 ↑x.2 / denom x.1 ↑x.2)) (g, τ)
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ proximity (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, proximity (f a) ⊤) r + log ↑s.card

Tactic:
apply proximity_sum_top_le s f hf r

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

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
⊢ (2 * π)⁻¹ * (2 * π)⁻¹ * ∫ (α : ℝ) (β : ℝ) in 0..2 * π, F α β =
    (2 * π)⁻¹ * (2 * π)⁻¹ * ∫ (β : ℝ) (α : ℝ) in 0..2 * π, F α β

Tactic:
rw [MeasureTheory.intervalIntegral_intervalIntegral_swap]

Goal state after:
f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
⊢ IntegrableOn (Function.uncurry F) (uIoc 0 (2 * π) ×ˢ uIoc 0 (2 * π)) volume
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
⊢ (2 * π)⁻¹ * (2 * π)⁻¹ * ∫ (α : ℝ) (β : ℝ) in 0..2 * π, F α β =
    (2 * π)⁻¹ * (2 * π)⁻¹ * ∫ (β : ℝ) (α : ℝ) in 0..2 * π, F α β

Tactic:
by
      rw [MeasureTheory.intervalIntegral_intervalIntegral_swap]
      exact Cartan.integrableOn_cartanKernel h

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

Goal state before:
pp: case pos
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : a = ⊤
⊢ logCounting f a = logCounting g a

Tactic:
simp only [logCounting, h, ↓reduceDIte]

Goal state after:
case pos
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : a = ⊤
⊢ locallyFinsuppWithin.logCounting (divisor f univ)⁻ = locallyFinsuppWithin.logCounting (divisor g univ)⁻
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case neg
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : ¬a = ⊤
⊢ logCounting f a = logCounting g a

Tactic:
simp only [logCounting, h, ↓reduceDIte]

Goal state after:
case neg
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : ¬a = ⊤
⊢ locallyFinsuppWithin.logCounting (divisor (fun x ↦ f x - a.untop₀) univ)⁺ =
    locallyFinsuppWithin.logCounting (divisor (fun x ↦ g x - a.untop₀) univ)⁺