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

Goal state before:
pp: 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 ‖g x‖) c R = log ‖g c‖

Tactic:
h₁g.circleAverage_log_norm_of_ne_zero

Goal state after:
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
⊢ log ‖g c‖ = log ‖g c‖

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
⊢ ∀ u ∈ closedBall c |R|, g u ≠ 0
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: ⊢ (-1).sqrt = I

Tactic:
simp [sqrt_neg_of_nonneg (a := 1) (by simp)]

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.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
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
⊢ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Tactic:
· refine (dist_le <| mul_nonneg h23.le hf.le).mpr fun x => ?_
    have hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖ := by
      simpa only [Real.norm_eq_abs, abs_le] using f.norm_coe_le_norm x
    rcases le_total (f x) (-‖f‖ / 3) with hle₁ | hle₁
    · calc
        |g (e x) - f x| = -‖f‖ / 3 - f x := by
          rw [hg₁ (mem_image_of_mem _ hle₁), Function.const_apply,
            abs_of_nonneg (sub_nonneg.2 hle₁)]
        _ ≤ 2 / 3 * ‖f‖ := by linarith
    · rcases le_total (f x) (‖f‖ / 3) with hle₂ | hle₂
      · simp only [neg_div] at *
        calc
          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
      · calc
          |g (e x) - f x| = f x - ‖f‖ / 3 := by
            rw [hg₂ (mem_image_of_mem _ hle₂), abs_sub_comm, Function.const_apply,
              abs_of_nonneg (sub_nonneg.2 hle₂)]
          _ ≤ 2 / 3 * ‖f‖ := by linarith

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

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

Tactic:
by simpa [Matrix.det_neg]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
this : (scalar (Fin 2)) (m.discr / 4) = 0
⊢ m.discr = 0

Tactic:
rw [← map_zero (scalar (Fin 2)), scalar_inj, div_eq_zero_iff] at this

Goal state after:
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
this : m.discr = 0 ∨ 4 = 0
⊢ m.discr = 0
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case succ
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)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ ‖f - (g n).compContinuous e‖ ≤ (2 / 3) ^ n * ‖f‖

Tactic:
rwa [← dist_eq_norm']

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
⊢ g • I = I ↔ ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 = -↑g 1 0

Tactic:
rw [gl_smul_eq_iff_num_eq, σ, if_pos hg]

Goal state after:
g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
⊢ num g ↑I = (ContinuousAlgEquiv.refl ℝ ℂ) ↑I * denom g ↑I ↔ ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 = -↑g 1 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : ↑(GeneralLinearGroup.det g) < 0
⊢ g • I = I ↔ ↑g 0 0 = -↑g 1 1 ∧ ↑g 0 1 = ↑g 1 0

Tactic:
by
  rw [gl_smul_eq_iff_num_eq, σ, if_neg (not_lt_of_gt hg)]
  simp [num, denom, Complex.ext_iff, and_comm]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
z : ℍ
⊢ g • z = { coe := num g ↑z / denom g ↑z, coe_im_pos := ⋯ }

Tactic:
ext; simp [coe_smul_of_det_pos hg]

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : 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))
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f

Tactic:
have hge : (limUnder atTop g).compContinuous e = f := by
    refine tendsto_nhds_unique this (tendsto_iff_dist_tendsto_zero.2 ?_)
    refine squeeze_zero (fun _ => dist_nonneg) hgf ?_
    rw [← zero_mul ‖f‖]
    refine (tendsto_pow_atTop_nhds_zero_of_lt_one ?_ ?_).mul tendsto_const_nhds <;> norm_num1

Goal state after:
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
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

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

Tactic:
div_mul_cancel₀ _ (by simpa using τ.ne_zero),

Goal state after:
τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
⊢ ‖r - ‖↑τ‖‖ < ε
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

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

Tactic:
div_mul_cancel₀ _ (by simpa using τ.ne_zero),

Goal state after:
case right
τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
this : ↑r / ↑‖↑τ‖ * ↑τ ∈ Metric.ball (↑τ) ε
ξ : ℍ
hξs : ξ ∈ s
hξτ : ↑ξ = ↑r / ↑‖↑τ‖ * ↑τ
⊢ ‖r‖ = r
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
⊢ f = 0

Tactic:
have := hf.analyticOnNhd isOpen_upperHalfPlaneSet

Goal state after:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
⊢ f = 0
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ 1 + x ^ 2 - x ^ 2 = 1

pp: x : ℝ
⊢ 0 ≤ 1 + x ^ 2

Tactic:
add_sub_cancel_right

Goal state after:
x : ℝ
⊢ 1 = 1

x : ℝ
⊢ 0 ≤ 1 + x ^ 2
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case e_a
z w : ℍ
⊢ 2 ^ 2 * (z.im * w.im) + dist ↑z ↑w ^ 2 = dist (↑z) ((starRingEnd ℂ) ↑w) ^ 2

Tactic:
simp only [Complex.dist_eq, Complex.sq_norm, Complex.normSq_sub, Complex.normSq_conj,
      Complex.conj_conj, Complex.mul_re, Complex.conj_re, Complex.conj_im, coe_im]

Goal state after:
case e_a
z w : ℍ
⊢ 2 ^ 2 * (z.im * w.im) + (Complex.normSq ↑z + Complex.normSq ↑w - 2 * ((↑z).re * (↑w).re - z.im * -w.im)) =
    Complex.normSq ↑z + Complex.normSq ↑w - 2 * ((↑z).re * (↑w).re - z.im * w.im)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case mpr
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' sphere z r

Tactic:
intro hw
    lift w to ℍ using im_pos_of_dist_center_le (sphere_subset_closedBall hw)
    exact mem_image_of_mem _ (dist_eq_iff_dist_coe_center_eq.2 hw)

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
a b : α
e : Ultrafilter.extend g ∘ pure = g
F G : Ultrafilter α
h : Relation.EqvGen (fun F G ↦ ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) F G
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G

Tactic:
induction h with
  | rel x y a => exact let ⟨a, hx, hy⟩ := a; preStoneCechCompat hg hx hy
  | refl x => rfl
  | symm x y _ h => rw [h]
  | trans x y z _ _ h h' => exact h.trans h'

Goal state after:
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:
eq_compactlyGenerated (X := X),

Goal state after:
X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed[compactlyGenerated X] 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)), IsOpen (⇑f ⁻¹' s)
⊢ IsOpen[tX] s

Tactic:
eq_compactlyGenerated (X := X),

Goal state after:
X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)
⊢ IsOpen[compactlyGenerated X] s
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ circleAverage ((fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x‖⁻¹) 0 R = circleAverage (fun x ↦ log ‖f x‖) 0 R

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

pp: case hf₂
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖⁻¹) 0 R

Tactic:
· simp_rw [← posLog_sub_posLog_inv, Pi.sub_def]

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

case hf₂
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖⁻¹) 0 R
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

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

Tactic:
apply (circleIntegrable_congr _).2 (circleIntegrable_const 0 0 1)
    exact fun _ ↦ log_trailingCoeff_eq_zero_on_unitSphere hpos

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

Goal state before:
pp: case hf₁
f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
hb : b ∈ Ioi 0
hab : a ≤ b
⊢ CircleIntegrable (fun x ↦ logCounting f (↑x) a) 0 1

Tactic:
exact circleIntegrable_logCounting h

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

Goal state before:
pp: case hf₂
f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
hb : b ∈ Ioi 0
hab : a ≤ b
⊢ CircleIntegrable (fun x ↦ logCounting f (↑x) b) 0 1

Tactic:
exact circleIntegrable_logCounting h

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

Goal state before:
pp: case h
f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
hb : b ∈ Ioi 0
hab : a ≤ b
x✝ : ℂ
a✝ : x✝ ∈ sphere 0 |1|
⊢ logCounting f (↑x✝) a ≤ logCounting f (↑x✝) b

Tactic:
exact circleIntegrable_logCounting h

Goal state after:
case h
f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
hb : b ∈ Ioi 0
hab : a ≤ b
x✝ : ℂ
a✝ : x✝ ∈ sphere 0 |1|
⊢ logCounting f (↑x✝) a ≤ logCounting f (↑x✝) b
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‖
r : ℝ
hr : R₀ ≤ r
⊢ ∑ c ∈ t, logCounting (single c 1) r = ∑ z ∈ t, (log r - log ‖z‖)

Tactic:
by
        congr! 1 with z hz;
        simpa using logCounting_single_eq_log_sub_const (e := z) (n := 1) ((hR₀ z hz).trans hr)

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 ≠ ⊤
⊢ logCounting (f₁ * f₂) ⊤ r ≤ (logCounting f₁ ⊤ + logCounting f₂ ⊤) r

Tactic:
simp only [logCounting, reduceDIte]
  rw [divisor_mul h₁f₁.meromorphicOn h₁f₂.meromorphicOn (fun z _ ↦ h₂f₁ z) (fun z _ ↦ h₂f₂ z),
    ← locallyFinsuppWithin.logCounting.map_add]
  apply locallyFinsuppWithin.logCounting_le _ hr
  apply locallyFinsuppWithin.negPart_add

Goal state after:
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'
hf : Injective ⇑f
⊢ Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z

Tactic:
by
  simp_rw [Sbtw, hf.wbtw_map_iff, hf.ne_iff]

Goal state after:
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
x z : P
t : R
ht : t ∈ Set.Icc 0 1
hyx : (lineMap x z) t ≠ x
hyz : (lineMap x z) t ≠ z
⊢ (lineMap x z) t ∈ ⇑(lineMap x z) '' Set.Ioo 0 1

Tactic:
rcases Set.eq_endpoints_or_mem_Ioo_of_mem_Icc ht with (rfl | rfl | ho)

Goal state after:
case inl
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
x z : P
ht : 0 ∈ Set.Icc 0 1
hyx : (lineMap x z) 0 ≠ x
hyz : (lineMap x z) 0 ≠ z
⊢ (lineMap x z) 0 ∈ ⇑(lineMap x z) '' Set.Ioo 0 1

case inr.inl
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
x z : P
ht : 1 ∈ Set.Icc 0 1
hyx : (lineMap x z) 1 ≠ x
hyz : (lineMap x z) 1 ≠ z
⊢ (lineMap x z) 1 ∈ ⇑(lineMap x z) '' Set.Ioo 0 1

case inr.inr
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
x z : P
t : R
ht : t ∈ Set.Icc 0 1
hyx : (lineMap x z) t ≠ x
hyz : (lineMap x z) t ≠ z
ho : t ∈ Set.Ioo 0 1
⊢ (lineMap x z) t ∈ ⇑(lineMap x z) '' Set.Ioo 0 1
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case pos
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
inst✝ : Nontrivial P
l : List P
h : List.Sbtw R l
hl : l = []
⊢ ∃ p₁ p₂, p₁ ≠ p₂ ∧ ∃ l', l'.SortedLT ∧ map (⇑(lineMap p₁ p₂)) l' = l

Tactic:
rcases exists_pair_ne P with ⟨p₁, p₂, hp₁p₂⟩

Goal state after:
case pos
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
inst✝ : Nontrivial P
l : List P
h : List.Sbtw R l
hl : l = []
p₁ p₂ : P
hp₁p₂ : p₁ ≠ p₂
⊢ ∃ p₁ p₂, p₁ ≠ p₂ ∧ ∃ l', l'.SortedLT ∧ map (⇑(lineMap p₁ p₂)) l' = l
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 y z : P
h : Wbtw R x y z
⊢ Wbtw R z x y ↔ x = y

Tactic:
← wbtw_rotate_iff R x,

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 y z : P
h : Wbtw R x y z
⊢ Wbtw R z x y ↔ Wbtw R x y ?m.40 ∧ Wbtw R ?m.40 x y

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 y z : P
h : Wbtw R x y z
⊢ P
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: case refine_1
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : FiniteDiagram J
ιA : FiniteDiagramArrow A.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : FiniteDiagramArrow B.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
⊢ (fun G ↦ partialSections F G.snd) A ⊇
    (fun G ↦ partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩

Tactic:
rintro u hu f hf
    have : ιA f ∈ A.2.image ιA ⊔ B.2.image ιB := by
      apply Finset.mem_union_left
      rw [Finset.mem_image]
      exact ⟨f, hf, rfl⟩
    exact hu this

Goal state after:
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
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
⊢ Sbtw R ((Finset.affineCombination R s p) w₁)
    ((lineMap ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w₂)) r)
    ((Finset.affineCombination R s p) w₂)

Tactic:
sbtw_lineMap_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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
⊢ (Finset.affineCombination R s p) w₁ ≠ (Finset.affineCombination R s p) w₂ ∧ r ∈ Set.Ioo 0 1
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✝³ : AffineSpace V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
s : Simplex R P 1
p : P
⊢ p ∈ s.interior ↔ Sbtw R (s.points 0) p (s.points 1)

Tactic:
rw [interior_eq_image_Ioo, sbtw_iff_mem_image_Ioo_and_ne]

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✝³ : AffineSpace V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
s : Simplex R P 1
p : P
⊢ p ∈ ⇑(lineMap (s.points 0) (s.points 1)) '' Set.Ioo 0 1 ↔
    p ∈ ⇑(lineMap (s.points 0) (s.points 1)) '' Set.Ioo 0 1 ∧ s.points 0 ≠ s.points 1
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: case h.none.none
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬none = none
hf : f i = none
hg : g i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ none then 1 else 0

Tactic:
exact (hi rfl).elim

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

Goal state before:
pp: 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 y z : P
⊢ Sbtw R x y z ↔ x ≠ y ∧ z ∈ ⇑(lineMap x y) '' Set.Ioi 1

Tactic:
refine ⟨fun h => ⟨h.left_ne, ?_⟩, fun h => ?_⟩
  · obtain ⟨r, ⟨hr, rfl⟩⟩ := h.wbtw.right_mem_image_Ici_of_left_ne h.left_ne
    rw [Set.mem_Ici] at hr
    rcases hr.lt_or_eq with (hrlt | rfl)
    · exact Set.mem_image_of_mem _ hrlt
    · simp at h
  · rcases h with ⟨hne, r, hr, rfl⟩
    rw [Set.mem_Ioi] at hr
    refine
      ⟨wbtw_iff_left_eq_or_right_mem_image_Ici.2
          (Or.inr (Set.mem_image_of_mem _ (Set.mem_of_mem_of_subset hr Set.Ioi_subset_Ici_self))),
        hne.symm, ?_⟩
    rw [lineMap_apply, ← @vsub_ne_zero V, vsub_vadd_eq_vsub_sub]
    nth_rw 1 [← one_smul R (y -ᵥ x)]
    rw [← sub_smul, smul_ne_zero_iff, vsub_ne_zero, sub_ne_zero]
    exact ⟨hr.ne, hne.symm⟩

Goal state after: