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

Goal state before:
pp: case hab.hb₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ⋯
I₂ : E := ⋯
I₃ : E := ⋯
I₄ : E := ⋯
I₅ : E := ⋯
I₆ : E := ⋯
I₇ : E := ⋯
I₈ : E := ⋯
z_ball : ball z (r - dist z c) ⊆ ball c r
w_mem : w ∈ ball c r
integrableHoriz :
  ∀ (a₁ a₂ b : ℝ),
    ↑a₁ + ↑b * I ∈ ball c r → ↑a₂ + ↑b * I ∈ ball c r → IntervalIntegrable (fun x ↦ f (↑x + ↑b * I)) volume a₁ a₂
integrableVert :
  ∀ (a b₁ b₂ : ℝ),
    ↑a + ↑b₁ * I ∈ ball c r → ↑a + ↑b₂ * I ∈ ball c r → IntervalIntegrable (fun y ↦ f (↑a + ↑y * I)) volume b₁ b₂
hI₁ : I₁ = I₃ + I₇
⊢ ↑w.re + ↑z.im * I ∈ ball c r

Tactic:
exact mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)

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

Goal state before:
pp: case hbc.hb₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ⋯
I₂ : E := ⋯
I₃ : E := ⋯
I₄ : E := ⋯
I₅ : E := ⋯
I₆ : E := ⋯
I₇ : E := ⋯
I₈ : E := ⋯
z_ball : ball z (r - dist z c) ⊆ ball c r
w_mem : w ∈ ball c r
integrableHoriz :
  ∀ (a₁ a₂ b : ℝ),
    ↑a₁ + ↑b * I ∈ ball c r → ↑a₂ + ↑b * I ∈ ball c r → IntervalIntegrable (fun x ↦ f (↑x + ↑b * I)) volume a₁ a₂
integrableVert :
  ∀ (a b₁ b₂ : ℝ),
    ↑a + ↑b₁ * I ∈ ball c r → ↑a + ↑b₂ * I ∈ ball c r → IntervalIntegrable (fun y ↦ f (↑a + ↑y * I)) volume b₁ b₂
hI₁ : I₁ = I₃ + I₇
⊢ ↑w.re + ↑z.im * I ∈ ball c r

Tactic:
exact mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)

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

Tactic:
have int3 : ContinuousAt (fun (x : ℝ) ↦ f (x + z.im * I)) z.re :=
    isOpen_Ioo.continuousOn_iff.mp f_contOn 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
int3 : ContinuousAt (fun x ↦ f (↑x + ↑z.im * I)) 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
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: z : ℍ
⊢ Function.Injective fun x ↦ x +ᵥ z

Tactic:
simp [Function.Injective]

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

Goal state before:
pp: c w : ℂ
⊢ poissonKernel c w = re ∘ herglotzRieszKernel c w

Tactic:
by
  ext z
  rw [Function.comp_apply, poissonKernel, herglotzRieszKernel,
    poissonKernel_eq_re_herglotzRieszKernel_aux]

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

Goal state before:
pp: a b : ℝ
ha : a < 0
hb : b < 0
⊢ ∫ (x : ℝ) in a..b, 1 / x = log (b / a)

Tactic:
by simp only [one_div, integral_inv_of_neg ha hb]

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

Goal state before:
pp: b : ℝ
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
rcases lt_trichotomy b 0 with h | h | h

Goal state after:
case inl
b : ℝ
h : b < 0
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

case inr.inl
b : ℝ
h : b = 0
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

case inr.inr
b : ℝ
h : 0 < b
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

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

Tactic:
apply inv_mul_le_one_of_le₀ hu (abs_nonneg R)

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

Goal state before:
pp: n : ℕ
⊢ 0 < ∫ (x : ℝ) in 0..π, sin x ^ n

Tactic:
rcases even_or_odd' n with ⟨k, rfl | rfl⟩ <;>
  simp only [integral_sin_pow_even, integral_sin_pow_odd] <;>
  refine mul_pos (by simp [pi_pos]) (prod_pos fun n _ => div_pos ?_ ?_) <;>
  norm_cast

Goal state after:
case inl.refine_1
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 1

case inl.refine_2
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 2

case inr.refine_1
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 2

case inr.refine_2
k n : ℕ
x✝ : n ∈ Finset.range k
⊢ 0 < 2 * n + 3
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Preorder R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ ((↑g)⁻¹ * m * ↑g).IsElliptic ↔ m.IsElliptic

Tactic:
simpa using isElliptic_conj_iff g⁻¹

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
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:
· exact hlt.trans_le (le_add_of_nonneg_right (dgmem y).1)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
ih :
  ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
    (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det
⊢ (f M.det * f (M k k ^ (Fintype.card m - 1))).det -
      (f (M k k)).det *
        ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
            (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    0

Tactic:
← map_mul,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
ih :
  ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
    (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det
⊢ (f (M.det * M k k ^ (Fintype.card m - 1))).det -
      (f (M k k)).det *
        ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
            (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
⊢ ∏ i ∈ s, f i = 0 ↔ ∃ i ∈ s, f i = 0

Tactic:
refine ⟨fun h0 ↦ ?_, fun ⟨i, hi, hi'⟩ ↦ Finset.prod_eq_zero hi hi'⟩
  have : ∃ᶠ τ in 𝓝[≠] I, ∏ i ∈ s, f i τ = 0 := .of_forall <| by simpa using congrFun h0
  simp only [Finset.prod_eq_zero_iff, Finset.frequently_exists] at this
  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 : ℝ
⊢ rexp (arsinh x) = x + √(1 + x ^ 2)

Tactic:
apply exp_log

Goal state after:
x : ℝ
⊢ 0 < x + √(1 + x ^ 2)
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 x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
⊢ dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c

Tactic:
by
  rcases eq_or_ne R 0 with rfl | hR; · simp [dist_comm, mul_comm]
  have hy' : inversion c R y ≠ c := by simp [*]
  conv in dist _ y => rw [← inversion_inversion c hR y]
  rw [dist_inversion_inversion hx hy', dist_inversion_center]
  field [dist_ne_zero.2 hx]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case refine_1
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) (𝓝 (dist c c))

Tactic:
exact ContinuousAt.tendsto <| by fun_prop

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

Goal state before:
pp: ⊢ ∀ (x : ℝ), 0 < deriv sinh x

Tactic:
by rw [Real.deriv_sinh]; exact cosh_pos

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

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

pp: case refine_2.hf
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ sinh x

pp: case refine_2.hg
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x ↦ x) x

Tactic:
deriv_sinh,

Goal state after:
case refine_2
x : ℝ
hx : 0 < x
⊢ 0 < cosh x - deriv (fun x ↦ x) x

case refine_2.hf
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ sinh x

case refine_2.hg
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x ↦ x) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: ⊢ logDeriv cosh = tanh

Tactic:
by
  ext
  rw [logDeriv, Real.deriv_cosh, Pi.div_apply, Real.tanh_eq_sinh_div_cosh]

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

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

Tactic:
rw [div_div_div_comm, ← norm_mul, div_self h₂, div_one]

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MulAction G X
inst✝³ : CompactlyGeneratedSpace (X × X)
inst✝² : T2Space X
inst✝¹ : DiscreteTopology G
inst✝ : ContinuousConstSMul G X
⊢ ProperlyDiscontinuousSMul G X ↔ ProperSMul G X

Tactic:
have : ContinuousSMul G X := ⟨continuous_prod_of_discrete_left.mpr continuous_const_smul⟩
  simp only [MulAction.properSMul_iff_isCompact_setOfPred_inter_nonempty, isCompact_iff_finite]
  rw [properlyDiscontinuousSMul_iff]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Tendsto (fun x ↦ ↑(f x)) (coclosedCompact X) (𝓝 (OnePoint.map f ∞)) ∧
      Continuous[inst✝¹, instTopologicalSpace] fun x ↦ ↑(f x)) ↔
    Continuous[inst✝¹, inst✝] f ∧ Tendsto f (coclosedCompact X) (coclosedCompact Y)

Tactic:
← comap_coe_nhds_infty,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Tendsto (fun x ↦ ↑(f x)) (comap some (𝓝 ∞)) (𝓝 (OnePoint.map f ∞)) ∧
      Continuous[inst✝¹, instTopologicalSpace] fun x ↦ ↑(f x)) ↔
    Continuous[inst✝¹, inst✝] f ∧ Tendsto f (comap some (𝓝 ∞)) (comap some (𝓝 ∞))
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f₁ f₂ : ℂ → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
⊢ characteristic (f₁ + f₂) ⊤ r ≤ characteristic f₁ ⊤ r + characteristic f₂ ⊤ r + log 2

Tactic:
have h_meromorphic : ∀ a ∈ Finset.univ, Meromorphic (![f₁, f₂] a) := by
    simpa using ⟨h₁f₁, h₁f₂⟩

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f₁ f₂ : ℂ → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
h_meromorphic : ∀ a ∈ Finset.univ, Meromorphic (![f₁, f₂] a)
⊢ characteristic (f₁ + f₂) ⊤ r ≤ characteristic f₁ ⊤ r + characteristic f₂ ⊤ r + log 2
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R β : ℝ
⊢ ∫ (α : ℝ) in Ioc 0 (2 * π), ‖cartanKernel f R α β‖ =
    (2 * ∫ (α : ℝ) in Ioc 0 (2 * π), (cartanKernel f R α β)⁺) - 2 * π * log⁺ ‖f (circleMap 0 R β)‖

Tactic:
let μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))

Goal state after:
f : ℂ → ℂ
R β : ℝ
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
⊢ ∫ (α : ℝ) in Ioc 0 (2 * π), ‖cartanKernel f R α β‖ =
    (2 * ∫ (α : ℝ) in Ioc 0 (2 * π), (cartanKernel f R α β)⁺) - 2 * π * log⁺ ‖f (circleMap 0 R β)‖
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
⊢ Integrable (fun x ↦ ∫ (α : ℝ) in Ioc 0 (2 * π), ‖cartanKernel f R α x‖) (volume.restrict (Ioc 0 (2 * π)))

Tactic:
let μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
⊢ Integrable (fun x ↦ ∫ (α : ℝ) in Ioc 0 (2 * π), ‖cartanKernel f R α x‖) (volume.restrict (Ioc 0 (2 * π)))
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: case pos
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
⊢ circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1 =
    log⁺ ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
rw [← circleAverage_congr_codiscreteWithin
      (eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero hf h) zero_ne_one.symm]

Goal state after:
case pos
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
⊢ circleAverage (fun x ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) 0 1 = log⁺ ‖meromorphicTrailingCoeffAt f 0‖
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
⊢ b ∈ Ioi 0 → a ≤ b → characteristic f ⊤ a ≤ characteristic f ⊤ b

Tactic:
hb

Goal state after:
f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
hb : b ∈ Ioi 0
⊢ a ≤ b → characteristic f ⊤ a ≤ characteristic f ⊤ b
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
⊢ b ∈ Ioi 0 → a ≤ b → logCounting D a ≤ logCounting D b

Tactic:
hb

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
hb : b ∈ Ioi 0
⊢ a ≤ b → logCounting D a ≤ logCounting D b
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case h₁.h.ha
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
z : E
h₁ : ¬D z = 0
a✝³ : ¬a = 0
a✝² : ¬z = 0
a✝¹ : ¬a * ‖z‖⁻¹ = 1
a✝ : ¬a * ‖z‖⁻¹ = -1
this : z ∈ closedBall 0 |a|
⊢ z ∈ closedBall 0 |b|

Tactic:
simp_all only [abs_of_pos ha, mem_closedBall, dist_zero_right, abs_of_pos hb]
        linarith

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

Goal state before:
pp: case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
ha : a ∈ Ioi ‖e‖
b : ℝ
⊢ b ∈ Ioi ‖e‖ → a < b → logCounting (single e 1) a < logCounting (single e 1) b

Tactic:
hb

Goal state after:
case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
ha : a ∈ Ioi ‖e‖
b : ℝ
hb : b ∈ Ioi ‖e‖
⊢ a < b → logCounting (single e 1) a < logCounting (single e 1) b
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case hg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
ha : a ∈ Ioi ‖e‖
b : ℝ
⊢ b ∈ Ioi ‖e‖ → a ≤ b → logCounting (D - single e 1) a ≤ logCounting (D - single e 1) b

Tactic:
hb

Goal state after:
case hg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
ha : a ∈ Ioi ‖e‖
b : ℝ
hb : b ∈ Ioi ‖e‖
⊢ a ≤ b → logCounting (D - single e 1) a ≤ logCounting (D - single e 1) b
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inr.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = t ∩ Icc z y
⊢ eVariationOn f (t ∩ Icc z y) = ENNReal.ofReal (↑l * (y - z))

Tactic:
hft zt yt zy

Goal state after:
case inr.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = t ∩ Icc z y
⊢ ENNReal.ofReal (↑l * (y - z)) = ENNReal.ofReal (↑l * (y - z))
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
hle : D' ≤ D
R₀ : ℝ
hR₀ : ∀ z ∈ t, ‖z‖ ≤ R₀
K : ℝ := ∑ z ∈ t, log ‖z‖
hK : K = ∑ z ∈ t, log ‖z‖
hEq : ∀ᶠ (r : ℝ) in atTop, logCounting D' r = ↑N * log r - K
hFinal : ∀ᶠ (r : ℝ) in atTop, (↑N - C) * log r ≤ K
⊢ False

Tactic:
have hTendsto : Tendsto (fun r ↦ ((N : ℝ) - C) * log r) atTop atTop :=
    tendsto_log_atTop.const_mul_atTop (sub_pos.mpr hCN')

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
hle : D' ≤ D
R₀ : ℝ
hR₀ : ∀ z ∈ t, ‖z‖ ≤ R₀
K : ℝ := ∑ z ∈ t, log ‖z‖
hK : K = ∑ z ∈ t, log ‖z‖
hEq : ∀ᶠ (r : ℝ) in atTop, logCounting D' r = ↑N * log r - K
hFinal : ∀ᶠ (r : ℝ) in atTop, (↑N - C) * log r ≤ K
hTendsto : Tendsto (fun r ↦ (↑N - C) * log r) atTop atTop
⊢ False
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mpr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
⊢ eVariationOn f s = 0 → ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0

Tactic:
rintro h x _ y _
    simpa [h] using eVariationOn.mono (s := s) f inter_subset_left

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l l' : ℝ≥0
hl' : l' ≠ 0
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasConstantSpeedOnWith (f ∘ φ) s l
hf : HasConstantSpeedOnWith f (φ '' s) l'
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ φ y - φ x = (y - x) * ↑l / ↑l'

Tactic:
eq_div_iff (NNReal.coe_ne_zero.mpr hl')

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l l' : ℝ≥0
hl' : l' ≠ 0
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasConstantSpeedOnWith (f ∘ φ) s l
hf : HasConstantSpeedOnWith f (φ '' s) l'
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ (φ y - φ x) * ↑l' = (y - x) * ↑l
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: case refine_2
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this✝ : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
z : ι
⊢ (if h : z = x then y else f' ⟨z, h⟩) ∈ t z

Tactic:
split_ifs with hz

Goal state after:
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this✝ : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
z : ι
hz : z = x
⊢ y ∈ t z

case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this✝ : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
z : ι
hz : ¬z = x
⊢ f' ⟨z, hz⟩ ∈ t z
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P ≃ᵃ[R] P'
⊢ Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z

Tactic:
by
  have : Function.Injective f.toAffineMap := f.injective
  -- `refine` or `exact` are very slow, `apply` is fast. Please check before golfing.
  apply this.wbtw_map_iff

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : PartialOrder R
x : R
⊢ Wbtw R 0 x 1 ↔ x ∈ Set.Icc 0 1

Tactic:
rw [Wbtw, affineSegment, Set.mem_image]
  simp_rw [lineMap_apply_ring]
  simp

Goal state after: