mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
⊢ CircleIntegrable (fun x ↦ log ‖f x‖) c R

Tactic:
by_cases t₀ : ∀ u : (sphere c |R|), meromorphicOrderAt f u ≠ ⊤
  · obtain ⟨g, h₁g, h₂g, h₃g⟩ := hf.extract_zeros_poles t₀
      ((divisor f (sphere c |R|)).finiteSupport (isCompact_sphere c |R|))
    have h₄g := MeromorphicOn.extract_zeros_poles_log h₂g h₃g
    apply CircleIntegrable.congr_codiscreteWithin h₄g.symm
    apply CircleIntegrable.add
    · apply CircleIntegrable.finsum
      intro i
      apply IntervalIntegrable.const_mul
      apply MeromorphicOn.intervalIntegrable_log_norm
      apply AnalyticOnNhd.meromorphicOn
      apply AnalyticOnNhd.sub _ analyticOnNhd_const
      apply (analyticOnNhd_circleMap c R).mono (by tauto)
    · apply ContinuousOn.intervalIntegrable
      apply ContinuousOn.log
      · apply ContinuousOn.norm
        apply h₁g.continuousOn.comp (t := sphere c |R|) (continuous_circleMap c R).continuousOn
        intro x hx
        simp
      · intro x hx
        rw [ne_eq, norm_eq_zero]
        apply h₂g ⟨circleMap c R x, circleMap_mem_sphere' c R x⟩
  · rw [← hf.exists_meromorphicOrderAt_ne_top_iff_forall (isConnected_sphere (by simp) c
      (abs_nonneg R))] at t₀
    push Not at t₀
    have : (log ‖f ·‖) =ᶠ[codiscreteWithin (sphere c |R|)] 0 := by
      filter_upwards [hf.meromorphicNFAt_mem_codiscreteWithin,
        self_mem_codiscreteWithin (sphere c |R|)] with x h₁x h₂x
      simp only [Pi.zero_apply, log_eq_zero, norm_eq_zero]
      left
      by_contra hCon
      simp_all [← h₁x.meromorphicOrderAt_eq_zero_iff, t₀ ⟨x, h₂x⟩]
    apply CircleIntegrable.congr_codiscreteWithin this.symm (circleIntegrable_const 0 c R)

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

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ circleAverage (fun z ↦ log ‖R‖ + log ‖z + ↑R⁻¹ * (c - a)‖) 0 1 = log R + log⁺ (|R|⁻¹ * ‖c - a‖)

Tactic:
rw [← Pi.add_def, circleAverage_add (circleIntegrable_const (log ‖R‖) 0 1)
      (MeromorphicOn.circleIntegrable_log_norm (fun _ _ ↦ by fun_prop)), circleAverage_const]
    simp

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

Goal state before:
pp: f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z ↦ ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
⊢ v ∈ f '' closedBall z₀ r

Tactic:
have h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖ := fun z hz => by
    linarith [hf z hz, show ‖v - f z₀‖ < ε / 2 from mem_ball_iff_norm.1 hv,
      norm_sub_sub_norm_sub_le_norm_sub (f z) v (f z₀)]

Goal state after:
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z ↦ ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
⊢ v ∈ f '' closedBall z₀ r
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
w : ℂ
hw : w ∈ P.roots.toFinset
⊢ 0 < ↑(rootMultiplicity w P)

Tactic:
by simp_all

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

Goal state before:
pp: h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
⊢ ContinuousAt (cuspFunction h (-g)) 0

Tactic:
simp [cuspFunction_neg, hgcts]

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

Goal state before:
pp: w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
this :
  (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) =
    Complex.re ∘ herglotzRieszKernel 0 (w - c) • fun x ↦ log ‖x - (ρ - c)‖
⊢ ρ - c ∈ sphere 0 R

Tactic:
by simp_all

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

Goal state before:
pp: case neg
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : D c = 0
x : ℂ
h₁ : ¬c = x
⊢ ↑(D x) * (log R - log ‖c - x‖) = ↑(D x) * log (R * ‖c - x‖⁻¹)

Tactic:
log_mul hR (inv_ne_zero (norm_ne_zero_iff.mpr (sub_eq_zero.not.2 h₁))),

Goal state after:
case neg
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : D c = 0
x : ℂ
h₁ : ¬c = x
⊢ ↑(D x) * (log R - log ‖c - x‖) = ↑(D x) * (log R + log ‖c - x‖⁻¹)
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
⊢ ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u ≠ ⊤

Tactic:
by simp_all

Goal state after:
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
x✝ : ℂ
⊢ (x✝ ∈ Function.support fun u ↦ ↑((divisor f CB) u) * log R) → x✝ ∈ (divisor f CB).support

Tactic:
by simp_all

Goal state after:
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
x✝ : ℂ
⊢ (x✝ ∈ Function.support fun u ↦ ↑((divisor f CB) u) * log ‖c - u‖) → x✝ ∈ (divisor f CB).support

Tactic:
by simp_all

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

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : I = 0
⊢ sqrt a = ↑√(re a)

pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ sqrt a = ↑√(re a)

Tactic:
· simp [h, sqrt_eq_ite]

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ sqrt a = ↑√(re a)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case neg
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 : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this✝ : divisor f CB = 0
this : f =ᶠ[codiscreteWithin CB] 0
⊢ circleAverage 0 c R = 0

Tactic:
simp only [circleAverage, mul_inv_rev, Pi.zero_apply, intervalIntegral.integral_zero,
        smul_eq_mul, mul_zero]

Goal state after:
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
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
x✝¹ : ℂ
x✝ : x✝¹ ∈ Function.support fun u ↦ ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r)
⊢ x✝¹ ∈ (divisor f (closedBall c |r|)).support

Tactic:
by simp_all

Goal state after:
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
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
x✝¹ : ℂ
x✝ : x✝¹ ∈ Function.support fun u ↦ ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)
⊢ x✝¹ ∈ (divisor f (closedBall c |R|)).support

Tactic:
by simp_all

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

Goal state before:
pp: case refine_1
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝ : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
x : E
hx : x ∈ frontier (Metric.closedBall 0 1)
⊢ id x = g x

Tactic:
replace hx : ‖x‖ = 1 := by simpa [frontier_closedBall (0 : E) one_ne_zero] using hx
    simp [g, hx]

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

Goal state before:
pp: X : Type u
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
f : ↑s →ᵇ E
hf : ¬‖f‖ = 0
⊢ 0 < ‖f‖

Tactic:
by simp_all

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:
by simpa using h

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
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)
x : X
hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖
hle₁ : f x ≤ -‖f‖ / 3
⊢ |g (e x) - f x| = -‖f‖ / 3 - f x

Tactic:
rw [hg₁ (mem_image_of_mem _ hle₁), Function.const_apply,
            abs_of_nonneg (sub_nonneg.2 hle₁)]

Goal state after:
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

Tactic:
hξτ,

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

Goal state before:
pp: case refine_1
⊢ Continuous fun z ↦ NNReal.mk z.im ⋯

pp: case refine_2
⊢ ∀ (x : ℍ), NNReal.mk x.im ⋯ ≠ 0

Tactic:
· exact continuous_im.subtype_mk _

Goal state after:
case refine_2
⊢ ∀ (x : ℍ), NNReal.mk x.im ⋯ ≠ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (↑ofComplex) z

Tactic:
rw [contMDiffAt_iff]

Goal state after:
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContinuousAt (↑ofComplex) z ∧
    ContDiffWithinAt ℂ n (↑(extChartAt 𝓘(ℂ, ℂ) (↑ofComplex z)) ∘ ↑ofComplex ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm)
      (Set.range ↑𝓘(ℂ, ℂ)) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (↑ofComplex) z

Tactic:
rw [contMDiffAt_iff]
  constructor
  · -- continuity at z
    rw [ContinuousAt, nhds_induced, tendsto_comap_iff]
    refine Tendsto.congr' (eventuallyEq_coe_comp_ofComplex hz).symm ?_
    simpa [ofComplex_apply_of_im_pos hz] using! tendsto_id
  · -- smoothness in local chart
    simpa using! contDiffAt_id.congr_of_eventuallyEq (eventuallyEq_coe_comp_ofComplex hz)

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
this : HasStrictDerivAt (num g / denom g) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ
⊢ num g / denom g =ᶠ[map UpperHalfPlane.coe (𝓝 τ)] fun z ↦ ↑(g • ↑ofComplex z)

Tactic:
eventuallyEq_map

Goal state after:
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
this : HasStrictDerivAt (num g / denom g) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ
⊢ (num g / denom g) ∘ UpperHalfPlane.coe =ᶠ[𝓝 τ] (fun z ↦ ↑(g • ↑ofComplex z)) ∘ UpperHalfPlane.coe
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

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

Tactic:
dist_comm,

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 x : P
⊢ inversion c (dist x c) x = x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a b c : ℍ
⊢ 0 < dist (↑b) ((starRingEnd ℂ) ↑b)

Tactic:
dist_comm,

Goal state after:
a b c : ℍ
⊢ 0 < dist ((starRingEnd ℂ) ↑b) ↑b
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z : ℍ
r : ℝ
⊢ dist (↑z).im (↑(z.center r)).im = z.im * (Real.cosh r - 1)

Tactic:
dist_comm,

Goal state after:
z : ℍ
r : ℝ
⊢ dist (↑(z.center r)).im (↑z).im = z.im * (Real.cosh r - 1)
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: case refine_2
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
⊢ ofHom P { toFun := ⇑E.symm, continuous_toFun := hE } ≫ f = 𝟙 Y

Tactic:
ext x
    apply E.apply_symm_apply

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ 𝓝 ∞ = map some (coclosedCompact X) ⊔ pure ∞

Tactic:
by
  rw [← nhdsNE_infty_eq, nhdsNE_sup_pure]

Goal state after:
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, ℝ)
hδK : δ ≤ (g • I).im
hg : g • I ∈ K
⊢ ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ 1 / δ

Tactic:
simp only [MulAction.compHom_smul_def, im_smul_eq_div_normSq, Matrix.SpecialLinearGroup.det_mapGL,
    Units.val_one, abs_one, I_im, mul_one] at hδK

Goal state after:
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 / δ
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

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

Tactic:
by_cases hf : MeromorphicAt f 0
  · rw [← circleAverage_congr_codiscreteWithin
      (eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero hf h) zero_ne_one.symm]
    simp_rw [norm_sub_rev]
    rw [circleAverage_log_norm_sub_const_eq_posLog]
  have {a : ℂ} : ¬ MeromorphicAt (fun x ↦ f x - a) 0 := by
    rwa [MeromorphicAt.meromorphicAt_fun_sub_iff_meromorphicAt₂ (by fun_prop)]
  simp_all [circleAverage_const]

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

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
a : ℂ
⊢ logCounting (f - fun x ↦ a) 0 R - logCounting f ⊤ R =
    circleAverage (fun x ↦ log ‖f x - a‖) 0 R - log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖

Tactic:
← logCounting_sub_const h

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
a : ℂ
⊢ logCounting (f - fun x ↦ a) 0 R - logCounting (f - fun x ↦ ?m.127) ⊤ R =
    circleAverage (fun x ↦ log ‖f x - a‖) 0 R - log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖

f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
a : ℂ
⊢ ℂ
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
a✝ : a ≤ b
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
z : E
hz : z ∈ hs.toFinset
h₂z : ¬z = 0
this : z ∈ closedBall 0 |b|
h₃z : z ∉ closedBall 0 |a|
⊢ ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹) ≤ ↑(D z) * log (b * ‖z‖⁻¹)

Tactic:
· 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]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
⊢ StrictMonoOn (logCounting D) (Ioi ‖e‖)

Tactic:
by
  rw [(by aesop : logCounting D = logCounting (single e 1) + logCounting (D - single e 1))]
  apply StrictMonoOn.add_monotone
  · intro a ha b hb hab
    rw [mem_Ioi] at ha hb
    rw [logCounting_single_eq_log_sub_const ha.le, logCounting_single_eq_log_sub_const hb.le]
    gcongr
    exact (norm_nonneg e).trans_lt ha
  · intro a ha b hb hab
    apply logCounting_mono _ _ ((norm_nonneg e).trans_lt hb) hab
    · simp [hD]
    · simpa [mem_Ioi] using (norm_nonneg e).trans_lt ha

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

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

Tactic:
by
  rw [wbtw_comm, wbtw_zero_one_iff]

Goal state after:
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: α : Type v
inst✝¹ : DecidableEq α
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val✝ : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι],
      (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) →
        ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
⊢ ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x

Tactic:
intro ι'

Goal state after:
α : Type v
inst✝¹ : DecidableEq α
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val✝ : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι],
      (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) →
        ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ι' : Type u
⊢ ∀ [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
⊢ ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')

Tactic:
intro ι'

Goal state after:
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
ι' : (Finset ι)ᵒᵖ
⊢ Finite ((hallMatchingsFunctor t).obj ι')
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: case mp.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i : ι
⊢ ∀ ⦃a₂ : ι⦄, (fun i ↦ ↑(u (Opposite.op {i})) ⟨i, ⋯⟩) i = (fun i ↦ ↑(u (Opposite.op {i})) ⟨i, ⋯⟩) a₂ → i = a₂

Tactic:
i'

Goal state after:
case mp.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
⊢ (fun i ↦ ↑(u (Opposite.op {i})) ⟨i, ⋯⟩) i = (fun i ↦ ↑(u (Opposite.op {i})) ⟨i, ⋯⟩) i' → i = i'
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j : n
⊢ (Equiv.toPEquiv (Equiv.swap i j)).toMatrix =
    1 - (single i i).toMatrix - (single j j).toMatrix + (single i j).toMatrix + (single j i).toMatrix

Tactic:
ext
  dsimp [toMatrix, single, Equiv.swap_apply_def, Equiv.toPEquiv, Matrix.one_apply]
  split_ifs <;> simp_all

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
hM : M ∈ rowStochastic R n
i j : n
⊢ M i j ≤ ∑ j, M i j

Tactic:
exact single_le_sum (fun k _ => hM.1 _ k) (mem_univ j)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
hM : M ∈ rowStochastic R n
i j : n
⊢ M i j ≤ 1

Tactic:
rw [← sum_row_of_mem_rowStochastic hM i]
  exact single_le_sum (fun k _ => hM.1 _ k) (mem_univ j)

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: k : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : DecidableEq k
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
b₁ b₂ : n
hb : b₁ ≠ b₂
a : m
c : k
⊢ ((single a b₁).trans (single b₂ c)).toMatrix = 0

Tactic:
single_trans_single_of_ne hb,

Goal state after:
k : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : DecidableEq k
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
b₁ b₂ : n
hb : b₁ ≠ b₂
a : m
c : k
⊢ ⊥.toMatrix = 0