mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun x ↦ c) (Ioo r R)
⊢ Tendsto f (𝓝[<] R) (𝓝 (f R))

Tactic:
apply (h₁f R (right_mem_Ioc.mpr hR)).mono_left

Goal state after:
f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun x ↦ c) (Ioo r R)
⊢ 𝓝[<] R ≤ 𝓝[Ioc r R] R
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: case hR
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ ‖w - c‖ < R

Tactic:
grind [mem_ball_iff_norm]

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
r : ℝ
hr : r ∈ Set.Ioo ‖w - c‖ R
⊢ w ∈ ball c r

Tactic:
grind [mem_ball_iff_norm]

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

Goal state before:
pp: R : ℝ
w : ℂ
g : ℂ → ℝ
hg : CircleIntegrable g 0 R
hw : w ∈ ball 0 R
⊢ (circleAverage (fun ζ ↦ herglotzRieszKernel 0 w ζ • ↑(g ζ)) 0 R).re =
    circleAverage (re ∘ herglotzRieszKernel 0 w • g) 0 R

Tactic:
have h₁ : CircleIntegrable (fun ζ ↦ (g ζ : ℂ)) 0 R := by
    simp only [CircleIntegrable, intervalIntegrable_iff] at hg ⊢
    exact Complex.ofRealCLM.integrable_comp hg
  have h₂ : CircleIntegrable (fun ζ ↦ herglotzRieszKernel 0 w ζ • (g ζ : ℂ)) 0 R :=
    h₁.continuousOn_smul (continuousOn_herglotzRieszKernel_sphere hw)
  calc (circleAverage (fun ζ ↦ herglotzRieszKernel 0 w ζ • (g ζ : ℂ)) 0 R).re
      = circleAverage (Complex.reCLM ∘ fun ζ ↦ herglotzRieszKernel 0 w ζ • (g ζ : ℂ)) 0 R :=
        (Complex.reCLM.circleAverage_comp_comm h₂).symm
    _ = circleAverage ((Complex.re ∘ herglotzRieszKernel 0 w) • g) 0 R := by
        simp [Function.comp_def, Complex.mul_re, Pi.mul_def]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: case neg
x y : ℝ
hx : ¬x = 0
hy : ¬y = 0
⊢ -(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)

Tactic:
log_mul hx hy

Goal state after:
case neg
x y : ℝ
hx : ¬x = 0
hy : ¬y = 0
⊢ -(x * y * (log x + log y)) = y * -(x * log x) + x * -(y * log y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: case inr.inr
x : ℝ
hx : 0 < x
⊢ sin x ≤ x⁻¹ * x

Tactic:
inv_mul_cancel₀ hx.ne'

Goal state after:
case inr.inr
x : ℝ
hx : 0 < x
⊢ sin x ≤ 1
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
⊢ Real.circleAverage (fun z ↦ ((z + w) / (z - w)).re • f z) 0 R =
    Real.circleAverage (fun z ↦ (z / (z - w) - q • z / (q • z - W)) • f z) 0 R

Tactic:
apply circleAverage_congr_sphere fun z hz ↦ ?_

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • (↑q * z / (↑q * z - W)) • f z = 0
z : ℂ
hz : z ∈ sphere 0 |R|
⊢ ((z + w) / (z - w)).re • f z = (z / (z - w) - q • z / (q • z - W)) • f z
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
this : ∀ (c : ℝ), ∫ (x : ℝ) in 0..c, ↑x ^ r = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
⊢ -(↑a ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)) + ∫ (x : ℝ) in 0..b, ↑x ^ r =
    ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)

Tactic:
this b,

Goal state after:
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
this : ∀ (c : ℝ), ∫ (x : ℝ) in 0..c, ↑x ^ r = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
⊢ -(↑a ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)) + (↑b ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)) =
    ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
hh : 0 < h
⊢ Tendsto (fun x ↦ rexp (-2 * π * x.im / h)) I∞ (𝓝 0)

Tactic:
apply (tendsto_comap'_iff (m := fun y ↦ Real.exp (-2 * π * y / h)) (range_im ▸ univ_mem)).mpr

Goal state after:
h : ℝ
hh : 0 < h
⊢ Tendsto (fun y ↦ rexp (-2 * π * y / h)) atTop (𝓝 0)
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₀)
⊢ ∀ t ∈ ball 0 r, gray w t = g z₀

Tactic:
have e1 : IsPreconnected (ball (0 : ℂ) r) := (convex_ball 0 r).isPreconnected

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}
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)
⊢ ∀ t ∈ ball 0 r, gray w t = g z₀
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖ ≤ (r + ‖w‖) / (r - ‖w‖)

Tactic:
by
        grw [norm_add_le, ← norm_sub_norm_le]
        all_goals simp only [norm_circleMap_zero, abs_of_pos hr]; grind

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

Goal state before:
pp: case inl
n : ℕ
inst✝ : NeZero ↑n
⊢ IsOpenQuotientMap fun z ↦ ⟨↑z ^ ↑n, ⋯⟩

Tactic:
have : NeZero n := ⟨Nat.cast_ne_zero.mp (NeZero.ne (n : ℤ))⟩

Goal state after:
case inl
n : ℕ
inst✝ : NeZero ↑n
this : NeZero n
⊢ IsOpenQuotientMap fun z ↦ ⟨↑z ^ ↑n, ⋯⟩
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: case inl
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0
a : ℂ
⊢ update ((a • f) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((a • f) ∘ invQParam h)) 0 =
    (a • update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0

pp: case inr
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0
a y : ℂ
hy : y ≠ 0
⊢ update ((a • f) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((a • f) ∘ invQParam h)) y =
    (a • update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) y

Tactic:
· simpa using! (Tendsto.const_mul _ (by simpa using! hfcts)).limUnder_eq

Goal state after:
case inr
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0
a y : ℂ
hy : y ≠ 0
⊢ update ((a • f) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((a • f) ∘ invQParam h)) y =
    (a • update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) y
Module: Mathlib.Analysis.Complex.TaylorSeries

Goal state before:
pp: c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Tactic:
convert! taylorSeries_eq_on_ball hf hz using 3 with n
  rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]

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

Goal state before:
pp: a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x * cos x = (sin b ^ 2 - sin a ^ 2) / 2

Tactic:
by
  simpa using integral_sin_pow_mul_cos_pow_odd 1 0

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
e' : X₁ ≃ₜ ↑(Set.range e) := ⋯.toHomeomorph
g : C(X, Y)
hg : restrict (Set.range e) g = f.comp ↑e'.symm
x : X₁
⊢ (g.comp { toFun := e, continuous_toFun := ⋯ }) x = f x

Tactic:
simpa using! congr($(hg) ⟨e' x, x, rfl⟩)

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z w : ℍ
⊢ g • z = w ↔ num g ↑z = (σ g) ↑w * denom g ↑z

Tactic:
rw [← (σ g).injective.eq_iff]

Goal state after:
g : GL (Fin 2) ℝ
z w : ℍ
⊢ g • z = w ↔ (σ g).toAlgEquiv (num g ↑z) = (σ g).toAlgEquiv ((σ g) ↑w * denom g ↑z)
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
⊢ discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = Complex.I ^ 2 * ↑(-(↑g).discr)

pp: g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
⊢ 0 ≤ -(↑g).discr

Tactic:
· simp [discrim, Matrix.discr_fin_two, Matrix.trace_fin_two, Matrix.det_fin_two]
      grind

Goal state after:
g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
⊢ 0 ≤ -(↑g).discr
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 : m.discr = 0 ∨ 4 = 0
⊢ 4 ≠ 0

Tactic:
simpa [show (4 : K) = 2 ^ 2 by norm_num] using NeZero.ne _

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z✝ z w : ℍ
m : Matrix (Fin 2) (Fin 2) ℝ := !![w.im, z.im * w.re - w.im * z.re; 0, z.im]
⊢ m.det ≠ 0

Tactic:
by simp [m, im_ne_zero]

Goal state after:
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
i j : m
lt : i = k ∧ ¬j = k
⊢ (∑ x, M i x * if x = k then -M k j else if x = j then M k k else 0) = 0

Tactic:
mul_ite,

Goal state after:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ (∑ x, if x = k then M i x * -M k j else if x = j then M i x * M k k else M i x * 0) = 0
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case pos
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
y : AlgebraicClosure ↥F
hy : y ∈ (minpoly K x).aroots (AlgebraicClosure ↥F)
P : K[X]
hP : Polynomial.map (algebraMap R K) (minpoly R x) = minpoly K x * P
⊢ (aeval y) (Polynomial.map (algebraMap R K) (minpoly R x)) = 0

Tactic:
simp [hP, aeval_mul, (mem_aroots'.mp hy).2]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
τ : ℍ
⊢ HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ

Tactic:
wlog hg : 0 < g.det.val generalizing g
  · replace hg := g.det.ne_zero.lt_or_gt.resolve_right hg
    convert! Complex.conjCLE.hasStrictFDerivAt.neg.comp _ (this (J * g) (by simpa))
    · simp [mul_smul, coe_J_smul]
    · ext
      simp
  have := (hasStrictDerivAt_smul hg τ).hasStrictFDerivAt.restrictScalars ℝ
  simp_all [smulFDeriv, σ]

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

Goal state before:
pp: a : ℝ
⊢ Isometry fun y ↦ { coe := { re := a, im := rexp y }, coe_im_pos := ⋯ }

Tactic:
refine Isometry.of_dist_eq fun y₁ y₂ => ?_

Goal state after:
a y₁ y₂ : ℝ
⊢ dist { coe := { re := a, im := rexp y₁ }, coe_im_pos := ⋯ } { coe := { re := a, im := rexp y₂ }, coe_im_pos := ⋯ } =
    dist y₁ y₂
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a : { x // 0 < x }
⊢ Isometry fun x ↦ a • x

Tactic:
refine Isometry.of_dist_eq fun y₁ y₂ => ?_

Goal state after:
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ dist (a • y₁) (a • y₂) = dist y₁ y₂
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X✝ : Type w
Y : Type x
X : Type v
t : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ ⊥ ≤ compactlyGenerated X

Tactic:
exact bot_le

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
z : X
⊢ Disjoint (map some (𝓝 z)) (map some (coclosedCompact X)) ∧ Disjoint (map some (𝓝 z)) (pure ∞)

Tactic:
coclosedCompact_eq_cocompact,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
z : X
⊢ Disjoint (map some (𝓝 z)) (map some (cocompact X)) ∧ Disjoint (map some (𝓝 z)) (pure ∞)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
⊢ Tendsto f (coclosedCompact X) (𝓝 y)

Tactic:
coclosedCompact_eq_cocompact,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
⊢ Tendsto f (cocompact X) (𝓝 y)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
s : Set (OnePoint X)
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst✝²] U
hU₃ : y ∈ U
⊢ Uᶜ ⊆ range f

Tactic:
by simpa [hy]

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

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

Tactic:
ext r

Goal state after:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ circleAverage (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r =
    (circleAverage (fun x ↦ log⁺ ‖f₁ x‖) 0 + circleAverage (fun x ↦ log⁺ ‖f₂ x‖) 0) r
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
⊢ (fun r ↦
      ∑ᶠ (z : E), (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹) +
        (↑(D₁ 0) + ↑(D₂ 0)) * log r) =
    (fun r ↦ ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ↑(D₁ 0) * log r) + fun r ↦
      ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹) + ↑(D₂ 0) * log r

Tactic:
ext r

Goal state after:
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
⊢ ∑ᶠ (z : E), (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹) +
      (↑(D₁ 0) + ↑(D₂ 0)) * log r =
    ((fun r ↦ ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ↑(D₁ 0) * log r) + fun r ↦
        ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹) + ↑(D₂ 0) * log r)
      r
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R β : ℝ
⊢ IntervalIntegrable (fun x ↦ cartanKernel f R x β) volume 0 (2 * π)

Tactic:
simpa [cartanKernel, norm_sub_rev, CircleIntegrable] using circleIntegrable_log_norm_sub_const 1

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))

Tactic:
exact h xs ys xy

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mp
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : HasConstantSpeedOnWith f s l
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ variationOnFromTo f s x y = ↑l * (y - x)

Tactic:
rw [hasConstantSpeedOnWith_iff_ordered] at h

Goal state after:
case mp
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ variationOnFromTo f s x y = ↑l * (y - x)
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

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

Tactic:
let F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R

Goal state after:
f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
⊢ circleAverage (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R) 0 1 = proximity f ⊤ R
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
⊢ CircleIntegrable (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R) 0 1

Tactic:
by_cases hR : R = 0
  · simp [hR, circleAverage_zero, norm_sub_rev, circleIntegrable_log_norm_sub_const]
  rw [CircleIntegrable, intervalIntegrable_iff_integrableOn_Ioc_of_le two_pi_pos.le]
  apply IntegrableOn.congr_fun
    ((Cartan.integrableOn_intervalIntegral_cartanKernel_right (R := R) h).const_mul (2 * π)⁻¹)
    (fun _ _ ↦ by simp [circleAverage, Cartan.cartanKernel]) measurableSet_Ioc

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

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

Tactic:
refine ⟨fun ⟨hh, ht⟩ i j k hij hjk hk ↦ ?_,
            fun h ↦ ⟨fun i j hi hj hij ↦ ?_, fun i j k hij hjk hk ↦ ?_⟩⟩

Goal state after:
case cons.refine_1
α : Type u_1
l : List α
p : α → α → α → Prop
head : α
tail : List α
ih : Triplewise p tail ↔ ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]
x✝ :
  (∀ (i j : Nat) (_hi : i < tail.length) (_hj : j < tail.length), i < j → p head tail[i] tail[j]) ∧
    ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]
i j k : Nat
hij : i < j
hjk : j < k
hk : k < tail.length + 1
hh : ∀ (i j : Nat) (_hi : i < tail.length) (_hj : j < tail.length), i < j → p head tail[i] tail[j]
ht : ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]
⊢ p (head :: tail)[i] (head :: tail)[j] (head :: tail)[k]

case cons.refine_2
α : Type u_1
l : List α
p : α → α → α → Prop
head : α
tail : List α
ih : Triplewise p tail ↔ ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]
h :
  ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length + 1),
    p (head :: tail)[i] (head :: tail)[j] (head :: tail)[k]
i j : Nat
hi : i < tail.length
hj : j < tail.length
hij : i < j
⊢ p head tail[i] tail[j]

case cons.refine_3
α : Type u_1
l : List α
p : α → α → α → Prop
head : α
tail : List α
ih : Triplewise p tail ↔ ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]
h :
  ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length + 1),
    p (head :: tail)[i] (head :: tail)[j] (head :: tail)[k]
i j k : Nat
hij : i < j
hjk : j < k
hk : k < tail.length
⊢ p tail[i] tail[j] tail[k]
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z ↦ ↑z) s')
this : #s' = #(s ∪ image (fun z ↦ ↑z) s') - #s
⊢ #(s ∪ image (fun z ↦ ↑z) s') - #(s.biUnion t) ≤ #(s'.biUnion fun x' ↦ t ↑x' \ s.biUnion t)

Tactic:
refine (Nat.sub_le_sub_right (ht _) _).trans ?_

Goal state after:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z ↦ ↑z) s')
this : #s' = #(s ∪ image (fun z ↦ ↑z) s') - #s
⊢ #((s ∪ image (fun z ↦ ↑z) s').biUnion t) - #(s.biUnion t) ≤ #(s'.biUnion fun x' ↦ t ↑x' \ s.biUnion t)
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z ↦ ↑z) s')
this : #s' = #(s ∪ image (fun z ↦ ↑z) s') - #s
⊢ s.biUnion t ⊆ (s ∪ image (fun z ↦ ↑z) s').biUnion t

Tactic:
apply biUnion_subset_biUnion_of_subset_left
    apply subset_union_left

Goal state after: