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

Goal state before:
pp: 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
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
e1 : IsPreconnected (ball 0 r)
e2 : w ∈ sphere 0 1
⊢ ∀ t ∈ ball 0 r, gray w t = g z₀

Tactic:
specialize h1 w e2

Goal state after:
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}
h : ∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
z : E
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
h1 : AnalyticOnNhd ℂ (gray w) (ball 0 r)
e1 : IsPreconnected (ball 0 r)
e2 : w ∈ sphere 0 1
⊢ ∀ t ∈ ball 0 r, gray w t = g z₀
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * ↑π * I / ↑h)) z
diff_ne : q * (2 * ↑π * I / ↑h) ≠ 0
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * ↑π * I / ↑h)) z qdiff diff_ne
diff_L : DifferentiableAt ℂ L q
hL : 𝕢 h ∘ L =ᶠ[𝓝 q] id
hF : cuspFunction h f ∘ 𝕢 h ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id
this : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Tactic:
rw [this] at hF

Goal state after:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * ↑π * I / ↑h)) z
diff_ne : q * (2 * ↑π * I / ↑h) ≠ 0
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * ↑π * I / ↑h)) z qdiff diff_ne
diff_L : DifferentiableAt ℂ L q
hL : 𝕢 h ∘ L =ᶠ[𝓝 q] id
hF : f ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id
this : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)
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
hzP : ¬eval z P = 0
⊢ ∑ x ∈ s, weight x • (z - x) = (starRingEnd ℂ) (∑ x ∈ s, rootMultiplicity x P • (1 / (z - x)))

Tactic:
simp only [map_sum, weight, derivRootWeight, if_neg hzP]
      refine Finset.sum_congr rfl fun x hx ↦ ?_
      have : z - x ≠ 0 := by
        rw [sub_ne_zero]
        rintro rfl
        simp_all [s]
      simp [← Complex.conj_mul', field]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
⊢ ∃ r' < r, 0 < r' ∧ z ∈ Metric.ball c r'

Tactic:
obtain ⟨r', h₁, h₂⟩ := exists_between (Metric.mem_ball'.mp hz)
    exact ⟨r', h₂, Metric.pos_of_mem_ball h₁, Metric.mem_ball'.mpr h₁⟩

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

Goal state before:
pp: case inr.refine_2
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : ¬0 ∉ U
a : ℂ
ha : a ∉ U
f : ℂ → ℂ
hf_inj : Injective f
hf_dense : ¬Dense (f '' (-a +ᵥ U))
hdf : ∀ z ∈ -a +ᵥ U, deriv f z ≠ 0
z : ℂ
hz : z ∈ U
⊢ deriv (f ∘ fun x ↦ -a + x) z ≠ 0

Tactic:
simpa [Function.comp_def, deriv_comp_const_add] using hdf (-a + z) (mapsTo_image _ _ hz)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
⊢ sqrt a = ↑√((‖a‖ + re a) / 2) + (if 0 ≤ im a then 1 else -1) * ↑√((‖a‖ - re a) / 2) * I

Tactic:
rw [sqrt, Complex.sqrt_eq_real_add_ite]

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
⊢ (map ℂ 𝕜)
      (↑√((‖(map 𝕜 ℂ) a‖ + ((map 𝕜 ℂ) a).re) / 2) +
        (if 0 ≤ ((map 𝕜 ℂ) a).im then 1 else -1) * ↑√((‖(map 𝕜 ℂ) a‖ - ((map 𝕜 ℂ) a).re) / 2) * Complex.I) =
    ↑√((‖a‖ + re a) / 2) + (if 0 ≤ im a then 1 else -1) * ↑√((‖a‖ - re a) / 2) * I
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) +
        ↑(ENat.map Nat.cast (analyticOrderAt f c)).untop₀ * Real.log R +
      Real.log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖

Tactic:
(h₁f c (by simp)).analyticOrderAt_eq_zero.mpr h₂f,

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) +
        ↑(ENat.map Nat.cast 0).untop₀ * Real.log R +
      Real.log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
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
⊢ ↑(∑ᶠ (u : ℂ), (divisor f (closedBall c |r|)) u) ≤ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u)

Tactic:
exact map_finsum (Int.castRingHom ℝ)
      ((divisor _ _).finiteSupport <| isCompact_closedBall ..) |>.le

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
F : Type u_3
inst✝¹ : Field F
inst✝ : IsAlgClosed F
h : ¬Nonempty n
⊢ IsEmpty n

Tactic:
simpa using h

Goal state after:
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
⊢ ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) + Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0)) ∨
      ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0)) ↔
    z = fixedPt g hell

Tactic:
rw [or_iff_left]

Goal state after:
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
⊢ ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) + Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0)) ↔ z = fixedPt g hell

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
⊢ ¬↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0))
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ (∃ a n, m = (scalar (Fin 2)) a + n ∧ n ≠ 0 ∧ n ^ 2 = 0) → m.IsParabolic

Tactic:
· rintro ⟨a, n, hm, hn0, hnsq⟩
    constructor
    · refine fun ⟨b, hb⟩ ↦ hn0 ?_
      rw [← sub_eq_iff_eq_add'] at hm
      simpa only [← hm, ← hb, ← map_sub, ← map_pow, ← map_zero (scalar (Fin 2)), scalar_inj,
        sq_eq_zero_iff] using hnsq
    · suffices scalar (Fin 2) (m.discr / 4) = 0 by
        rw [← map_zero (scalar (Fin 2)), scalar_inj, div_eq_zero_iff] at this
        have : (4 : K) ≠ 0 := by simpa [show (4 : K) = 2 ^ 2 by norm_num] using NeZero.ne _
        tauto
      rw [← sub_scalar_sq_eq_discr, hm, trace_add, scalar_apply, trace_diagonal]
      simp [mul_div_cancel_left₀ _ (NeZero.ne (2 : K)),
        (Matrix.isNilpotent_trace_of_isNilpotent ⟨2, hnsq⟩).eq_zero, hnsq]

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

Goal state before:
pp: h : IsCompact univ
this : IsCompact (Complex.im ⁻¹' Ioi 0)
⊢ False

Tactic:
simpa [closure_preimage_im] using! congr(0 ∈ $this.isClosed.closure_eq)

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

Goal state before:
pp: u : ℝˣ
z : ℍ
⊢ (GeneralLinearGroup.scalar (Fin 2)) u • z = z

Tactic:
rw [glPos_smul_def]
  · simp
  · simp [sq_pos_iff]

Goal state after:
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: case «0»
z : ℂ
i : Fin 2
⊢ ![z.re * re 1 - z.im * im 1, z.re * im 1 + z.im * re 1] i = ![![z.re, -z.im], ![z.im, z.re]] i 0

Tactic:
simp only [one_re, mul_one, one_im, mul_zero,
      sub_zero, zero_add]

Goal state after:
case «0»
z : ℂ
i : Fin 2
⊢ ![z.re, z.im] i = ![![z.re, -z.im], ![z.im, z.re]] i 0
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
⊢ M.det * M k k ^ (Fintype.card m - 1) = M k k * ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det

Tactic:
by
  trans (M * auxMat M k).det
  · simp [det_mul, (auxMat_blockTriangular M k).det_fintype,
      auxMat_toSquareBlock_ne, auxMat_toSquareBlock_eq]
  rw [(mul_auxMat_blockTriangular M k).det_fintype, Fintype.prod_Prop, mul_auxMat_toSquareBlock_eq]
  simp_rw [det_smul_of_tower, eq_iff_iff, iff_true, Fintype.card_unique,
    pow_one, det_one, smul_eq_mul, mul_one]
  -- `Decidable (P = Q)` diamond induced by `Prop.linearOrder`, which is classical, when `P` and `Q`
  -- are themselves decidable.
  convert! rfl

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

Goal state before:
pp: x : ℝ
⊢ (rexp (arsinh x) - rexp (-arsinh x)) / 2 = x

Tactic:
← arsinh_neg,

Goal state after:
x : ℝ
⊢ (rexp (arsinh x) - rexp (arsinh (-x))) / 2 = x
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : HasProp P X
⊢ ∀ {A B : CompHausLike P} (f : A ⟶ B) [IsIso ((forget (CompHausLike P)).map f)], IsIso f

Tactic:
by intro A B f hf; rw [isIso_iff_bijective] at hf; exact isIso_of_bijective _ hf

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

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ ↑(Ultrafilter.map f b) ≤ map (Ultrafilter.extend f) ↑b'

Tactic:
change _ ≤ map (Ultrafilter.extend f ∘ pure) ↑b

Goal state after:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ ↑(Ultrafilter.map f b) ≤ map (Ultrafilter.extend f ∘ pure) ↑b
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
⊢ IsClosed[instTopologicalSpace] s ↔ IsClosed[inst✝] (some ⁻¹' s)

Tactic:
by
  have : ∞ ∉ sᶜ := fun H => H h
  rw [← isOpen_compl_iff, isOpen_iff_of_notMem this, ← isOpen_compl_iff, preimage_compl]

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
H : Type u_3
inst✝³ : Group H
inst✝² : MulAction H X
inst✝¹ : TopologicalSpace H
inst✝ : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding ⇑f
f_compat : ∀ (h : H) (x : X), f h • x = h • x
h : IsProperMap (Prod.map ⇑f fun x ↦ x)
⊢ (fun hx ↦ (hx.1 • hx.2, hx.2)) = fun hx ↦ (f hx.1 • hx.2, hx.2)

Tactic:
simp [f_compat]

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⇑(continuousMapMkNat u p hup) ∘ ULift.down
⊢ Tendsto OnePoint.some atTop (𝓝 ∞)

Tactic:
rw [← Nat.cofinite_eq_atTop, ← cocompact_eq_cofinite, ← coclosedCompact_eq_cocompact]

Goal state after:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⇑(continuousMapMkNat u p hup) ∘ ULift.down
⊢ Tendsto OnePoint.some (coclosedCompact ℕ) (𝓝 ∞)
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⇑(continuousMapMkNat u p hup) ∘ ULift.down
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → g { down := ↑b } ∈ s

Tactic:
exact ⟨0, fun b _ ↦ hu b⟩

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ circleAverage (fun x ↦ log⁺ ‖∑ c ∈ s, f c x‖) 0 r ≤ circleAverage (fun x ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card) 0 r

Tactic:
apply circleAverage_mono

Goal state after:
case hf₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ CircleIntegrable (fun x ↦ log⁺ ‖∑ c ∈ s, f c x‖) 0 r

case hf₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ CircleIntegrable (fun x ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card) 0 r

case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ ∀ x ∈ sphere 0 |r|, log⁺ ‖∑ c ∈ s, f c x‖ ≤ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card
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✝ : WeaklyLocallyCompactSpace X
⊢ CompactlyGeneratedSpace X

Tactic:
by
  refine compactlyGeneratedSpace_of_isClosed_of_t2 fun s h ↦ ?_
  rw [isClosed_iff_forall_filter]
  intro x ℱ hℱ₁ hℱ₂ hℱ₃
  rcases exists_compact_mem_nhds x with ⟨K, hK, K_mem⟩
  exact Set.mem_of_mem_inter_left <| isClosed_iff_forall_filter.1 (h _ hK) x ℱ hℱ₁
    (Filter.inf_principal ▸ le_inf hℱ₂ (le_trans hℱ₃ <| Filter.le_principal_iff.2 K_mem)) hℱ₃

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

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ circleAverage (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 r ≤ circleAverage (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r

Tactic:
apply circleAverage_mono

Goal state after:
case hf₁
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 r

case hf₂
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r

case h
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ ∀ x ∈ sphere 0 |r|, log⁺ (‖f₁ x‖ * ‖f₂ x‖) ≤ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
h_bound_nonneg : 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
⊢ ∫ (α : ℝ) in Ioc 0 (2 * π), (cartanKernel f R α β)⁺ ≤ ∫ (x : ℝ) in Ioc 0 (2 * π), log⁺ ‖f (circleMap 0 R β)‖ + log 2

Tactic:
refine integral_mono_of_nonneg (.of_forall (by simp [posPart])) (integrable_const _)
        (.of_forall ?_)

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
h_bound_nonneg : 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
⊢ ∀ (x : ℝ), (fun α ↦ (cartanKernel f R α β)⁺) x ≤ (fun x ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) x
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case h₁
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
⊢ ∑ᶠ (z : E), ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹) ≤ ∑ᶠ (z : E), ↑(((toClosedBall b) D) z) * log (b * ‖z‖⁻¹)

Tactic:
let s := (toClosedBall b D).support
    have hs : s.Finite := (toClosedBall b D).finiteSupport (isCompact_closedBall 0 |b|)
    repeat rw [finsum_eq_sum_of_support_subset (s := hs.toFinset)]
    · gcongr 1 with z hz
      by_cases h₂z : z = 0
      · simp [h₂z]
      · have := (toClosedBall_support_subset_closedBall D (hs.mem_toFinset.1 hz))
        rw [toClosedBall_eval_within _ this]
        by_cases h₃z : z ∈ closedBall 0 |a|
        · rw [toClosedBall_eval_within _ h₃z]
          gcongr
          exact Int.cast_nonneg (hD z)
        · simp only [h₃z, not_false_eq_true, apply_eq_zero_of_notMem, Int.cast_zero, zero_mul,
            ge_iff_le]
          apply mul_nonneg (Int.cast_nonneg (hD z)) (log_nonneg _)
          apply (le_mul_inv_iff₀ (norm_pos_iff.mpr h₂z)).2
          simp_all [abs_of_pos hb]
    · intro z
      aesop
    · intro z
      simp only [support_mul, mem_inter_iff, mem_support, ne_eq, Int.cast_eq_zero, log_eq_zero,
        mul_eq_zero, inv_eq_zero, norm_eq_zero, not_or, Finite.coe_toFinset, and_imp, s]
      intro h₁ _ _ _ _
      have : z ∈ closedBall 0 |a| := mem_of_indicator_ne_zero h₁
      rw [toClosedBall_eval_within _ this] at h₁
      rwa [toClosedBall_eval_within]
      · 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: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ locallyFinsuppWithin.logCounting (divisor f₁ univ + divisor f₂ univ)⁺ r ≤
    locallyFinsuppWithin.logCounting ((divisor (fun x ↦ f₁ x) univ)⁺ + (divisor (fun x ↦ f₂ x) univ)⁺) r

Tactic:
apply locallyFinsuppWithin.logCounting_le _ hr

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ (divisor f₁ univ + divisor f₂ univ)⁺ ≤ (divisor (fun x ↦ f₁ x) univ)⁺ + (divisor (fun x ↦ f₂ x) univ)⁺
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ locallyFinsuppWithin.logCounting (divisor f₁ univ + divisor f₂ univ)⁻ r ≤
    locallyFinsuppWithin.logCounting ((divisor f₁ univ)⁻ + (divisor f₂ univ)⁻) r

Tactic:
apply locallyFinsuppWithin.logCounting_le _ hr

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ (divisor f₁ univ + divisor f₂ univ)⁻ ≤ (divisor f₁ univ)⁻ + (divisor f₂ univ)⁻
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl.inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
xy : x ≤ y
yz : y ≤ z
⊢ HasConstantSpeedOnWith f (Icc x z) l

Tactic:
rw [← Set.Icc_union_Icc_eq_Icc xy yz]
      exact hfs.union hft (isGreatest_Icc xy) (isLeast_Icc yz)

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
⊢ ((Pairwise (Sbtw R p) l ∧ Triplewise (Sbtw R) l) ∧ ¬∃ x, p :: l = [x, x]) ↔
    Pairwise (Sbtw R p) l ∧ List.Sbtw R l ∧ l ≠ [p]

Tactic:
simp only [cons.injEq, exists_eq_left', and_assoc, and_congr_right_iff, ne_eq, and_congr_left_iff]

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
⊢ Pairwise (Sbtw R p) l → ¬l = [p] → (Triplewise (Sbtw R) l ↔ List.Sbtw R l)
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case refine_2.refine_2.cons.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
l' : List R
hl's : l'.SortedLE
head head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
hp : (∀ a' ∈ head2 :: tail, head ≠ a') ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head2 :: tail)
hl'l :
  map (⇑(lineMap ((head :: head2 :: tail).head hl) ((head :: head2 :: tail).getLast hl))) l' = head :: head2 :: tail
⊢ head ≠ (head :: head2 :: tail).getLast hl

Tactic:
refine hp.1 ((head :: head2 :: tail).getLast hl) ?_

Goal state after:
case refine_2.refine_2.cons.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
l' : List R
hl's : l'.SortedLE
head head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
hp : (∀ a' ∈ head2 :: tail, head ≠ a') ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head2 :: tail)
hl'l :
  map (⇑(lineMap ((head :: head2 :: tail).head hl) ((head :: head2 :: tail).getLast hl))) l' = head :: head2 :: tail
⊢ (head :: head2 :: tail).getLast hl ∈ head2 :: tail
Module: Mathlib.Analysis.Convex.Between

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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
hxz : x ≠ z
t : R
ht : t ∈ Set.Ioo 0 1
⊢ t • (z -ᵥ x) + 0 ≠ 0 ∧ (t + -1) • (z -ᵥ x) ≠ 0

Tactic:
← sub_eq_add_neg

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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x z : P
hxz : x ≠ z
t : R
ht : t ∈ Set.Ioo 0 1
⊢ t • (z -ᵥ x) + 0 ≠ 0 ∧ (t - 1) • (z -ᵥ x) ≠ 0