mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p
v : (ι → ℝ) → F := u ∘ ⇑e.symm
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  ↑c * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (⇑e.symm) volume ≤
    ↑C * ↑(c ^ p) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂Measure.map (⇑e.symm) volume) ^ p
⊢ ↑c * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (⇑e.symm) volume ≤
    ↑C * (↑c ^ p * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂Measure.map (⇑e.symm) volume) ^ p)

Tactic:
← mul_assoc,

Goal state after:
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p
v : (ι → ℝ) → F := u ∘ ⇑e.symm
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  ↑c * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (⇑e.symm) volume ≤
    ↑C * ↑(c ^ p) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂Measure.map (⇑e.symm) volume) ^ p
⊢ ↑c * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (⇑e.symm) volume ≤
    ↑C * ↑c ^ p * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂Measure.map (⇑e.symm) volume) ^ p
Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : LipschitzWith 1 ⇑f
g : E →L[𝕜] ↥(f.eqLocus 1)
hg_proj : ∀ (x : ↥(f.eqLocus 1)), g ↑x = x
hg_ker : ↑(↑g).ker ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(f - 1).range
y : E
hy : g y = 0
z : E
hz : IsFixedPt (⇑f) z
this :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    {x | Tendsto (fun x_1 ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 0)}
x : E
⊢ (f - 1) x ∈ {x | Tendsto (fun x_1 ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 0)}

Tactic:
have : IsBounded (Set.range (_root_.id <| f^[·] x)) :=
    isBounded_iff_forall_norm_le.2 ⟨‖x‖, Set.forall_mem_range.2 fun n ↦ by
      have H : f^[n] 0 = 0 := iterate_map_zero (f : E →+ E) n
      simpa [H] using (hf.iterate n).dist_le_mul x 0⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : LipschitzWith 1 ⇑f
g : E →L[𝕜] ↥(f.eqLocus 1)
hg_proj : ∀ (x : ↥(f.eqLocus 1)), g ↑x = x
hg_ker : ↑(↑g).ker ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(f - 1).range
y : E
hy : g y = 0
z : E
hz : IsFixedPt (⇑f) z
this✝ :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    {x | Tendsto (fun x_1 ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 0)}
x : E
this : Bornology.IsBounded (Set.range fun x_1 ↦ _root_.id ((⇑f)^[x_1] x))
⊢ (f - 1) x ∈ {x | Tendsto (fun x_1 ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 0)}
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ RCLike.re (∑ x, ∑ x_1, ‖f‖ ^ 2 • inner 𝕜 (e x_1) (e x) * inner 𝕜 (g x_1) (g x)) -
      RCLike.re (∑ x, ∑ x_1, (∑ i, Matrix.vecMulVec (A i) (star (A i))) x_1 x * inner 𝕜 (g x_1) (g x)) ≤
    ‖f‖ ^ 2 * RCLike.re (∑ x, ∑ i, inner 𝕜 (e i) (e x) * inner 𝕜 (g i) (g x))

Tactic:
← RCLike.smul_re,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ RCLike.re (∑ x, ∑ x_1, ‖f‖ ^ 2 • inner 𝕜 (e x_1) (e x) * inner 𝕜 (g x_1) (g x)) -
      RCLike.re (∑ x, ∑ x_1, (∑ i, Matrix.vecMulVec (A i) (star (A i))) x_1 x * inner 𝕜 (g x_1) (g x)) ≤
    RCLike.re (‖f‖ ^ 2 • ∑ x, ∑ i, inner 𝕜 (e i) (e x) * inner 𝕜 (g i) (g x))
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ 0 ≤ RCLike.re (∑ x, ∑ x_1, ∑ x_2, A x x_2 * (inner 𝕜 (g x_2) (g x_1) * star (A x x_1)))

Tactic:
← mul_assoc,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ 0 ≤ RCLike.re (∑ x, ∑ x_1, ∑ x_2, A x x_2 * inner 𝕜 (g x_2) (g x_1) * star (A x x_1))
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case pos
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : μ (s \ t) = ∞
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
rw [htop, add_top, ← htop]

Goal state after:
case pos
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : μ (s \ t) = ∞
⊢ μ (s \ t) ≤ μ s
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
⊢ f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖

Tactic:
have hrank : finrank 𝕜 U = finrank 𝕜 f.range := by
    rw [finrank_eq_nat_card_basis bu.toBasis, finrank_eq_nat_card_basis bv.toBasis]

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
⊢ f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
b : ℝ≥0∞
hb : b ∈ {a | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a}
t : Set X
htx : t ∈ 𝓝[s] x
ht : ∀ t_1 ⊆ t, dimH t_1 ≤ b
⊢ r ≤ b

Tactic:
exact (hxr t htx).le.trans (ht t Subset.rfl)

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets = dimH s

Tactic:
refine le_antisymm (iSup₂_le fun x _ => ?_) ?_
  · refine limsup_le_of_le isCobounded_le_of_bot ?_
    exact eventually_smallSets.2 ⟨s, self_mem_nhdsWithin, fun t => dimH_mono⟩
  · refine le_of_forall_lt_imp_le_of_dense fun r hr => ?_
    rcases exists_mem_nhdsWithin_lt_dimH_of_lt_dimH hr with ⟨x, hxs, hxr⟩
    refine le_iSup₂_of_le x hxs ?_; rw [limsup_eq]; refine le_sInf fun b hb => ?_
    rcases eventually_smallSets.1 hb with ⟨t, htx, ht⟩
    exact (hxr t htx).le.trans (ht t Subset.rfl)

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : 𝕜
x y : E
⊢ (starRingEnd 𝕜) ↑(re r) * inner_ 𝕜 x y + (starRingEnd 𝕜) ↑(im r) * ((starRingEnd 𝕜) I * inner_ 𝕜 x y) =
    (starRingEnd 𝕜) (↑(re r) + ↑(im r) * I) * inner_ 𝕜 x y

Tactic:
map_add,

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : 𝕜
x y : E
⊢ (starRingEnd 𝕜) ↑(re r) * inner_ 𝕜 x y + (starRingEnd 𝕜) ↑(im r) * ((starRingEnd 𝕜) I * inner_ 𝕜 x y) =
    ((starRingEnd 𝕜) ↑(re r) + (starRingEnd 𝕜) (↑(im r) * I)) * inner_ 𝕜 x y
Module: Mathlib.Analysis.InnerProductSpace.StarOrder

Goal state before:
pp: case mpr
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
⊢ (∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p) → f ≤ g

Tactic:
rintro ⟨p, hp, rfl⟩

Goal state after:
case mpr
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ (H →L[𝕜] H) IsSelfAdjoint
f p : H →L[𝕜] H
hp : p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
⊢ f ≤ f + p
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
⊢ ⇑(toWeakSpace 𝕜 E) '' closure s = closure (⇑(toWeakSpace 𝕜 E) '' s)

Tactic:
by
  refine le_antisymm (map_continuous <| toWeakSpaceCLM 𝕜 E).continuousOn.image_closure
    (Set.compl_subset_compl.mp fun x hx ↦ ?_)
  obtain ⟨x, -, rfl⟩ := (toWeakSpace 𝕜 E).toEquiv.image_compl (closure s) |>.symm.subset hx
  have : ContinuousSMul ℝ E := IsScalarTower.continuousSMul 𝕜
  obtain ⟨f, u, hus, hux⟩ := RCLike.geometric_hahn_banach_closed_point (𝕜 := 𝕜)
    hs.closure isClosed_closure (by simpa using hx)
  let f' : StrongDual 𝕜 (WeakSpace 𝕜 E) :=
    { toLinearMap := (f : E →ₗ[𝕜] 𝕜).comp ((toWeakSpace 𝕜 E).symm : WeakSpace 𝕜 E →ₗ[𝕜] E)
      cont := WeakBilin.eval_continuous (topDualPairing 𝕜 E).flip _ }
  have hux' : u < RCLike.reCLM.comp (f'.restrictScalars ℝ) (toWeakSpace 𝕜 E x) := by simpa [f']
  have hus' : closure (toWeakSpace 𝕜 E '' s) ⊆
      {y | RCLike.reCLM.comp (f'.restrictScalars ℝ) y ≤ u} := by
    refine closure_minimal ?_ <| isClosed_le (by fun_prop) (by fun_prop)
    rintro - ⟨y, hy, rfl⟩
    simpa [f'] using (hus y <| subset_closure hy).le
  exact (hux'.not_ge <| hus' ·)

Goal state after:
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ mellinInv σ (fun s ↦ 𝓕 g (s.im / (2 * π))) x = ↑x ^ (-↑σ) • g (-Real.log x)

Tactic:
rw [mellinInv_eq_fourierInv _ _ hx, ← hf.fourierInv_fourier_eq hFf hfx]
      simp [mul_div_cancel_left₀ _ (show 2 * π ≠ 0 by simp)]

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (t ^ a) = (|a|⁻¹ * (|a| * t ^ (a - 1))) • ↑(t ^ a) ^ (s / ↑a - 1) • f (t ^ a)

Tactic:
← mul_assoc,

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (t ^ a) = (|a|⁻¹ * |a| * t ^ (a - 1)) • ↑(t ^ a) ^ (s / ↑a - 1) • f (t ^ a)
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this : EqOn (fun t ↦ ↑t ^ (s - 1) • f (a * t)) (fun t ↦ ↑a ^ (1 - s) • (fun u ↦ ↑u ^ (s - 1) • f u) (a * t)) (Ioi 0)
⊢ ∫ (x : ℝ) in Ioi 0, ↑a ^ (1 - s) • (fun u ↦ ↑u ^ (s - 1) • f u) (a * x) ∂volume =
    ↑a ^ (-s) • ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t

Tactic:
integral_smul,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this : EqOn (fun t ↦ ↑t ^ (s - 1) • f (a * t)) (fun t ↦ ↑a ^ (1 - s) • (fun u ↦ ↑u ^ (s - 1) • f u) (a * t)) (Ioi 0)
⊢ ↑a ^ (1 - s) • ∫ (a_1 : ℝ) in Ioi 0, (fun u ↦ ↑u ^ (s - 1) • f u) (a * a_1) ∂volume =
    ↑a ^ (-s) • ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹
⊢ ‖z‖ * (‖z‖ ^ n * ‖∫ (x : ℝ) in 0..1, ↑x ^ n * (1 + ↑x * z)⁻¹‖) ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

Tactic:
← mul_assoc,

Goal state after:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹
⊢ ‖z‖ * ‖z‖ ^ n * ‖∫ (x : ℝ) in 0..1, ↑x ^ n * (1 + ↑x * z)⁻¹‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
| HasSum (fun n ↦ z ^ n / ↑n) (-log (1 - z))

Tactic:
enter [1, n]

Goal state after:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
| z ^ n / ↑n
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun n ↦ z ^ n / ↑n) (-log (1 - z))

Tactic:
conv => enter [1, n]; rw [← neg_neg (z ^ n / n)]
  refine HasSum.neg ?_
  convert! hasSum_taylorSeries_log (z := -z) (norm_neg z ▸ hz) using 2 with n
  rcases n.eq_zero_or_pos with rfl | hn
  · simp
  simp [field, pow_add, ← mul_pow]

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
⊢ 1 / 2 * ((↑(2 * n) + 1) / (↑(2 * n) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))

Tactic:
← mul_assoc,

Goal state after:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
⊢ 1 / 2 * ((↑(2 * n) + 1) / (↑(2 * n) + 2)) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
⊢ 1 / 2 * ((↑(2 * n) + 1) / (↑(2 * n) + 2)) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))

Tactic:
← mul_assoc,

Goal state after:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
⊢ 1 / 2 * ((↑(2 * n) + 1) / (↑(2 * n) + 2)) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * (1 / 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le' (f := logGammaSeq x)
    (g := fun n ↦ f x - f 1 - x * (log (n + 1) - log n)) ?_ tendsto_const_nhds ?_ ?_

Goal state after:
case refine_1
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
⊢ Tendsto (fun n ↦ f x - f 1 - x * (log (↑n + 1) - log ↑n)) atTop (𝓝 (f x - f 1))

case refine_2
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
⊢ ∀ᶠ (b : ℕ) in atTop, f x - f 1 - x * (log (↑b + 1) - log ↑b) ≤ logGammaSeq x b

case refine_3
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
⊢ ∀ᶠ (b : ℕ) in atTop, logGammaSeq x b ≤ f x - f 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le' (f := logGammaSeq x)
    (g := fun n ↦ f x - f 1 - x * (log (n + 1) - log n)) ?_ tendsto_const_nhds ?_ ?_
  · have : f x - f 1 = f x - f 1 - x * 0 := by ring
    nth_rw 2 [this]
    exact Tendsto.sub tendsto_const_nhds (tendsto_log_nat_add_one_sub_log.const_mul _)
  · filter_upwards with n
    rw [sub_le_iff_le_add', sub_le_iff_le_add']
    convert! le_logGammaSeq hf_conv (@hf_feq) hx hx' n using 1
    ring
  · change ∀ᶠ n : ℕ in atTop, logGammaSeq x n ≤ f x - f 1
    filter_upwards [eventually_ne_atTop 0] with n hn using
      le_sub_iff_add_le'.mpr (ge_logGammaSeq hf_conv hf_feq hx hn)

Goal state after:
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
hF : (mulSupport F).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hsub : (support fun i ↦ logDeriv (F i)) ⊆ ↑hF.toFinset
⊢ logDeriv (∏ i ∈ hF.toFinset, F i) =ᶠ[codiscreteWithin U] ∑ i ∈ hF.toFinset, logDeriv (F i)

Tactic:
exact logDeriv_prod_eventuallyEq (fun i _ ↦ h i) (fun i _ ↦ h' i)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
n : ℕ
hn : n ≠ 0
| ↑n * (↑n ^ s * ↑n !) / ((↑n + 1 + s) * ((∏ k ∈ Finset.range n, (s + ↑(k + 1))) * s))

Tactic:
← mul_assoc,

Goal state after:
s : ℂ
n : ℕ
hn : n ≠ 0
| ↑n * ↑n ^ s * ↑n ! / ((↑n + 1 + s) * ((∏ k ∈ Finset.range n, (s + ↑(k + 1))) * s))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
n : ℕ
hn : n ≠ 0
| ↑n * ↑n ^ s * ↑n ! / ((↑n + 1 + s) * ((∏ k ∈ Finset.range n, (s + ↑(k + 1))) * s))

Tactic:
← mul_assoc,

Goal state after:
s : ℂ
n : ℕ
hn : n ≠ 0
| ↑n * ↑n ^ s * ↑n ! / (((↑n + 1 + s) * ∏ k ∈ Finset.range n, (s + ↑(k + 1))) * s)