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
⊢ (∫⁻ (y : ι → ℝ), ‖fderiv ℝ u (e.symm y) ∘SL fderiv ℝ (⇑e.symm) y‖ₑ) ^ p ≤
    (∫⁻ (y : ι → ℝ), ‖fderiv ℝ u (e.symm y)‖ₑ * ‖↑e.symm‖ₑ) ^ p

Tactic:
gcongr with y
        rw [e.symm.fderiv]
        apply ContinuousLinearMap.opENorm_comp_le

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

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
⊢ f ≤ f.closure

Tactic:
by
  by_cases hf : f.IsClosable
  · refine le_of_le_graph ?_
    rw [← hf.graph_closure_eq_closure_graph]
    exact (graph f).le_topologicalClosure
  rw [closure_def' hf]

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

Goal state before:
pp: case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
h : f.closure.toFun.ker = ⊥
⊢ f.inverse.graph.topologicalClosure = f.closure.inverse.graph

Tactic:
exact (closure_inverse_graph hf hf' h).symm

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
y : ↥T†.domain
⊢ (if hT : Dense ↑T.domain then adjointAux hT else 0) y = (adjointAux hT) y

Tactic:
simp only [hT, dif_pos]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x y : E ⊗[𝕜] F
x✝¹ : E
x✝ : F
⊢ ∀ (x : E) (y : F),
    inner 𝕜 ((TensorProduct.comm 𝕜 E F) (x✝¹ ⊗ₜ[𝕜] x✝)) ((TensorProduct.comm 𝕜 E F) (x ⊗ₜ[𝕜] y)) =
      inner 𝕜 (x✝¹ ⊗ₜ[𝕜] x✝) (x ⊗ₜ[𝕜] y)

Tactic:
by simp [mul_comm]

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 →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) -
        ∑ 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:
map_sub,

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)) ≤
    ‖f‖ ^ 2 * RCLike.re (∑ x, ∑ i, inner 𝕜 (e i) (e x) * inner 𝕜 (g i) (g x))
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
inst✝ : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖↑e.symm‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ ↑p
C₂ : ℝ≥0 := ‖↑e‖₊
v : E → F' := ⇑e ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ eLpNorm u (↑p') μ ≤ ↑(SNormLESNormFDerivOfEqConst F μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
have := eLpNorm_le_eLpNorm_fderiv_of_eq_inner μ hv h2v hp hn hp'

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
inst✝ : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖↑e.symm‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ ↑p
C₂ : ℝ≥0 := ‖↑e‖₊
v : E → F' := ⇑e ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this : eLpNorm v (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ v) (↑p) μ
⊢ eLpNorm u (↑p') μ ≤ ↑(SNormLESNormFDerivOfEqConst F μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case pos
𝕜 : 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 ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
⊢ f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖

pp: case neg
𝕜 : 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 ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U ≠ finrank 𝕜 ↥f.range
⊢ f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖

Tactic:
· have h : f.range = ⊤ := by
      apply Submodule.eq_of_le_of_finrank_le le_top
      simp [finrank_eq_card_basis bv.toBasis, ← hrank, finrank_eq_card_basis bu.toBasis]
    let bv' : OrthonormalBasis ι 𝕜 f.range := bv.map (LinearIsometryEquiv.ofTop _ _ h).symm
    rw [f.normDet_eq_norm_det_toMatrix_rangeRestrict bu bv']
    rfl

Goal state after:
case neg
𝕜 : 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 ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U ≠ finrank 𝕜 ↥f.range
⊢ f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖
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∞
⊢ (mkMetric m).trim = mkMetric m

Tactic:
simp only [mkMetric, mkMetric'.eq_iSup_nat, trim_iSup]
  congr 1 with n : 1
  refine mkMetric'.trim_pre _ (fun s => ?_) _
  simp

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₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
s : Set X
⊢ (OuterMeasure.mkMetric m₁) s ≤ (c • ⇑(mkMetric m₂)) s

Tactic:
← OuterMeasure.coe_mkMetric

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
s : Set X
⊢ (OuterMeasure.mkMetric m₁) s ≤ (c • ⇑(OuterMeasure.mkMetric m₂)) s
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ∞
⊢ ∀ (c : ℝ≥0), c ≠ 0 → μH[d₂] s ≤ ↑c * μH[d₁] s

Tactic:
intro c

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ∞
c : ℝ≥0
⊢ c ≠ 0 → μH[d₂] s ≤ ↑c * μH[d₁] s
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : 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
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
h : finrank 𝕜 U = finrank 𝕜 V
htop : ¬f.range = ⊤
hker : f.ker ≠ ⊥
⊢ (g ∘ₗ f).ker ≠ ⊥

Tactic:
contrapose hker with hbot

Goal state after:
𝕜 : 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
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
h : finrank 𝕜 U = finrank 𝕜 V
htop : ¬f.range = ⊤
hbot : (g ∘ₗ f).ker = ⊥
⊢ f.ker = ⊥
Module: Mathlib.Analysis.InnerProductSpace.Reproducing

Goal state before:
pp: case refine_1
𝕜 : 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
s : X →₀ V →L[𝕜] V
⊢ (s.sum fun i m ↦ star (fun i xi ↦ s.sum fun j xj ↦ star xi * kernel H i j * xj) i m) =
    s.sum fun x' v' ↦ s.sum fun x v ↦ star v * kernel H x x' * v'

Tactic:
simp [← mul_assoc, (isHermitian_kernel H).apply]

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

Goal state before:
pp: H : Type u_1
inst✝¹ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S T : ClosedSubmodule ℝ H
⊢ (S ⊓ T).symplComp = S.symplComp ⊔ T.symplComp

Tactic:
rw [symplComp, symplComp, symplComp, mulI_inf]
  exact Eq.symm (sup_orthogonal S.mulI T.mulI)

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

Goal state before:
pp: 𝕜 : 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)
f : H →L[𝕜] H
hf : f.IsPositive
⊢ ∀ x ∈ spectrum ℝ f, 0 ≤ x

Tactic:
intro c

Goal state after:
𝕜 : 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)
f : H →L[𝕜] H
hf : f.IsPositive
c : ℝ
⊢ c ∈ spectrum ℝ f → 0 ≤ c
Module: Mathlib.Analysis.InnerProductSpace.StarOrder

Goal state before:
pp: 𝕜 : 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)
f : H →L[𝕜] H
hf : f.IsPositive
c✝ : ℝ
c : ℝ := -c✝
hc : 0 < c
x : H
⊢ re ⟪((algebraMap ℝ (H →L[𝕜] H)) c) x, x⟫_𝕜 ≤ re ⟪(f + (algebraMap ℝ (H →L[𝕜] H)) c) x, x⟫_𝕜

Tactic:
by
      simpa only [add_apply, inner_add_left, map_add, le_add_iff_nonneg_left]
        using hf.re_inner_nonneg_left x

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

Goal state before:
pp: case mp
𝕜 : 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
h : (g - f).IsPositive
p : H →L[𝕜] H
hp₁ : IsSelfAdjoint p
hp₃ : p * p = g - f
⊢ p ^ 2 ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)

Tactic:
exact AddSubmonoid.subset_closure ⟨p, by simp only [hp₁.star_eq, sq]⟩

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ μH[d] (⇑(AffineMap.homothety x c) ⁻¹' s) = ‖c‖₊⁻¹ ^ d • μH[d] s

Tactic:
change μH[d] (AffineEquiv.homothetyUnitsMulHom x (Units.mk0 c hc) ⁻¹' s) = _
  rw [← AffineEquiv.image_symm, AffineEquiv.coe_homothetyUnitsMulHom_apply_symm,
    hausdorffMeasure_homothety_image hd x (_ : 𝕜ˣ).isUnit.ne_zero, Units.val_inv_eq_inv_val,
    Units.val_mk0, nnnorm_inv]

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

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✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : IsTopologicalAddGroup E
inst✝⁷ : ContinuousSMul 𝕜₁ E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₂ F
inst✝¹ : T1Space E
inst✝ : MontelSpace 𝕜₁ E
s : Set (E →SL_c[σ] F)
hs : IsOpen[UniformConvergenceCLM.instTopologicalSpace σ F {S | IsCompact S}] s
⊢ topologicalSpace ≤ UniformConvergenceCLM.instTopologicalSpace σ F {S | IsCompact S}

Tactic:
apply UniformConvergenceCLM.topologicalSpace_mono

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : IsTopologicalAddGroup E
inst✝⁷ : ContinuousSMul 𝕜₁ E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₂ F
inst✝¹ : T1Space E
inst✝ : MontelSpace 𝕜₁ E
s : Set (E →SL_c[σ] F)
hs : IsOpen[UniformConvergenceCLM.instTopologicalSpace σ F {S | IsCompact S}] s
⊢ {S | IsCompact S} ⊆ {S | IsVonNBounded 𝕜₁ S}
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ ((o.kahler x) a * (o.kahler a) y).im = (↑(‖a‖ ^ 2) * (o.kahler x) y).im

Tactic:
· simp only [o.kahler_apply_apply, Complex.add_im, Complex.add_re, Complex.I_im, Complex.I_re,
        Complex.mul_im, Complex.mul_re, Complex.ofReal_im, Complex.ofReal_re, Complex.real_smul]
      rw [real_inner_comm a x, o.areaForm_swap x a]
      linear_combination o.inner_mul_areaForm_sub a x y

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 : 0 < a
this :
  IntegrableOn (fun x ↦ ↑(a * x) ^ (s - 1) • f (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f t) (Ioi (a * 0)) volume
⊢ MellinConvergent (fun t ↦ f (a * t)) s ↔ MellinConvergent f s

Tactic:
mul_zero

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x ↦ ↑(a * x) ^ (s - 1) • f (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f t) (Ioi 0) volume
⊢ MellinConvergent (fun t ↦ f (a * t)) s ↔ MellinConvergent f s
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : 1 + -z ∈ slitPlane
⊢ -log (1 + -z) = z * ∫ (t : ℝ) in 0..1, (1 - t • z)⁻¹

Tactic:
neg_eq_iff_eq_neg,

Goal state after:
z : ℂ
hz : 1 + -z ∈ slitPlane
⊢ log (1 + -z) = -(z * ∫ (t : ℝ) in 0..1, (1 - t • z)⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case pos
m : ℕ
hs : -↑m ≠ 0
⊢ 0 = -↑m * 0

pp: case pos
m : ℕ
hs : -↑m ≠ 0
⊢ 1 ≤ m

Tactic:
mul_zero

Goal state after:
case pos
m : ℕ
hs : -↑m ≠ 0
⊢ 0 = 0

case pos
m : ℕ
hs : -↑m ≠ 0
⊢ 1 ≤ m
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
⊢ ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)

Tactic:
intro c

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
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
c : ℝ
⊢ ∀ {x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
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)
⊢ ∀ {c u : ℝ}, 0 < c → 0 < u → MemLp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))

Tactic:
intro c

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
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)
c : ℝ
⊢ ∀ {u : ℝ}, 0 < c → 0 < u → MemLp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))
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:
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.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)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x ↦ x ^ (c * (u - 1))) x

Tactic:
exact continuousAt_rpow_const _ _ (Or.inl (mem_Ioi.mp hx).ne')

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

Goal state before:
pp: u : ℂ
hu : 0 < u.re
⊢ -1 < u.re - 1

Tactic:
← sub_pos,

Goal state after:
u : ℂ
hu : 0 < u.re
⊢ 0 < u.re - 1 - -1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: u : ℂ
hu : 0 < u.re
n : ℕ
⊢ u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)

Tactic:
induction n generalizing u with
  | zero =>
    rw [Nat.cast_zero, zero_add, betaIntegral_eval_one_right hu, Nat.factorial_zero, Nat.cast_one]
    simp
  | succ n IH =>
    have := betaIntegral_recurrence hu (?_ : 0 < re n.succ)
    swap; · rw [← ofReal_natCast, ofReal_re]; positivity
    rw [mul_comm u _, ← eq_div_iff] at this
    swap; · contrapose! hu; rw [hu, zero_re]
    rw [this, Finset.prod_range_succ', Nat.cast_succ, IH]
    swap; · rw [add_re, one_re]; positivity
    rw [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one, Nat.cast_zero, add_zero, ←
      mul_div_assoc, ← div_div]
    congr 3 with j : 1
    push_cast; abel

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
s : Set P
c : k
v : V
hc : 0 ≤ c
h : v ∈ asymptoticCone k s
⊢ c • v ∈ asymptoticCone k s

Tactic:
rcases hc.eq_or_lt with rfl | hc
  · rw [zero_smul, zero_mem_asymptoticCone, ← asymptoticCone_nonempty (k := k)]; exact ⟨v, h⟩
  · rwa [smul_mem_asymptoticCone_iff hc]

Goal state after: