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

Goal state before:
pp: c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
x✝¹ : ℂ
x✝ : x✝¹ ∈ Function.support fun u ↦ ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r)
⊢ x✝¹ ∈ (divisor f (closedBall c |r|)).support

Tactic:
simp_all

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

Goal state before:
pp: c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
x✝¹ : ℂ
x✝ : x✝¹ ∈ Function.support fun u ↦ ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)
⊢ x✝¹ ∈ (divisor f (closedBall c |R|)).support

Tactic:
simp_all

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

Goal state before:
pp: X : Type u
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
f : ↑s →ᵇ E
hf : ¬‖f‖ = 0
⊢ 0 < ‖f‖

Tactic:
simp_all

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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
u : Rˣ
⊢ mk ((GeneralLinearGroup.scalar n) u) = 1

Tactic:
by
  rw [← MonoidHom.mem_ker, ker_mk, GeneralLinearGroup.center_eq_range_scalar]
  simp

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

Goal state before:
pp: c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∉ closedBall c |R|
⊢ u ∉ closedBall c |r|

Tactic:
simp_all

Goal state after:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
u : ℂ
r_pos : ¬r = 0
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : ¬f c = 0
f_bound : ∀ (z : ℂ), ‖z - c‖ = |R| → ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound :
  ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖ ≤ Real.log M
h1 : |R| < dist u c
⊢ |r| < dist u c
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case inr
g : GL (Fin 2) ℝ
z : ℍ
hpos : 0 < (↑g).det
hell : g.IsElliptic
this : ∀ {g : GL (Fin 2) ℝ}, 0 < (↑g).det → ∀ (hell : g.IsElliptic), 0 < ↑g 1 0 → (g • z = z ↔ z = fixedPt g hell)
hc : ¬0 < ↑g 1 0
⊢ g • z = z ↔ z = fixedPt g hell

pp: g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
⊢ g • z = z ↔ z = fixedPt g hell

Tactic:
· replace hc := hell.c_ne_zero.lt_or_gt.resolve_right hc
    simpa using @this (-g) (by simpa [Matrix.det_neg]) hell.neg (by simpa)

Goal state after:
g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
⊢ g • z = z ↔ z = fixedPt g hell
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g h : GL (Fin 2) R
⊢ (g * h * g⁻¹).IsParabolic ↔ h.IsParabolic

Tactic:
simp [IsParabolic]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g h : GL (Fin 2) R
⊢ (g⁻¹ * h * g).IsParabolic ↔ h.IsParabolic

Tactic:
simp [IsParabolic]

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

Goal state before:
pp: case mp.inl.inl
g : GL (Fin 2) ℝ
hg : { coe := 1 + Complex.I, coe_im_pos := ⋯ }.re = ↑g 0 1 / (2 * ↑g 1 1)
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g).det < 0
ha : (↑g).trace = 0
hb : ↑g 0 1 = ↑g 1 0
hc : ↑g 1 0 = 0
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: w : ℂ
⊢ ↑ofComplex w = if hw : 0 < w.im then { coe := w, coe_im_pos := hw } else Classical.choice ⋯

Tactic:
split_ifs with hw

Goal state after:
case pos
w : ℂ
hw : 0 < w.im
⊢ ↑ofComplex w = { coe := w, coe_im_pos := hw }

case neg
w : ℂ
hw : ¬0 < w.im
⊢ ↑ofComplex w = Classical.choice ⋯
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
⊢ ‖r / ‖‖↑τ‖‖ - 1‖ * ‖‖↑τ‖‖ < ε

Tactic:
← norm_mul,

Goal state after:
τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
⊢ ‖(r / ‖‖↑τ‖‖ - 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
⊢ !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] = ↑(upperRightHom (!![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] 0 1))

Tactic:
simp_all

Goal state after:
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
⊢ !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] = ↑(-upperRightHom (-!![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] 0 1))

Tactic:
simp_all

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

Goal state before:
pp: z : ℍ
⊢ ↑√z.im ≠ 0

Tactic:
simpa [Real.sqrt_ne_zero'] using z.im_pos

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

Goal state before:
pp: z : ℍ
this✝ : ↑√z.im ≠ 0
this : ↑z.re / ↑√z.im + ↑√z.im * Complex.I = ↑z * (↑√z.im)⁻¹
⊢ ↑(z.toSL2R • I) = ↑z

Tactic:
rw [coe_specialLinearGroup_apply, div_eq_iff (mod_cast denom_ne_zero z.toSL2R I)]

Goal state after:
z : ℍ
this✝ : ↑√z.im ≠ 0
this : ↑z.re / ↑√z.im + ↑√z.im * Complex.I = ↑z * (↑√z.im)⁻¹
⊢ ↑((algebraMap ℝ ℝ) (↑z.toSL2R 0 0)) * ↑I + ↑((algebraMap ℝ ℝ) (↑z.toSL2R 0 1)) =
    ↑z * (↑((algebraMap ℝ ℝ) (↑z.toSL2R 1 0)) * ↑I + ↑((algebraMap ℝ ℝ) (↑z.toSL2R 1 1)))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure

Goal state before:
pp: case e'_3
g : GL (Fin 2) ℝ
s : Set ℍ
hs : MeasurableSet s
hinj : Set.InjOn (fun z ↦ ↑(g • ↑ofComplex z)) (UpperHalfPlane.coe '' s)
main :
  ∫⁻ (x : ℂ) in (fun z ↦ ↑(g • ↑ofComplex z)) '' UpperHalfPlane.coe '' s, ↑((1 / ‖x.im‖₊) ^ 2) =
    ∫⁻ (x : ℂ) in UpperHalfPlane.coe '' s,
      ENNReal.ofReal |(smulFDeriv g x).det| * ↑((1 / ‖(↑(g • ↑ofComplex x)).im‖₊) ^ 2)
τ : ℍ
⊢ ↑((1 / ‖(↑τ).im‖₊) ^ 2) = ↑‖(smulFDeriv g ↑τ).det‖₊ * ↑((1 / ‖(↑(g • ↑ofComplex ↑τ)).im‖₊) ^ 2)

Tactic:
have : ‖(SignType.sign g.val.det : ℝ)‖₊ = 1 := by
      rcases g.det_ne_zero.lt_or_gt with h | h <;> simp [h]

Goal state after:
case e'_3
g : GL (Fin 2) ℝ
s : Set ℍ
hs : MeasurableSet s
hinj : Set.InjOn (fun z ↦ ↑(g • ↑ofComplex z)) (UpperHalfPlane.coe '' s)
main :
  ∫⁻ (x : ℂ) in (fun z ↦ ↑(g • ↑ofComplex z)) '' UpperHalfPlane.coe '' s, ↑((1 / ‖x.im‖₊) ^ 2) =
    ∫⁻ (x : ℂ) in UpperHalfPlane.coe '' s,
      ENNReal.ofReal |(smulFDeriv g x).det| * ↑((1 / ‖(↑(g • ↑ofComplex x)).im‖₊) ^ 2)
τ : ℍ
this : ‖↑(SignType.sign (↑g).det)‖₊ = 1
⊢ ↑((1 / ‖(↑τ).im‖₊) ^ 2) = ↑‖(smulFDeriv g ↑τ).det‖₊ * ↑((1 / ‖(↑(g • ↑ofComplex ↑τ)).im‖₊) ^ 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
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
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

Tactic:
have : OrdConnected t' := by
    constructor
    rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ z hz
    lift z to Ioo (-1 : ℝ) 1 using Icc_subset_Ioo (h x).2.1 (h y).2.2 hz
    change z ∈ Icc (h x) (h y) at hz
    rw [← h.image_Icc] at hz
    rcases hz with ⟨z, hz, rfl⟩
    exact ⟨z, hs.out hx hy hz, rfl⟩

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
this : t'.OrdConnected
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case convert_2
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
hτ : ∀ᶠ (a : ℍ) in 𝓝 τ, ↑a ∈ {↑τ}ᶜ → (f ∘ ↑ofComplex) ↑a ≠ 0
⊢ ∀ᶠ (x : ℍ) in 𝓝[≠] τ, f x ≠ 0

Tactic:
eventually_nhdsWithin_iff

Goal state after:
case convert_2
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
hτ : ∀ᶠ (a : ℍ) in 𝓝 τ, ↑a ∈ {↑τ}ᶜ → (f ∘ ↑ofComplex) ↑a ≠ 0
⊢ ∀ᶠ (x : ℍ) in 𝓝 τ, x ∈ {τ}ᶜ → f x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ sinh (arsinh x) = x

Tactic:
sinh_eq,

Goal state after:
x : ℝ
⊢ (rexp (arsinh x) - rexp (-arsinh x)) / 2 = x
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ Tendsto (dist c) (𝓝[≠] c) (𝓝[>] 0)

Tactic:
rw [tendsto_nhdsWithin_iff]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ Tendsto (dist c) (𝓝[≠] c) (𝓝 0) ∧ ∀ᶠ (n : P) in 𝓝[≠] c, dist c n ∈ Ioi 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case inr
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
hzw₀ : 0 < 2 * z.im * w.im
⊢ cmp (Real.cosh (dist z w)) (Real.cosh r) =
    cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2) ((w.im * Real.sinh r) ^ 2)

Tactic:
rw [← cmp_mul_pos_left hzw₀, ← cmp_sub_zero, ← mul_sub, ← cmp_add_right, zero_add]

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

Goal state before:
pp: z w : ℍ
⊢ dist ↑z ↑(w.center (dist z w)) + dist ↑w ↑(w.center (dist z w)) = w.im * (rexp (dist z w) - 1)

Tactic:
dist_center_dist,

Goal state after:
z w : ℍ
⊢ w.im * Real.sinh (dist z w) + dist ↑w ↑(w.center (dist z w)) = w.im * (rexp (dist z w) - 1)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ w.im * (Real.sinh (dist z w) + Real.cosh (dist z w) - 1) = w.im * (rexp (dist z w) - 1)

Tactic:
Real.sinh_add_cosh

Goal state after:
z w : ℍ
⊢ w.im * (rexp (dist z w) - 1) = w.im * (rexp (dist z w) - 1)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ w.im * (1 - rexp (-dist z w)) = dist ↑z ↑(w.center (dist z w)) - dist ↑w ↑(w.center (dist z w))

Tactic:
dist_center_dist,

Goal state after:
z w : ℍ
⊢ w.im * (1 - rexp (-dist z w)) = w.im * Real.sinh (dist z w) - dist ↑w ↑(w.center (dist z w))
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: case mpr
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ s ∈ x, {v | s ∈ v} ∈ u) → ∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s ↦ {u | s ∈ u}) → i ∈ ↑u

Tactic:
rintro h a ⟨xi, a, rfl⟩

Goal state after:
case mpr
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ s ∈ x, {v | s ∈ v} ∈ u
a : Set α
xi : x ∈ (fun s ↦ {u | s ∈ u}) a
⊢ (fun s ↦ {u | s ∈ u}) a ∈ ↑u
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₂ / (2 * √(y₁.im * y₂.im)) / (‖↑y₁‖ * ‖↑y₂‖ / ‖↑y₁ * ↑y₂‖)) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))

Tactic:
← norm_mul,

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₂ / (2 * √(y₁.im * y₂.im)) / (‖↑y₁ * ↑y₂‖ / ‖↑y₁ * ↑y₂‖)) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
x₁ x₂ : X
⊢ ↑x₁ = ↑x₂ ↔ x₁ = x₂

Tactic:
iff_eq_eq

Goal state after:
X : Type u_1
x₁ x₂ : X
⊢ (↑x₁ = ↑x₂) = (x₁ = 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✝)

pp: case coe.infty
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✝) (𝓝 ∞)

pp: case coe.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
⊢ ↑x✝¹ ⤳ ↑x✝ ∨ Disjoint (𝓝 ↑x✝¹) (𝓝 ↑x✝)

Tactic:
· exact .inr (key _).symm

Goal state after:
case coe.infty
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✝) (𝓝 ∞)

case coe.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
⊢ ↑x✝¹ ⤳ ↑x✝ ∨ Disjoint (𝓝 ↑x✝¹) (𝓝 ↑x✝)
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
h : a = ⊤
⊢ 0 ≤ proximity f a

Tactic:
intro r
    simpa [proximity, h] using circleAverage_nonneg_of_nonneg (fun x _ ↦ posLog_nonneg)

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

Goal state before:
pp: case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
h : ¬a = ⊤
⊢ 0 ≤ proximity f a

Tactic:
intro r
    simpa [proximity, h] using circleAverage_nonneg_of_nonneg (fun x _ ↦ posLog_nonneg)

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

Goal state before:
pp: case pos
f : ℂ → ℂ
h : ¬MeromorphicAt f 0
this : ∀ {a : ℂ}, ¬MeromorphicAt (fun x ↦ f x - a) 0
⊢ CircleIntegrable (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1

Tactic:
simp_all

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

Goal state before:
pp: case neg.inr.inl
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hzero : meromorphicOrderAt f 0 = 0
⊢ CircleIntegrable (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1

Tactic:
apply CircleIntegrable.congr_codiscreteWithin
     (eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero (not_not.1 h) hzero)
    simpa [norm_sub_rev] using circleIntegrable_log_norm_sub_const 1

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

Goal state before:
pp: case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this✝ : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
x : E
hx : x ∈ Function.support fun z ↦ ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)
this : x ∉ ↑h₁s.toFinset
⊢ False

pp: case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

pp: case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

Tactic:
simp_all

Goal state after:
case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this✝ : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
x : E
hx : x ∈ Function.support fun z ↦ ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹)
this : x ∉ ↑h₁s.toFinset
⊢ False

pp: case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

Tactic:
simp_all

Goal state after:
case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this✝ : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
x : E
hx : x ∈ Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)
this : x ∉ ↑h₁s.toFinset
⊢ False

Tactic:
simp_all

Goal state after:
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 : ℝ
⊢ ∃ b_1, b ≤ b_1 ∧ 1 < a * |logCounting D b_1|

Tactic:
obtain ⟨c, hc⟩ := eventually_atTop.1
    (isLittleO_iff.1 (one_isLittleO_logCounting_single (e := e)) ha)

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‖
⊢ ∃ b_1, b ≤ b_1 ∧ 1 < a * |logCounting D b_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‖
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ 1 ≤ a * |logCounting (single e 1) ℓ|

Tactic:
simpa [h₁ℓ] using hc ℓ

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

Goal state before:
pp: case pos
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
a : E
h₁a : a = 0
⊢ 0 ≤ ↑(((toClosedBall r) f) a) * log (r * ‖a‖⁻¹)

Tactic:
simp_all

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

Goal state before:
pp: case e_a
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ ∑ᶠ (z : ℂ), ↑(((toClosedBall R) (divisor f univ)) z) * log (R * ‖z‖⁻¹) =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall 0 |R|)) u) * log (R * ‖u‖⁻¹)

Tactic:
simp_all

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕'.Nonempty
f : ℕ → ↑s → ℝ
hf : 𝓕' = range f
i : ℕ
⊢ ∃ l c, f i = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c

Tactic:
simp_all

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

Goal state before:
pp: case pos.refine_2
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕' = ∅
hsφ : s.domRestrict φ = 0
this : ∀ (a : ↑s), s.domRestrict φ a = 0 a
x✝ : ↑s
⊢ (⨆ i, s.domRestrict (⇑re ∘ ⇑((fun x ↦ 0) i)) + const (↑s) ((fun x ↦ 0) i)) x✝ = s.domRestrict φ x✝

Tactic:
simp_all

Goal state after: