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

Goal state before:
pp: case pos
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ circleAverage (fun x ↦ log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * log (R * ‖c - u‖⁻¹) +
        ↑((divisor f (closedBall c |R|)) c) * log R +
      log ‖meromorphicTrailingCoeffAt f c‖

Tactic:
calc circleAverage (log ‖f ·‖) c R
    _ = circleAverage ((∑ᶠ u, (divisor f CB u * log ‖· - u‖)) + (log ‖g ·‖)) c R := by
      have h₄g := extract_zeros_poles_log h₂g h₃g
      rw [circleAverage_congr_codiscreteWithin (codiscreteWithin_mono sphere_subset_closedBall h₄g)
        hR]
    _ = circleAverage (∑ᶠ u, (divisor f CB u * log ‖· - u‖)) c R + circleAverage (log ‖g ·‖) c R :=
      circleAverage_add (circleIntegrable_log_norm_factorizedRational (divisor f CB))
        ((h₁g.mono sphere_subset_closedBall).meromorphicOn.circleIntegrable_log_norm)
    _ = ∑ᶠ u, divisor f CB u * log R + log ‖g c‖ := by
      simp only [circleAverage_log_norm_factorizedRational, add_right_inj]
      rw [h₁g.circleAverage_log_norm_of_ne_zero]
      exact fun u hu ↦ h₂g ⟨u, hu⟩
    _ = ∑ᶠ u, divisor f CB u * log R
      + (log ‖meromorphicTrailingCoeffAt f c‖ - ∑ᶠ u, divisor f CB u * log ‖c - u‖) := by
      have t₀ : c ∈ CB := by simp [CB]
      have t₁ : AccPt c (𝓟 CB) := by
        apply accPt_iff_frequently_nhdsNE.mpr
        apply compl_notMem
        apply mem_nhdsWithin.mpr
        use ball c |R|
        simpa [hR] using! fun _ ⟨h, _⟩ ↦ ball_subset_closedBall h
      simp [MeromorphicOn.log_norm_meromorphicTrailingCoeffAt_extract_zeros_poles h₃f t₀ t₁
        (h₁f c t₀) (h₁g c t₀) (h₂g ⟨c, t₀⟩) h₃g]
    _ = ∑ᶠ u, divisor f CB u * log R - ∑ᶠ u, divisor f CB u * log ‖c - u‖
      + log ‖meromorphicTrailingCoeffAt f c‖ := by
      ring
    _ = (∑ᶠ u, divisor f CB u * (log R - log ‖c - u‖)) + log ‖meromorphicTrailingCoeffAt f c‖ := by
      rw [← finsum_sub_distrib]
      · simp_rw [← mul_sub]
      repeat apply h₃f.subset (fun _ ↦ (by simp_all))
    _ = ∑ᶠ u, divisor f CB u * log (R * ‖c - u‖⁻¹) + divisor f CB c * log R
      + log ‖meromorphicTrailingCoeffAt f c‖ := by
      rw [countingFunction_finsum_eq_finsum_add hR h₃f]

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
g : GL n R
⊢ g ∈ mk.ker ↔ g ∈ Subgroup.center (GL n R)

Tactic:
ker_mk

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : GL n R
⊢ g ∈ Subgroup.center (GL n R) ↔ g ∈ Subgroup.center (GL n R)
Module: Mathlib.Topology.TietzeExtension

Goal state before:

Tactic:
dist (g (e x)) (f x) ≤ |g (e x)| + |f x| := dist_le_norm_add_norm _ _
          _ ≤ ‖f‖ / 3 + ‖f‖ / 3 := (add_le_add (abs_le.2 <| hgf _) (abs_le.2 ⟨hle₁, hle₂⟩))
          _ = 2 / 3 * ‖f‖ := by linarith

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]

Goal state after:
g : GL (Fin 2) ℝ
z : ℂ
⊢ (↑g 0 0 * z.im * (↑g 1 0 * z.re + ↑g 1 1) - (↑g 0 0 * z.re + ↑g 0 1) * (↑g 1 0 * z.im)) /
      Complex.normSq (↑(↑g 1 0) * z + ↑(↑g 1 1)) =
    (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) * z.im / Complex.normSq (↑(↑g 1 0) * z + ↑(↑g 1 1))
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : (-m).IsParabolic
⊢ m.IsParabolic

Tactic:
simpa using h.neg

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

Goal state before:
pp: g : GL (Fin 2) ℝ
⊢ Continuous fun x ↦ (σ g) (num g ↑x / denom g ↑x)

Tactic:
UpperHalfPlane.σ

Goal state after:
g : GL (Fin 2) ℝ
⊢ Continuous fun x ↦
    (if 0 < ↑(Matrix.GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else conjCAE) (num g ↑x / denom g ↑x)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: a : ℍ
hw : ¬0 < (↑a).im
⊢ a.im ≤ 0

Tactic:
simpa using hw

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

Goal state before:
pp: w w' : ℂ
hw : w.im ≤ 0
hw' : w'.im ≤ 0
⊢ ↑ofComplex w = ↑ofComplex w'

Tactic:
by
  simp [ofComplex_apply_of_im_nonpos, hw, hw']

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
⊢ -g • z = g • z

Tactic:
by
  ext1
  simp [coe_smul]

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
hge : (atTop.limUnder g).compContinuous e = f
⊢ ‖atTop.limUnder g‖ ≤ ‖f‖

pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
hge : (atTop.limUnder g).compContinuous e = f
⊢ ‖f‖ ≤ ‖atTop.limUnder g‖

Tactic:
· rw [← dist_zero_left, ← g0]
    refine
      (dist_le_of_le_geometric_of_tendsto₀ _ _ (by norm_num1)
        hg_dist hg_cau.tendsto_limUnder).trans_eq ?_
    ring

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
hge : (atTop.limUnder g).compContinuous e = f
⊢ ‖f‖ ≤ ‖atTop.limUnder g‖
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.inr.inl.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 →ᵇ ℝ
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)
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hyb : (g - dg) y < b
xu : X
hyxu : (g - dg) y < f xu
right✝ : f xu ≤ b
hc : c < g y
h✝ : a ∉ range ⇑f
⊢ ∃ x₁ x₂, (g - dg) y ∈ Icc (f x₁) (f x₂)

Tactic:
have hay : a < (g - dg) y := by
        calc
          a = c - (b - c) := by rw [← hsub, sub_sub_cancel]
          _ < g y - (b - c) := sub_lt_sub_right hc _
          _ ≤ g y - dg y := sub_le_sub_left (dgmem _).2 _

Goal state after:
case inr.inr.inl.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 →ᵇ ℝ
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)
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hyb : (g - dg) y < b
xu : X
hyxu : (g - dg) y < f xu
right✝ : f xu ≤ b
hc : c < g y
h✝ : a ∉ range ⇑f
hay : a < (g - dg) y
⊢ ∃ x₁ x₂, (g - dg) y ∈ Icc (f x₁) (f x₂)
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ inversion c (dist x c) x = x

Tactic:
inversion,

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ (dist x c / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c = x
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr
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
x : P
hne : x ≠ c
⊢ inversion c R (inversion c R x) = x

Tactic:
inversion,

Goal state after:
case inr
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
x : P
hne : x ≠ c
⊢ (R / dist (inversion c R x) c) ^ 2 • (inversion c R x -ᵥ c) +ᵥ c = 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 (inversion c R) (𝓝[≠] c) (Bornology.cobounded P)

Tactic:
rw [← tendsto_dist_left_atTop_iff c]

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 (fun x ↦ dist c (inversion c R x)) (𝓝[≠] c) atTop
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a b c : ℍ
⊢ dist a c ≤ dist a b + dist b c

Tactic:
rw [dist_le_iff_le_sinh, sinh_half_dist_add_dist, div_mul_eq_div_div _ _ (dist _ _), le_div_iff₀,
    div_mul_eq_mul_div]
  · gcongr
    exact EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist (a : ℂ) b c (conj (b : ℂ))
  · rw [dist_comm, dist_pos, Ne, Complex.conj_eq_iff_im]
    exact b.im_ne_zero

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

Goal state before:
pp: z w : ℍ
⊢ Real.cosh (dist z w) = ((z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2) / (2 * z.im * w.im)

Tactic:
by
  simp [field, cosh_dist, Complex.dist_eq, Complex.sq_norm, normSq_apply]
  ring

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

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ dist ↑z ↑(w.center r) = √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2)

Tactic:
by
  rw [← sqrt_sq dist_nonneg, dist_coe_center_sq]

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

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

Tactic:
simp; abel

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

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

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

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

Goal state before:
pp: X : Type w
Y : Type x
inst✝ : TopologicalSpace X
t : TopologicalSpace Y
f : X → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous[_, t] (f ∘ ⇑g)
⊢ Continuous[compactlyGenerated X, t] f

Tactic:
continuous_coinduced_dom

Goal state after:
X : Type w
Y : Type x
inst✝ : TopologicalSpace X
t : TopologicalSpace Y
f : X → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous[_, t] (f ∘ ⇑g)
⊢ Continuous[_, t]
    (f ∘ fun x ↦
      match x with
      | ⟨⟨fst, i⟩, s⟩ => i s)
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed[tX] s

Tactic:
by
  rw [eq_compactlyGenerated (X := X), TopologicalSpace.compactlyGenerated, isClosed_coinduced,
    isClosed_sigma_iff]
  exact fun ⟨S, f⟩ ↦ hs S f

Goal state after:
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), IsCompact K → IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)

Tactic:
intro K

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
⊢ IsCompact K → IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: 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
⊢ |(characteristic f ⊤ - characteristic (fun x ↦ f x - a₀) ⊤) r| ≤ log⁺ ‖a₀‖ + log 2

Tactic:
characteristic_sub_characteristic_eq_proximity_sub_proximity h

Goal state after:
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
⊢ |(proximity f ⊤ - proximity (fun x ↦ f x - a₀) ⊤) r| ≤ log⁺ ‖a₀‖ + log 2
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‖
⊢ (support D).Finite

Tactic:
obtain ⟨N, hCN⟩ := exists_nat_gt (max C 0)

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
⊢ (support D).Finite
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
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
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
t' : ↥s → Finset α := fun x' ↦ t ↑x'
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s)ᶜ
t'' : ↑ι'' → Finset α := fun a'' ↦ t ↑a'' \ s.biUnion t
⊢ Fintype.card ↑(↑s)ᶜ < Fintype.card ι

Tactic:
← Finset.coe_compl,

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
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
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
t' : ↥s → Finset α := fun x' ↦ t ↑x'
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s)ᶜ
t'' : ↑ι'' → Finset α := fun a'' ↦ t ↑a'' \ s.biUnion t
⊢ Fintype.card ↑↑sᶜ < Fintype.card ι
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
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
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
t' : ↥s → Finset α := fun x' ↦ t ↑x'
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s)ᶜ
t'' : ↑ι'' → Finset α := fun a'' ↦ t ↑a'' \ s.biUnion t
card_ι''_le : Fintype.card ↑ι'' ≤ n
f'' : ↑ι'' → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : ↑ι''), f'' x ∈ t'' x
x'' : ι
hx'' : x'' ∉ s
h : f'' ⟨x'', hx''⟩ ∈ t'' ⟨x'', hx''⟩
⊢ f'' ⟨x'', hx''⟩ ∉ s.biUnion t

Tactic:
rw [mem_sdiff] at h

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
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
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
t' : ↥s → Finset α := fun x' ↦ t ↑x'
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s)ᶜ
t'' : ↑ι'' → Finset α := fun a'' ↦ t ↑a'' \ s.biUnion t
card_ι''_le : Fintype.card ↑ι'' ≤ n
f'' : ↑ι'' → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : ↑ι''), f'' x ∈ t'' x
x'' : ι
hx'' : x'' ∉ s
h : f'' ⟨x'', hx''⟩ ∈ t ↑⟨x'', hx''⟩ ∧ f'' ⟨x'', hx''⟩ ∉ s.biUnion t
⊢ f'' ⟨x'', hx''⟩ ∉ s.biUnion t
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
w x y z : P
h₁ : Wbtw R w y z
h₂ : Sbtw R w x y
⊢ Sbtw R w x z

Tactic:
refine ⟨h₁.trans_left h₂.wbtw, h₂.ne_left, ?_⟩

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
w x y z : P
h₁ : Wbtw R w y z
h₂ : Sbtw R w x y
⊢ x ≠ z
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) ↔ ∃ f, Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
constructor
  · intro h
    -- Set up the functor
    have : ∀ ι' : (Finset ι)ᵒᵖ, Nonempty ((hallMatchingsFunctor t).obj ι') := fun ι' =>
      hallMatchingsOn.nonempty t h ι'.unop
    classical
      have : ∀ ι' : (Finset ι)ᵒᵖ, Finite ((hallMatchingsFunctor t).obj ι') := by
        intro ι'
        rw [hallMatchingsFunctor]
        infer_instance
      -- Apply the compactness argument
      obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (hallMatchingsFunctor t)
      -- Interpret the resulting section of the inverse limit
      refine ⟨?_, ?_, ?_⟩
      · -- Build the matching function from the section
        exact fun i =>
          (u (Opposite.op ({i} : Finset ι))).val ⟨i, by simp only [mem_singleton]⟩
      · -- Show that it is injective
        intro i i'
        have subi : ({i} : Finset ι) ⊆ {i, i'} := by simp
        have subi' : ({i'} : Finset ι) ⊆ {i, i'} := by simp
        simp only
        rw [← hu (CategoryTheory.homOfLE subi).op, ← hu (CategoryTheory.homOfLE subi').op]
        let uii' := u (Opposite.op ({i, i'} : Finset ι))
        exact fun h => Subtype.mk_eq_mk.mp (uii'.property.1 h)
      · -- Show that it maps each index to the corresponding finite set
        intro i
        apply (u (Opposite.op ({i} : Finset ι))).property.2
  · -- The reverse direction is a straightforward cardinality argument
    rintro ⟨f, hf₁, hf₂⟩ s
    rw [← Finset.card_image_of_injective s hf₁]
    apply Finset.card_le_card
    grind

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝² : Category.{v_1, u} J
F : J ⥤ Type v
inst✝¹ : IsCofilteredOrEmpty J
h✝ : F.IsMittagLeffler
inst✝ : ∀ (j : J), Nonempty (F.obj j)
j i : J
f : i ⟶ j
h : F.eventualRange j = range ⇑(ConcreteCategory.hom (F.map f))
⊢ Nonempty (F.toEventualRanges.obj j)

Tactic:
rw [toEventualRanges_obj, h]

Goal state after:
J : Type u
inst✝² : Category.{v_1, u} J
F : J ⥤ Type v
inst✝¹ : IsCofilteredOrEmpty J
h✝ : F.IsMittagLeffler
inst✝ : ∀ (j : J), Nonempty (F.obj j)
j i : J
f : i ⟶ j
h : F.eventualRange j = range ⇑(ConcreteCategory.hom (F.map f))
⊢ Nonempty ↑(range ⇑(ConcreteCategory.hom (F.map f)))
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_1.inl
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
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ x = (lineMap x z) r ∨ ∃ x_1 ∈ Set.Ici 1, (lineMap x ((lineMap x z) r)) x_1 = z

Tactic:
refine .inr ⟨r⁻¹, (one_le_inv₀ hr0').2 hr1, ?_⟩

Goal state after:
case refine_1.inl
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
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ (lineMap x ((lineMap x z) r)) r⁻¹ = z