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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfd : DiffContOnCl ℂ f {z | 0 < z.re}
hgd : DiffContOnCl ℂ g {z | 0 < z.re}
hfexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hgexp : ∃ c < 2, ∃ B, g =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x - g ↑x‖
hfim : ∃ C, ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hgim : ∃ C, ∀ (x : ℝ), ‖g (↑x * I)‖ ≤ C
⊢ EqOn (f - g) 0 {z | 0 ≤ z.re}

Tactic:
refine eq_zero_on_right_half_plane_of_superexponential_decay (hfd.sub hgd) ?_ hre ?_

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfd : DiffContOnCl ℂ f {z | 0 < z.re}
hgd : DiffContOnCl ℂ g {z | 0 < z.re}
hfexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hgexp : ∃ c < 2, ∃ B, g =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x - g ↑x‖
hfim : ∃ C, ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hgim : ∃ C, ∀ (x : ℝ), ‖g (↑x * I)‖ ≤ C
⊢ ∃ c < 2, ∃ B, (f - g) =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfd : DiffContOnCl ℂ f {z | 0 < z.re}
hgd : DiffContOnCl ℂ g {z | 0 < z.re}
hfexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hgexp : ∃ c < 2, ∃ B, g =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x - g ↑x‖
hfim : ∃ C, ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hgim : ∃ C, ∀ (x : ℝ), ‖g (↑x * I)‖ ≤ C
⊢ ∃ C, ∀ (x : ℝ), ‖(f - g) (↑x * I)‖ ≤ C
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:

Tactic:
|((circleMap 0 r θ + w) / (circleMap 0 r θ - w)).re|
     _ ≤ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖ := by grw [Complex.abs_re_le_norm, norm_div]
     _ ≤ (r + ‖w‖) / (r - ‖w‖) := by
        grw [norm_add_le, ← norm_sub_norm_le]
        all_goals simp only [norm_circleMap_zero, abs_of_pos hr]; grind
      _ ≤ (R + ‖w‖) / (r₀ - ‖w‖) := by gcongr

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

Goal state before:
pp: P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
this : ∑ x ∈ s, weight x • (z - x) = 0
⊢ (s.centerMass weight fun x ↦ z - x) + s.centerMass weight id = s.centerMass weight id

Tactic:
by
      simp only [add_eq_right, Finset.centerMass, this, smul_zero]

Goal state after:
Module: Mathlib.Order.Interval.Set.IsoIoo

Goal state before:
pp: case refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ StrictMono (codRestrict (fun x ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)

Tactic:
refine (strictMono_of_odd_strictMonoOn_nonneg ?_ ?_).codRestrict _
    · intro x
      simp only [abs_neg, neg_div]
    · rintro x (hx : 0 ≤ x) y (hy : 0 ≤ y) hxy
      simp [abs_of_nonneg, mul_add, mul_comm x y, div_lt_div_iff₀, hx.trans_lt (lt_one_add _),
        hy.trans_lt (lt_one_add _), *]

Goal state after:
Module: Mathlib.Topology.UrysohnsBounded

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
⊢ a ≤ (BoundedContinuousFunction.const X a + (b - a) • f) x

Tactic:
dsimp

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
⊢ a ≤ a + (b - a) * f x
Module: Mathlib.Topology.UrysohnsBounded

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
⊢ (BoundedContinuousFunction.const X a + (b - a) • f) x ≤ b

Tactic:
dsimp

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
⊢ a + (b - a) * f x ≤ b
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Goal state before:
pp: case mk
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
hR : ∀ (r : Rˣ), ∃ k, k ^ Fintype.card n = r
g : GL n R
⊢ ∃ a, toPGL a = mk g

Tactic:
| mk g =>

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

Goal state before:
pp: case mk
n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
S : Type u_4
T : Type u_5
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g✝ : S →+* T
g : GL n R
⊢ (map (g✝.comp f)) (mk g) = ((map g✝).comp (map f)) (mk g)

Tactic:
| mk g =>

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ (num g z / denom g z).im = ↑(GeneralLinearGroup.det g) * z.im / Complex.normSq (denom g z)

Tactic:
simp only [num, denom, Complex.div_im, Complex.add_im, Complex.mul_im, Complex.ofReal_re,
    Complex.ofReal_im, zero_mul, add_zero, Complex.add_re, Complex.mul_re, sub_zero, ← sub_div,
    GeneralLinearGroup.val_det_apply, g.1.det_fin_two]
  ring

Goal state after:
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: z : ℂ
⊢ ((leftMulMatrix basisOneI) z).trace = 2 * z.re

Tactic:
Algebra.leftMulMatrix_complex,

Goal state after:
z : ℂ
⊢ !![z.re, -z.im; z.im, z.re].trace = 2 * z.re
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: z : ℂ
⊢ ((leftMulMatrix basisOneI) z).det = normSq z

Tactic:
Algebra.leftMulMatrix_complex,

Goal state after:
z : ℂ
⊢ !![z.re, -z.im; z.im, z.re].det = normSq z
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.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 →ᵇ ℝ
hgf : ⇑g ∘ e = ⇑f
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})
⊢ ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f

Tactic:
rcases exists_bounded_mem_Icc_of_closed_of_le
      (he.isClosed_range.union <| isClosed_Iic.preimage g.continuous)
      (isClosed_singleton.preimage g.continuous) hd (sub_nonneg.2 hcb.le) with
    ⟨dg, dg0, dgb, dgmem⟩

Goal state after:
case inr.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 →ᵇ ℝ
hgf : ⇑g ∘ e = ⇑f
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)
⊢ ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: case left
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, instTopologicalSpaceMatrix] fun x ↦ !![1, x; 0, 1]

Tactic:
· refine continuous_matrix fun i j ↦ ?_
    fin_cases i <;> fin_cases j <;> simp [continuous_const, continuous_neg, continuous_id']

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: case right
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, instTopologicalSpaceMatrix] fun x ↦ !![1, -x; 0, 1]

Tactic:
· refine continuous_matrix fun i j ↦ ?_
    fin_cases i <;> fin_cases j <;> simp [continuous_const, continuous_neg, continuous_id']

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

Goal state before:
pp: z w : ℍ
r : ℝ
g : SL(2, ℝ)
⊢ Isometry fun x ↦ g • x

Tactic:
have h₀ : Isometry (fun z => ModularGroup.S • z : ℍ → ℍ) :=
      Isometry.of_dist_eq fun y₁ y₂ => by
        have h₁ : 0 ≤ im y₁ * im y₂ := by positivity
        have h₂ : ‖(y₁ * y₂ : ℂ)‖ ≠ 0 := by simp [y₁.ne_zero, y₂.ne_zero]
        simp_rw [modular_S_smul, inv_neg, dist_eq, dist_neg_neg,
          dist_inv_inv₀ y₁.ne_zero y₂.ne_zero, mk_im, neg_im, inv_im, coe_im, neg_div, neg_neg,
          div_mul_div_comm, ← normSq_mul, Real.sqrt_div h₁, ← norm_def, mul_div (2 : ℝ)]
        rw [div_div_div_comm, ← norm_mul, div_self h₂, div_one]

Goal state after:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z ↦ ModularGroup.S • z
⊢ Isometry fun x ↦ g • x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case inr
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
g : SL(2, ℝ)
hg : g • I ∈ K
hδK : δ ≤ 1 / Complex.normSq (denom ((Matrix.SpecialLinearGroup.mapGL ℝ) g) ↑I)
⊢ ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ 1 / δ

Tactic:
le_div_iff₀ (normSq_denom_pos (Matrix.SpecialLinearGroup.mapGL ℝ g) (show I.im ≠ 0 by simp)),

Goal state after:
case inr
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
g : SL(2, ℝ)
hg : g • I ∈ K
hδK : δ * Complex.normSq (denom ((Matrix.SpecialLinearGroup.mapGL ℝ) g) ↑I) ≤ 1
⊢ ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ 1 / δ
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)
K : Set X
hK : IsCompact K
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)

Tactic:
← Subtype.preimage_coe_inter_self

Goal state after:
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)
K : Set X
hK : IsCompact K
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' (s ∩ K))
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case e_a
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
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

Tactic:
← Finset.sum_add_distrib,

Goal state after:
case e_a
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
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h✝ : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : θ ∈ sphere 0 |r|
h : 0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
⊢ |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ log⁺ ‖a₀‖ + log 2

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h✝ : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : θ ∈ sphere 0 |r|
h : ¬0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
⊢ |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ log⁺ ‖a₀‖ + log 2

Tactic:
· simpa [abs_of_nonneg h, sub_le_iff_le_add, add_comm (log⁺ ‖a₀‖ + log 2), ← add_assoc]
        using (posLog_norm_add_le (f θ - a₀) a₀)

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h✝ : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : θ ∈ sphere 0 |r|
h : ¬0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
⊢ |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ log⁺ ‖a₀‖ + log 2
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
⊢ a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ →
    log ‖meromorphicTrailingCoeffAt f 0 - a‖ = log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖

Tactic:
ha_ne

Goal state after:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ log ‖meromorphicTrailingCoeffAt f 0 - a‖ = log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
⊢ (fun x ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) =ᶠ[codiscreteWithin (sphere 0 |1|)] fun a ↦
    log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖

Tactic:
filter_upwards [self_mem_codiscreteWithin (sphere 0 |1|), compl_singleton_mem_codiscreteWithin
    (meromorphicTrailingCoeffAt f 0)] with a ha_sphere ha_ne

Goal state after:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ log ‖meromorphicTrailingCoeffAt f 0 - a‖ = log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case e_a
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
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ i ∈ h₁s.toFinset, ↑(((toClosedBall r) D₁) i) * log (r * ‖i‖⁻¹) +
      ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

Tactic:
← Finset.sum_add_distrib,

Goal state after:
case e_a
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
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ i ∈ h₁s.toFinset, ↑(((toClosedBall r) D₁) i) * log (r * ‖i‖⁻¹) +
      ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
⊢ (fun x ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) =ᶠ[codiscreteWithin (sphere 0 |1|)] fun a ↦
    log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖

Tactic:
filter_upwards [self_mem_codiscreteWithin (sphere 0 |1|), compl_singleton_mem_codiscreteWithin
    (meromorphicTrailingCoeffAt f 0)] with a ha_sphere ha_ne
  congr
  rw [h₁.meromorphicTrailingCoeffAt_fun_sub_eq_sub
    (by fun_prop), meromorphicTrailingCoeffAt_const, sub_eq_add_neg]
  · simp only [meromorphicOrderAt_const]
    aesop
  · simp only [meromorphicTrailingCoeffAt_const, ne_eq]
    grind

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

Goal state before:
pp: case e_a
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
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ i ∈ h₁s.toFinset, ↑(((toClosedBall r) D₁) i) * log (r * ‖i‖⁻¹) +
      ∑ i ∈ h₁s.toFinset, ↑(((toClosedBall r) D₂) i) * log (r * ‖i‖⁻¹)

Tactic:
← Finset.sum_add_distrib,

Goal state after:
case e_a
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
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ x ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) x) * log (r * ‖x‖⁻¹) + ↑(((toClosedBall r) D₂) x) * log (r * ‖x‖⁻¹))
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
e : WithTop E
⊢ 0 ≤ᶠ[atTop] logCounting f e

Tactic:
filter_upwards [eventually_ge_atTop 1] using fun _ hr ↦ by simp [logCounting_nonneg hr]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ logCounting (f₁ + f₂) ⊤ ≤ᶠ[atTop] logCounting f₁ ⊤ + logCounting f₂ ⊤

Tactic:
by
  filter_upwards [eventually_ge_atTop 1] using fun _ hr ↦ logCounting_add_top_le h₁f₁ h₁f₂ hr

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: case cons
α : Type u_1
l : List α
p q : α → α → α → Prop
h : ∀ {a b c : α}, p a b c → q a b c
a✝ : α
l✝ : List α
head : Pairwise (p a✝) l✝
tail : Triplewise p l✝
ih : Triplewise q l✝
⊢ Triplewise q (a✝ :: l✝)

Tactic:
| cons head tail ih =>

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: case cons
α : Type u_1
l : List α
p : α → α → α → Prop
head : α
tail : List α
ih : Triplewise p tail ↔ ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]
⊢ Triplewise p (head :: tail) ↔
    ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < (head :: tail).length),
      p (head :: tail)[i] (head :: tail)[j] (head :: tail)[k]

Tactic:
| cons head tail ih =>

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

Goal state before:
pp: case cons
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
⊢ List.Wbtw R (head :: tail) ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail) ↔
    Triplewise (Sbtw R) (head :: tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]

Tactic:
| cons head tail ih =>

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
p : P
l : List P
hp : Pairwise (Sbtw R p) l
hne : ¬l = [p]
⊢ Triplewise (Sbtw R) l → ∀ (a : P), l ≠ [a, a]

Tactic:
← not_exists

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
p : P
l : List P
hp : Pairwise (Sbtw R p) l
hne : ¬l = [p]
⊢ Triplewise (Sbtw R) l → ¬∃ x, l = [x, x]
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: 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'
z : ι
hz : ¬z = x
hfr : f' ⟨z, hz⟩ ∈ t' ⟨z, hz⟩
⊢ f' ⟨z, hz⟩ ∈ t z

Tactic:
mem_erase

Goal state after:
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'
z : ι
hz : ¬z = x
hfr : f' ⟨z, hz⟩ ≠ y ∧ f' ⟨z, hz⟩ ∈ t ↑⟨z, hz⟩
⊢ f' ⟨z, hz⟩ ∈ t z
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case refine_2.cons
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
head : P
tail : List P
ih :
  ∀ (hl : tail ≠ []),
    List.Wbtw R tail →
      ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (tail.head hl) (tail.getLast hl))) l' = tail
hl : head :: tail ≠ []
h : List.Wbtw R (head :: tail)
⊢ ∃ l',
    (∀ a ∈ l', 0 ≤ a) ∧
      l'.SortedLE ∧ map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl))) l' = head :: tail

Tactic:
| cons head tail ih =>

Goal state after: