mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
g : E →L[𝕜] F
⊢ ‖(commIsometry 𝕜 F G).toLinearIsometry.toContinuousLinearMap ∘SL
        rTensor G g ∘SL (commIsometry 𝕜 G E).toLinearIsometry.toContinuousLinearMap‖ ≤
    ‖g‖

Tactic:
opNorm_comp_le,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
g : E →L[𝕜] F
⊢ ‖(commIsometry 𝕜 F G).toLinearIsometry.toContinuousLinearMap‖ *
      ‖rTensor G g ∘SL (commIsometry 𝕜 G E).toLinearIsometry.toContinuousLinearMap‖ ≤
    ‖g‖
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
g : E →L[𝕜] F
⊢ ‖(commIsometry 𝕜 F G).toLinearIsometry.toContinuousLinearMap‖ *
      ‖rTensor G g ∘SL (commIsometry 𝕜 G E).toLinearIsometry.toContinuousLinearMap‖ ≤
    ‖g‖

Tactic:
opNorm_comp_le,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
g : E →L[𝕜] F
⊢ ‖(commIsometry 𝕜 F G).toLinearIsometry.toContinuousLinearMap‖ *
      (‖rTensor G g‖ * ‖(commIsometry 𝕜 G E).toLinearIsometry.toContinuousLinearMap‖) ≤
    ‖g‖
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
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
h1 : bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis = 1
h2 : (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis * bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis = 1
⊢ ‖(bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * h.some.toBasis.toMatrix ⇑bv.toBasis).det‖ *
      ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖ =
    ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖

Tactic:
suffices ‖(bu.toBasis.toMatrix (stdOrthonormalBasis 𝕜 U).toBasis *
      h.some.toBasis.toMatrix ⇑bv.toBasis).det‖ = 1 by
    rw [this, one_mul]

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
h : Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
h1 : bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis = 1
h2 : (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis * bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis = 1
⊢ ‖(bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * h.some.toBasis.toMatrix ⇑bv.toBasis).det‖ = 1
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
⊢ dimH (f '' s) ≤ dimH s / ↑r

Tactic:
borelize X Y

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
⊢ dimH (f '' s) ≤ dimH s / ↑r
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
⊢ dimH (f ⁻¹' s) ≤ dimH s

Tactic:
borelize X Y

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
⊢ dimH (f ⁻¹' s) ≤ dimH 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
f : U →ₗ[𝕜] V
tfae_1_iff_2 : f.normDet = 0 ↔ f.ker ≠ ⊥
tfae_1_iff_3 : f.normDet = 0 ↔ finrank 𝕜 ↥f.range ≠ finrank 𝕜 U
tfae_3_iff_4 : finrank 𝕜 ↥f.range ≠ finrank 𝕜 U ↔ finrank 𝕜 ↥f.range < finrank 𝕜 U
⊢ [f.normDet = 0, f.ker ≠ ⊥, finrank 𝕜 ↥f.range ≠ finrank 𝕜 U, finrank 𝕜 ↥f.range < finrank 𝕜 U,
      IsEmpty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range), ¬Function.Injective ⇑f].TFAE

Tactic:
tfae_have 3 ↔ 5 := by
    have h := (f.normDet_ne_zero_tfae.out 2 3).not
    simpa using h

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
f : U →ₗ[𝕜] V
tfae_1_iff_2 : f.normDet = 0 ↔ f.ker ≠ ⊥
tfae_1_iff_3 : f.normDet = 0 ↔ finrank 𝕜 ↥f.range ≠ finrank 𝕜 U
tfae_3_iff_4 : finrank 𝕜 ↥f.range ≠ finrank 𝕜 U ↔ finrank 𝕜 ↥f.range < finrank 𝕜 U
tfae_3_iff_5 : finrank 𝕜 ↥f.range ≠ finrank 𝕜 U ↔ IsEmpty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
⊢ [f.normDet = 0, f.ker ≠ ⊥, finrank 𝕜 ↥f.range ≠ finrank 𝕜 U, finrank 𝕜 ↥f.range < finrank 𝕜 U,
      IsEmpty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range), ¬Function.Injective ⇑f].TFAE
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
hc' : c ≠ 0
⊢ mkMetric (c • m) = c • mkMetric m

Tactic:
by
  simp only [mkMetric, mkMetric', mkMetric'.pre]
  simp_rw [smul_iSup, smul_boundedBy hc, ennreal_smul_extend _ hc', Pi.smul_apply]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : InnerProductSpace 𝕜 W
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
hf : f.ker = ⊥
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
hgf : (g ∘ₗ f).ker = ⊥
bw : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(g ∘ₗ f).range
bw' : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(g.domRestrict f.range).range :=
  bw.map (LinearIsometryEquiv.ofEq (g ∘ₗ f).range (g.domRestrict f.range).range ⋯)
⊢ (g ∘ₗ f).normDet = (g.domRestrict f.range).normDet * f.normDet

Tactic:
(g ∘ₗ f).normDet_eq_norm_det_toMatrix_rangeRestrict bu bw,

Goal state after:
case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : InnerProductSpace 𝕜 W
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
hf : f.ker = ⊥
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
hgf : (g ∘ₗ f).ker = ⊥
bw : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(g ∘ₗ f).range
bw' : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(g.domRestrict f.range).range :=
  bw.map (LinearIsometryEquiv.ofEq (g ∘ₗ f).range (g.domRestrict f.range).range ⋯)
⊢ ‖((toMatrix bu.toBasis bw.toBasis) (g ∘ₗ f).rangeRestrict).det‖ = (g.domRestrict f.range).normDet * f.normDet
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
⊢ S.mulI.mulI = S

Tactic:
ext x
  simp only [Submodule.carrier_eq_coe, coe_toSubmodule, SetLike.mem_coe]
  constructor
  · intro h
    rw [mem_mapEquiv_iff (scalarSMulCLE H UnitI), ← SetLike.forall_smul_mem_iff] at h
    simpa [← smul_assoc, Units.smul_def] using (h (-1 : ℝ))
  · intro h
    rw [← SetLike.forall_smul_mem_iff] at h
    simpa [← smul_assoc, Units.smul_def] using (h (-1 : ℝ))

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : RKHS 𝕜 H X V
inst✝² : CompleteSpace H
inst✝¹ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
x : X
v : V
⊢ ‖(kerFunAux x) v‖ ^ 2 ≤ (√‖K x x‖ * ‖v‖) ^ 2

Tactic:
simp only [LinearMap.coe_mk, AddHom.coe_mk, UniformSpace.Completion.norm_coe,
    ← inner_self_eq_norm_sq (𝕜 := 𝕜), inner_self_re_eq_norm]

Goal state after:
𝕜 : Type u_1
inst✝⁸ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : RKHS 𝕜 H X V
inst✝² : CompleteSpace H
inst✝¹ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
x : X
v : V
⊢ ‖⟪Finsupp.single (x, v) 1, Finsupp.single (x, v) 1⟫_𝕜‖ ≤ (√‖K x x‖ * ‖v‖) ^ 2
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : ↑K ^ d ≠ 0
hKd : ↑K ^ d ≠ ∞
⊢ μH[d] (f ⁻¹' s) ≤ ↑K ^ d * μH[d] s

Tactic:
simp only [hausdorffMeasure_apply, ENNReal.mul_iSup, ENNReal.mul_iInf_of_ne hKd0 hKd,
    ← ENNReal.tsum_mul_left]

Goal state after:
case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : ↑K ^ d ≠ 0
hKd : ↑K ^ d ≠ ∞
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : f ⁻¹' s ⊆ ⋃ n, t n),
            ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d ≤
    ⨆ i,
      ⨆ (_ : 0 < i),
        ⨅ i_1,
          ⨅ (_ : s ⊆ ⋃ n, i_1 n),
            ⨅ (_ : ∀ (n : ℕ), ediam (i_1 n) ≤ i), ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), ↑K ^ d * ediam (i_1 i) ^ d
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n ↦ (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f ↦ univ.pi fun i ↦ Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
⊢ μH[↑(Fintype.card ι)] (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)) ≤ ∏ x, volume ((fun i ↦ Ioo ↑(a i) ↑(b i)) x)

Tactic:
have A : Tendsto (fun n : ℕ => 1 / (n : ℝ≥0∞)) atTop (𝓝 0) := by
    simp only [one_div, ENNReal.tendsto_inv_nat_nhds_zero]

Goal state after:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n ↦ (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f ↦ univ.pi fun i ↦ Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n ↦ 1 / ↑n) atTop (𝓝 0)
⊢ μH[↑(Fintype.card ι)] (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)) ≤ ∏ x, volume ((fun i ↦ Ioo ↑(a i) ↑(b i)) x)
Module: Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E →WOT[𝕜] F
⊢ Continuous[inst✝, instTopologicalSpace] f ↔
    ∀ (x : E) (y : F), Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x_1 ↦ ⟪y, (f x_1) x⟫_𝕜

Tactic:
by
  simp_rw [continuous_iff_continuousAt, forall_comm (α := E), forall_comm (α := F),
    continuousAt_iff]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
⊢ μH[1] ((fun r ↦ r • v) '' s) = ‖v‖₊ • μH[1] s

Tactic:
obtain rfl | hv := eq_or_ne v 0

Goal state after:
case inl
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set ℝ
⊢ μH[1] ((fun r ↦ r • 0) '' s) = ‖0‖₊ • μH[1] s

case inr
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
⊢ μH[1] ((fun r ↦ r • v) '' s) = ‖v‖₊ • μH[1] s
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hf : MellinConvergent f s
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
inst✝² : SMulZeroClass 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : SMulCommClass ℂ 𝕜 E
c : 𝕜
⊢ MellinConvergent (fun t ↦ c • f t) s

Tactic:
by
  simpa only [MellinConvergent, smul_comm] using! hf.smul c

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: 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) = ↑t ^ (↑a - 1 + ↑a * (s / ↑a - 1)) • f (t ^ a)

Tactic:
mul_sub,

Goal state after:
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) = ↑t ^ (↑a - 1 + (↑a * (s / ↑a) - ↑a * 1)) • f (t ^ a)
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) = ↑t ^ (↑a - 1 + ↑a * (s / ↑a - 1)) • f (t ^ a)

Tactic:
mul_sub,

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) = ↑t ^ (↑a - 1 + (↑a * (s / ↑a) - ↑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
T : Set ℝ
hT : T ⊆ Ioi 0
hT' : MeasurableSet T
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
s : ℂ
this : AEStronglyMeasurable (fun t ↦ ↑t ^ (s - 1) • f t) (volume.restrict T)
⊢ IntegrableOn (fun a ↦ ‖↑a ^ (s - 1) • f a‖) T volume ↔ IntegrableOn (fun t ↦ t ^ (s.re - 1) * ‖f t‖) T volume

Tactic:
refine integrableOn_congr_fun (fun t ht => ?_) hT'

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
T : Set ℝ
hT : T ⊆ Ioi 0
hT' : MeasurableSet T
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
s : ℂ
this : AEStronglyMeasurable (fun t ↦ ↑t ^ (s - 1) • f t) (volume.restrict T)
t : ℝ
ht : t ∈ T
⊢ ‖↑t ^ (s - 1) • f t‖ = t ^ (s.re - 1) * ‖f t‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
H : -z = 1
⊢ False

Tactic:
neg_eq_iff_eq_neg

Goal state after:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
H : z = -1
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
⊢ Γ (a * s + b * t) ≤ Γ s ^ a * Γ t ^ b

Tactic:
have posf : ∀ c u x : ℝ, x ∈ Ioi (0 : ℝ) → 0 ≤ f c u x := fun c u x hx =>
    mul_nonneg (exp_pos _).le (rpow_pos_of_pos hx _).le

Goal state after:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
⊢ Γ (a * s + b * t) ≤ Γ s ^ a * Γ t ^ b
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp : ∀ {c u : ℝ}, 0 < c → 0 < u → MemLp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
⊢ rexp (-x) = rexp (-a * x) * rexp (-b * x)

Tactic:
rw [← exp_add, ← add_mul, ← neg_add, hab, neg_one_mul]

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

Goal state before:
pp: case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ (↑a - ↑x) ^ (t - 1) = (↑a * (1 - ↑x / ↑a)) ^ (t - 1)

Tactic:
mul_sub,

Goal state after:
case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ (↑a - ↑x) ^ (t - 1) = (↑a * 1 - ↑a * (↑x / ↑a)) ^ (t - 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
⊢ Tendsto
    (fun n ↦
      ↑(∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n ∂volume)⁻¹ * ∫ (x : ℝ) in Icc 0 (π / 2), ↑(cos x) ^ n * f x ∂volume)
    atTop (𝓝 (f 0))

Tactic:
← Complex.ofReal_pow,

Goal state after:
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
⊢ Tendsto
    (fun n ↦
      ↑(∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n ∂volume)⁻¹ * ∫ (x : ℝ) in Icc 0 (π / 2), ↑(cos x ^ n) * f x ∂volume)
    atTop (𝓝 (f 0))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_2
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
e1 : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x - (log ∘ f) 1))
⊢ (log ∘ f) x = (log ∘ Γ) x

Tactic:
rw [Function.comp_apply (f := log) (g := f) (x := 1), hf_one, log_one, sub_zero] at e1
    exact tendsto_nhds_unique e1 (BohrMollerup.tendsto_log_gamma hx)

Goal state after:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case a
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ ⨆ p, atTop • 𝓝 v +ᵥ pure p ≤ atTop • 𝓝 v

pp: case a
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ atTop • 𝓝 v ≤ ⨆ p, atTop • 𝓝 v +ᵥ pure p

Tactic:
· refine iSup_le fun u => ?_
    simp_rw [vadd_eq_add, add_pure, ← map₂_smul, map_map₂, ← map_prod_eq_map₂]
    have : (fun x : k × V => x.1 • x.2 + u) =ᶠ[atTop ×ˢ 𝓝 v]
        (Function.uncurry (· • ·)) ∘ (fun x : k × V => (x.1, x.2 + x.1⁻¹ • u)) := by
      filter_upwards [tendsto_fst.eventually (eventually_ne_atTop 0)] with _ h
      simp [h]
    rw [map_congr this, ← map_map]
    apply map_mono
    have : Tendsto (fun x : k × V => (x.1, x.2 + x.1⁻¹ • u)) (atTop ×ˢ 𝓝 v) _ :=
      tendsto_fst.prodMk <| tendsto_snd.add <| tendsto_fst.inv_tendsto_atTop.smul_const u
    simpa

Goal state after:
case a
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ atTop • 𝓝 v ≤ ⨆ p, atTop • 𝓝 v +ᵥ pure p
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
⊢ s.GammaSeq n = ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1)

Tactic:
GammaSeq_eq_betaIntegral_of_re_pos hs

Goal state after:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
⊢ ↑n ^ s * s.betaIntegral (↑n + 1) = ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1)
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
p : P → Prop
⊢ (∀ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, ∀ᶠ (y : P) in asymptoticNhds k P (a.1 • a.2), p y) ↔
    ∀ᶠ (x : P) in (𝓝 v).bind (asymptoticNhds k P), p x

Tactic:
eventually_bind

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
p : P → Prop
⊢ (∀ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, ∀ᶠ (y : P) in asymptoticNhds k P (a.1 • a.2), p y) ↔
    ∀ᶠ (x : V) in 𝓝 v, ∀ᶠ (y : P) in asymptoticNhds k P x, p y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case pos
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : -z = ↑k
⊢ Gamma z * Gamma (1 - z) = 0

Tactic:
neg_eq_iff_eq_neg

Goal state after:
case pos
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : z = -↑k
⊢ Gamma z * Gamma (1 - z) = 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e'_3
s : ℂ
this : (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π = ((Gamma (2 * s))⁻¹ * 2 ^ (2 * s - 1) / ↑√π)⁻¹

Tactic:
div_eq_mul_inv,

Goal state after:
case e'_3
s : ℂ
this : (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π = ((Gamma (2 * s))⁻¹ * 2 ^ (2 * s - 1) * (↑√π)⁻¹)⁻¹