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
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
g : G →L[𝕜] H
⊢ ↑(mapL f g) = map ↑f ↑g

Tactic:
ext; simp

Goal state after:
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 →ₗᵢ[𝕜] F
g : G →ₗᵢ[𝕜] H
⊢ (mapIsometry f g).toContinuousLinearMap = mapL f.toContinuousLinearMap g.toContinuousLinearMap

Tactic:
ext; simp

Goal state after:
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
A : Type u_6
inst✝¹ : NormedAddCommGroup A
inst✝ : InnerProductSpace 𝕜 A
f₁ : E →L[𝕜] F
f₂ : A →L[𝕜] E
g : G →L[𝕜] H
⊢ mapL f₁ g ∘SL ContinuousLinearMap.rTensor G f₂ = mapL (f₁ ∘SL f₂) g

Tactic:
ext; simp

Goal state after:
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
A : Type u_6
inst✝¹ : NormedAddCommGroup A
inst✝ : InnerProductSpace 𝕜 A
f : E →L[𝕜] F
g₁ : G →L[𝕜] H
g₂ : A →L[𝕜] G
⊢ mapL f g₁ ∘SL ContinuousLinearMap.lTensor E g₂ = mapL f (g₁ ∘SL g₂)

Tactic:
ext; simp

Goal state after:
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
A : Type u_6
inst✝¹ : NormedAddCommGroup A
inst✝ : InnerProductSpace 𝕜 A
f₁ : E →L[𝕜] F
f₂ : A →L[𝕜] E
g : G →L[𝕜] H
⊢ ContinuousLinearMap.rTensor H f₁ ∘SL mapL f₂ g = mapL (f₁ ∘SL f₂) g

Tactic:
ext; simp

Goal state after:
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
A : Type u_6
inst✝¹ : NormedAddCommGroup A
inst✝ : InnerProductSpace 𝕜 A
f : E →L[𝕜] F
g₁ : G →L[𝕜] H
g₂ : A →L[𝕜] G
⊢ ContinuousLinearMap.lTensor F g₁ ∘SL mapL f g₂ = mapL f (g₁ ∘SL g₂)

Tactic:
ext; simp

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

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
s : Set X
h : s.Subsingleton
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ dimH s = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
s : Set X
h : s.Subsingleton
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ dimH s ≤ 0
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h₁ : ‖x - x‖ = 0
⊢ x + x = 2 • x

Tactic:
module

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

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
⊢ (mkMetric m) s =
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n))

Tactic:
classical
  -- We mostly unfold the definitions but we need to switch the order of `∑'` and `⨅`
  simp only [← OuterMeasure.coe_mkMetric, OuterMeasure.mkMetric, OuterMeasure.mkMetric',
    OuterMeasure.iSup_apply, OuterMeasure.mkMetric'.pre, OuterMeasure.boundedBy_apply, extend]
  refine
    surjective_id.iSup_congr id fun r =>
      iSup_congr_Prop Iff.rfl fun _ =>
        surjective_id.iInf_congr _ fun t => iInf_congr_Prop Iff.rfl fun ht => ?_
  dsimp
  by_cases htr : ∀ n, ediam (t n) ≤ r
  · rw [iInf_eq_if, if_pos htr]
    congr 1 with n : 1
    simp only [iInf_eq_if, htr n, if_true]
  · rw [iInf_eq_if, if_neg htr]
    push Not at htr; rcases htr with ⟨n, hn⟩
    refine ENNReal.tsum_eq_top_of_eq_top ⟨n, ?_⟩
    rw [iSup_eq_if, if_pos, iInf_eq_if, if_neg]
    · exact hn.not_ge
    rcases ediam_pos_iff.1 hn.pos with ⟨x, hx, -⟩
    exact ⟨x, hx⟩

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

Goal state before:
pp: case a
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
hI : ¬I = 0
hI' : I * I = -1
I_smul : ∀ (v : E), ‖I • v‖ = ‖v‖
⊢ I • y - x + (I * I) • x - (I • (I • x + y) + -1 • x) = 0

Tactic:
module

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

Goal state before:
pp: case a
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
hI : ¬I = 0
hI' : I * I = -1
I_smul : ∀ (v : E), ‖I • v‖ = ‖v‖
h₁ : ‖I • y - x‖ = ‖I • x + y‖
⊢ I • x - y + (I * I) • y - (I • (I • y + x) + -1 • y) = 0

Tactic:
module

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
⊢ inner_ 𝕜 (↑(re r) • x + (↑(im r) * I) • x) y = (starRingEnd 𝕜) (↑(re r) + ↑(im r) * I) * inner_ 𝕜 x y

Tactic:
add_left,

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
⊢ inner_ 𝕜 (↑(re r) • x) y + inner_ 𝕜 ((↑(im r) * I) • x) y = (starRingEnd 𝕜) (↑(re r) + ↑(im r) * I) * inner_ 𝕜 x y
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
⊢ μH[d] (f ⁻¹' s) ≤ ↑K ^ d * μH[d] s

Tactic:
have hKd : (K : ℝ≥0∞) ^ d ≠ ∞ := by simp [hd]

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 ≠ ∞
⊢ μH[d] (f ⁻¹' s) ≤ ↑K ^ d * μH[d] s
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 ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
this : μH[1] ((fun x ↦ ‖v‖ • x) '' ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s) = ‖v‖₊ • μH[1] s
⊢ μH[1] ((fun r ↦ r • v) '' s) = ‖v‖₊ • μH[1] s

Tactic:
by
    simpa only [Set.image_image, smul_comm (norm _), inv_smul_smul₀ hn,
      LinearMap.toSpanSingleton_apply] using this

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ o.rightAngleRotation.trans o.rightAngleRotation = LinearIsometryEquiv.neg ℝ

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁹ : NormedField 𝕜₁
inst✝⁸ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜₂ F
x y : E →SWOT[σ] F
⊢ (fun x_1 ↦
      match x_1 with
      | (x_2, y_1) => y_1 ((x + y) x_2)) =
    (fun x_1 ↦
        match x_1 with
        | (x_2, y) => y (x x_2)) +
      fun x ↦
      match x with
      | (x, y_1) => y_1 (y x)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁹ : NormedField 𝕜₁
inst✝⁸ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜₂ F
x : 𝕜₂
y : E →SWOT[σ] F
⊢ (fun x_1 ↦
      match x_1 with
      | (x_2, y_1) => y_1 ((x • y) x_2)) =
    (RingHom.id 𝕜₂) x • fun x ↦
      match x with
      | (x, y_1) => y_1 (y x)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁✝ : Type u_1
𝕜₂✝ : Type u_2
inst✝³¹ : NormedField 𝕜₁✝
inst✝³⁰ : NormedField 𝕜₂✝
σ : 𝕜₁✝ →+* 𝕜₂✝
E✝ : Type u_3
F✝ : Type u_4
inst✝²⁹ : AddCommGroup E✝
inst✝²⁸ : TopologicalSpace E✝
inst✝²⁷ : Module 𝕜₁✝ E✝
inst✝²⁶ : AddCommGroup F✝
inst✝²⁵ : TopologicalSpace F✝
inst✝²⁴ : Module 𝕜₂✝ F✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²³ : NormedField 𝕜₁
inst✝²² : NormedField 𝕜₂
inst✝²¹ : NormedField 𝕜₃
inst✝²⁰ : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : AddCommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : AddCommGroup H
inst✝⁵ : TopologicalSpace H
inst✝⁴ : Module 𝕜₄ H
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
x✝ : F →WOT[𝕜₂] F
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun x ↦ x✝ * x

Tactic:
by simp_rw [mul_eq_comp]; fun_prop

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
hf : MellinConvergent f ↑σ
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
⊢ mellinInv σ (mellin f) x = f x

Tactic:
by
  let g := fun (u : ℝ) => Real.exp (-σ * u) • f (Real.exp (-u))
  replace hf : Integrable g := by
    rw [MellinConvergent, ← rexp_neg_image_aux, integrableOn_image_iff_integrableOn_abs_deriv_smul
      MeasurableSet.univ rexp_neg_deriv_aux rexp_neg_injOn_aux] at hf
    replace hf : Integrable fun (x : ℝ) ↦ cexp (-↑σ * ↑x) • f (rexp (-x)) := by
      simpa [rexp_cexp_aux] using hf
    norm_cast at hf
  replace hFf : Integrable (𝓕 g) := by
    have h2π : 2 * π ≠ 0 := by simp
    have : Integrable (𝓕 (fun u ↦ rexp (-(σ * u)) • f (rexp (-u)))) := by
      simpa [mellin_eq_fourier, mul_div_cancel_right₀ _ h2π] using hFf.comp_mul_right' h2π
    simp_rw [neg_mul_eq_neg_mul] at this
    exact this
  replace hfx : ContinuousAt g (-Real.log x) := by
    refine ContinuousAt.fun_smul (by fun_prop) (ContinuousAt.comp ?_ (by fun_prop))
    simpa [Real.exp_log hx] using hfx
  calc
    mellinInv σ (mellin f) x
      = mellinInv σ (fun s ↦ 𝓕 g (s.im / (2 * π))) x := by
      simp [g, mellinInv, mellin_eq_fourier]
    _ = (x : ℂ) ^ (-σ : ℂ) • g (-Real.log x) := by
      rw [mellinInv_eq_fourierInv _ _ hx, ← hf.fourierInv_fourier_eq hFf hfx]
      simp [mul_div_cancel_left₀ _ (show 2 * π ≠ 0 by simp)]
    _ = (x : ℂ) ^ (-σ : ℂ) • rexp (σ * Real.log x) • f (rexp (Real.log x)) := by simp [g]
    _ = f x := by
      norm_cast
      rw [mul_comm σ, ← rpow_def_of_pos hx, Real.exp_log hx, ← Complex.ofReal_cpow hx.le]
      norm_cast
      rw [← smul_assoc, smul_eq_mul, Real.rpow_neg hx.le,
        inv_mul_cancel₀ (ne_of_gt (rpow_pos_of_pos hx σ)), one_smul]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁✝ : Type u_1
𝕜₂✝ : Type u_2
inst✝³¹ : NormedField 𝕜₁✝
inst✝³⁰ : NormedField 𝕜₂✝
σ : 𝕜₁✝ →+* 𝕜₂✝
E✝ : Type u_3
F✝ : Type u_4
inst✝²⁹ : AddCommGroup E✝
inst✝²⁸ : TopologicalSpace E✝
inst✝²⁷ : Module 𝕜₁✝ E✝
inst✝²⁶ : AddCommGroup F✝
inst✝²⁵ : TopologicalSpace F✝
inst✝²⁴ : Module 𝕜₂✝ F✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²³ : NormedField 𝕜₁
inst✝²² : NormedField 𝕜₂
inst✝²¹ : NormedField 𝕜₃
inst✝²⁰ : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : AddCommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : AddCommGroup H
inst✝⁵ : TopologicalSpace H
inst✝⁴ : Module 𝕜₄ H
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
x✝ : F →WOT[𝕜₂] F
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun x ↦ x * x✝

Tactic:
by simp_rw [mul_eq_comp]; fun_prop

Goal state after:
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 : ℂ
⊢ IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f t) T volume ↔ IntegrableOn (fun t ↦ t ^ (s.re - 1) * ‖f t‖) T volume

Tactic:
have : AEStronglyMeasurable (fun t : ℝ => (t : ℂ) ^ (s - 1) • f t) (volume.restrict T) := by
    refine ((continuousOn_of_forall_continuousAt ?_).aestronglyMeasurable hT').smul
      (hfc.mono_set hT)
    exact fun t ht => continuousAt_ofReal_cpow_const _ _ (Or.inr <| ne_of_gt (hT ht))
  rw [IntegrableOn, ← integrable_norm_iff this, ← IntegrableOn]
  refine integrableOn_congr_fun (fun t ht => ?_) hT'
  simp_rw [norm_smul, norm_cpow_eq_rpow_re_of_pos (hT ht), sub_re, one_re]

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

Goal state before:
pp: n : ℕ
ih : ¬ContinuousAt Gamma (-↑n)
⊢ ¬ContinuousAt Gamma (-↑(n + 1))

Tactic:
contrapose ih

Goal state after:
n : ℕ
ih : ContinuousAt Gamma (-↑(n + 1))
⊢ ContinuousAt Gamma (-↑n)
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)⁻¹
⊢ ‖∫ (t : ℝ) in 0..1, ↑t ^ n * (1 + ↑t * z)⁻¹‖ ≤ ∫ (t : ℝ) in 0..1, t ^ n * (1 - ‖z‖)⁻¹

Tactic:
by
      refine intervalIntegral.norm_integral_le_of_norm_le zero_le_one ?_ help
      filter_upwards with t ⟨ht₀, ht₁⟩
      rw [norm_mul, norm_pow, Complex.norm_of_nonneg ht₀.le]
      gcongr
      exact norm_one_add_mul_inv_le ⟨ht₀.le, ht₁⟩ hz

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: f : ℕ → ℂ
t : ℂ
hf : (fun n ↦ f n - (1 + t / ↑n)) =o[atTop] fun n ↦ 1 / ↑n
⊢ (fun n ↦ f n ^ n) = fun n ↦ (1 + (f n - 1)) ^ n

Tactic:
ext; simp

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

Goal state before:
pp: n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ (∫ (x : ℝ) in 0..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0..π / 2, cos x ^ n = ∫ (x : ℝ) in 0..π, sin x ^ n

Tactic:
← integral_add_adjacent_intervals L R

Goal state after:
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ (∫ (x : ℝ) in 0..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0..π / 2, cos x ^ n =
    (∫ (x : ℝ) in 0..π / 2, sin x ^ n) + ∫ (x : ℝ) in π / 2..π, sin x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (log (Γ x)))

Tactic:
by
  have : log (Gamma x) = (log ∘ Gamma) x - (log ∘ Gamma) 1 := by
    simp_rw [Function.comp_apply, Gamma_one, log_one, sub_zero]
  rw [this]
  refine BohrMollerup.tendsto_logGammaSeq convexOn_log_Gamma (fun {y} hy => ?_) hx
  rw [Function.comp_apply, Gamma_add_one hy.ne', log_mul hy.ne' (Gamma_pos_of_pos hy).ne', add_comm,
    Function.comp_apply]

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

Goal state before:
pp: s : ℝ
hs : s ∈ Ioi 0
h1 : √π ≠ 0
h2 : Γ (s / 2) ≠ 0
h3 : Γ (s / 2 + 1 / 2) ≠ 0
h4 : 2 ^ (s - 1) ≠ 0
⊢ (log ∘ doublingGamma) s = (fun s ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s

Tactic:
rw [Function.comp_apply, doublingGamma, log_div (mul_ne_zero (mul_ne_zero h2 h3) h4) h1,
    log_mul (mul_ne_zero h2 h3) h4, log_mul h2 h3, log_rpow two_pos, log_mul two_ne_zero h1]

Goal state after:
s : ℝ
hs : s ∈ Ioi 0
h1 : √π ≠ 0
h2 : Γ (s / 2) ≠ 0
h3 : Γ (s / 2 + 1 / 2) ≠ 0
h4 : 2 ^ (s - 1) ≠ 0
⊢ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + (s - 1) * log 2 - log √π =
    (fun s ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - (log 2 + log √π)) s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: ⊢ ConvexOn ℝ (Ioi 0) (log ∘ doublingGamma)

Tactic:
refine (((ConvexOn.add ?_ ?_).add ?_).add_const _).congr log_doublingGamma_eq.symm
  · convert!
      convexOn_log_Gamma.comp_affineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap
      using 1
    · simpa only [zero_div] using! (preimage_const_mul_Ioi₀ (0 : ℝ) one_half_pos).symm
    · ext1 x
      simp only [LinearMap.coe_toAffineMap, Function.comp_apply, DistribSMul.toLinearMap_apply]
      rw [smul_eq_mul, mul_comm, mul_one_div]
  · refine ConvexOn.subset ?_ (Ioi_subset_Ioi <| neg_one_lt_zero.le) (convex_Ioi _)
    convert!
      convexOn_log_Gamma.comp_affineMap
        ((DistribSMul.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap +
          AffineMap.const ℝ ℝ (1 / 2 : ℝ)) using 1
    · change Ioi (-1 : ℝ) = ((fun x : ℝ => x + 1 / 2) ∘ fun x : ℝ => (1 / 2 : ℝ) * x) ⁻¹' Ioi 0
      rw [preimage_comp, preimage_add_const_Ioi, zero_sub,
        preimage_const_mul_Ioi₀ (_ : ℝ) one_half_pos, neg_div, div_self (@one_half_pos ℝ _).ne']
    · ext1 x
      change log (Gamma (x / 2 + 1 / 2)) = log (Gamma ((1 / 2 : ℝ) • x + 1 / 2))
      rw [smul_eq_mul, mul_comm, mul_one_div]
  · simpa only [mul_comm _ (log _)] using!
      (convexOn_id (convex_Ioi (0 : ℝ))).smul (log_pos one_lt_two).le

Goal state after:
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
⊢ ∀ᶠ (x : k × V) in atTop ×ˢ 𝓝 v,
    (∀ᶠ (y : P) in asymptoticNhds k P (x.1 • x.2), p y) ↔ ∀ᶠ (y : P) in asymptoticNhds k P x.2, p y

Tactic:
filter_upwards [tendsto_fst.eventually (eventually_gt_atTop 0)] with ⟨c, u⟩ (hc : 0 < c)

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
c : k
u : V
hc : 0 < c
⊢ (∀ᶠ (y : P) in asymptoticNhds k P ((c, u).1 • (c, u).2), p y) ↔ ∀ᶠ (y : P) in asymptoticNhds k P (c, u).2, p y
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
this :
  ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
hn' : ↑n ≠ 0
A : ↑n ^ s = ↑n ^ (s - 1) * ↑n
⊢ (↑x * ↑↑n) ^ (s - 1) = ↑x ^ (s - 1) * ↑↑n ^ (s - 1)

Tactic:
mul_cpow_ofReal_nonneg hx.1.le (Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)).le

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

Goal state before:
pp: 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
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
v : V
⊢ v ∈ asymptoticCone k s ↔ v ∈ closure[inst✝⁵] s

Tactic:
rw [mem_closure_iff_frequently, ← map_snd_prod (atTop (α := k)) (𝓝 v), frequently_map,
    mem_asymptoticCone_iff, asymptoticNhds_eq_smul, ← map₂_smul, ← map_prod_eq_map₂, frequently_map]

Goal state after:
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
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
v : V
⊢ (∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 ∈ s) ↔ ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.2 ∈ s
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s✝ s : Set V
hs : Convex k s
hs' : IsClosed[inst✝²] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
h₁ : c • v +ᵥ p ∈ s
h₂ : c • u +ᵥ p ∈ s
⊢ a • c • v + b • c • u = (c * a) • v + (c * b) • u

Tactic:
module

Goal state after: