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

Goal state before:
pp: case e'_4.e'_5
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p' : ℝ≥0
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
n' : ℝ≥0 := (↑n).conjExponent
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hp : 1 ≤ 1
hp' : (↑p')⁻¹ = ↑1⁻¹ - (↑n)⁻¹
h2p : ↑1 < ↑n
hnp : 0 < ↑n - ↑1
⊢ eLpNormLESNormFDerivOfEqInnerConst μ 1 = eLpNormLESNormFDerivOneConst μ ↑n'

Tactic:
simp_rw [n', n, eLpNormLESNormFDerivOfEqInnerConst]

Goal state after:
case e'_4.e'_5
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p' : ℝ≥0
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
n' : ℝ≥0 := (↑n).conjExponent
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hp : 1 ≤ 1
hp' : (↑p')⁻¹ = ↑1⁻¹ - (↑n)⁻¹
h2p : ↑1 < ↑n
hnp : 0 < ↑n - ↑1
⊢ eLpNormLESNormFDerivOneConst μ ↑(↑(finrank ℝ E)).conjExponent *
      (1 * (↑(finrank ℝ E) - 1) / (↑(finrank ℝ E) - 1)).toNNReal =
    eLpNormLESNormFDerivOneConst μ ↑(↑(finrank ℝ E)).conjExponent
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 : Tendsto (fun x ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x y) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x (y + z)) atTop (𝓝 ↑(g (y + z)))

Tactic:
have hgz : g z = z := congr_arg Subtype.val (hg_proj ⟨z, hz⟩)

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 : Tendsto (fun x ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x y) atTop (𝓝 0)
hgz : ↑(g z) = z
⊢ Tendsto (fun x ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x (y + z)) atTop (𝓝 ↑(g (y + z)))
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : IsSelfAdjoint A
⊢ A.IsClosed

Tactic:
← isSelfAdjoint_def.mp hA

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : IsSelfAdjoint A
⊢ A†.IsClosed
Module: Mathlib.Analysis.InnerProductSpace.SingularValues

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
⊢ (adjoint T ∘ₗ T).ker = ⊥ ↔ ∀ i < finrank 𝕜 E, 0 < T.singularValues i

Tactic:
← not_iff_not,

Goal state after:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
⊢ ¬(adjoint T ∘ₗ T).ker = ⊥ ↔ ¬∀ i < finrank 𝕜 E, 0 < T.singularValues i
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
this : eLpNorm v (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ v) (↑p) μ
x : E
⊢ ‖↑e‖ * ‖fderiv ℝ u x‖ = ↑C₂ * ‖fderiv ℝ u x‖

Tactic:
C₂,

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) μ
x : E
⊢ ‖↑e‖ * ‖fderiv ℝ u x‖ = ↑‖↑e‖₊ * ‖fderiv ℝ u 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
this : eLpNorm v (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ v) (↑p) μ
h4v : ∀ (x : E), ‖fderiv ℝ v x‖ ≤ ↑C₂ * ‖fderiv ℝ u x‖
⊢ ↑C₁ * ↑C * (↑C₂ * eLpNorm (fderiv ℝ u) (↑p) μ) = ↑(SNormLESNormFDerivOfEqConst F μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
C₂,

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) μ
h4v : ∀ (x : E), ‖fderiv ℝ v x‖ ≤ ↑C₂ * ‖fderiv ℝ u x‖
⊢ ↑C₁ * ↑C * (↑‖↑e‖₊ * eLpNorm (fderiv ℝ u) (↑p) μ) =
    ↑(SNormLESNormFDerivOfEqConst F μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ x ∈ s, t x ∈ 𝓝[s] x
hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : u.Countable
huU : ⋃ i ∈ u, s ∩ t i = s
⊢ dimH (⋃ i ∈ u, f '' (s ∩ t i)) ≤ dimH (⋃ i ∈ u, s ∩ t i) / ↑r

Tactic:
dimH_bUnion huc,

Goal state after:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ x ∈ s, t x ∈ 𝓝[s] x
hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : u.Countable
huU : ⋃ i ∈ u, s ∩ t i = s
⊢ ⨆ i ∈ u, dimH (f '' (s ∩ t i)) ≤ dimH (⋃ i ∈ u, s ∩ t i) / ↑r
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
s : Set X
⊢ extend (fun s x ↦ m (ediam s)) (f '' s) = extend (fun s x ↦ m (ediam s)) s

Tactic:
apply extend_congr <;> simp [hf.ediam_image]

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

Goal state before:
pp: E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : ↑(finrank ℝ E) < d
⊢ μH[d] = 0

Tactic:
lift d to ℝ≥0 using (Nat.cast_nonneg _).trans hd.le

Goal state after:
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ≥0
hd : ↑(finrank ℝ E) < ↑d
⊢ μH[↑d] = 0
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
p : Submodule 𝕜 V
f : U →ₗ[𝕜] V
h : ∀ (c : U), f c ∈ p
⊢ (codRestrict p f h).normDet = f.normDet

Tactic:
have : f = p.subtype ∘ₗ f.codRestrict p h := rfl
  conv_rhs => rw [this]
  rw [normDet_comp]
  have : (p.subtype.domRestrict (codRestrict p f h).range).normDet = 1 :=
    (p.subtypeₗᵢ.comp (codRestrict p f h).range.subtypeₗᵢ).normDet_eq_one
  simp [this]

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

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

Tactic:
symplComp,

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
⊢ S.mulIᗮ.mulI = S.mulI.symplComp
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.mulI.symplComp

Tactic:
symplComp,

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
⊢ S.mulIᗮ.mulI = S.mulI.mulIᗮ
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

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

Tactic:
symplComp,

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
⊢ (S ⊔ T).mulIᗮ = S.symplComp ⊓ T.symplComp
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

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

Tactic:
symplComp,

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
⊢ (S ⊔ T).mulIᗮ = S.mulIᗮ ⊓ T.symplComp
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

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

Tactic:
symplComp,

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
⊢ (S ⊔ T).mulIᗮ = S.mulIᗮ ⊓ T.mulIᗮ
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:
symplComp,

Goal state after:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S T : ClosedSubmodule ℝ H
⊢ (S ⊓ T).mulIᗮ = S.symplComp ⊔ T.symplComp
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).mulIᗮ = S.symplComp ⊔ T.symplComp

Tactic:
symplComp,

Goal state after:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S T : ClosedSubmodule ℝ H
⊢ (S ⊓ T).mulIᗮ = S.mulIᗮ ⊔ T.symplComp
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).mulIᗮ = S.mulIᗮ ⊔ T.symplComp

Tactic:
symplComp,

Goal state after:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S T : ClosedSubmodule ℝ H
⊢ (S ⊓ T).mulIᗮ = S.mulIᗮ ⊔ T.mulIᗮ
Module: Mathlib.Analysis.InnerProductSpace.Trace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : Module.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
⊢ RCLike.re ↑(∑ i, hT.eigenvalues ?m.55 i) = ∑ i, hT.eigenvalues hn i

pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : Module.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
⊢ Module.finrank 𝕜 E = ?m.53

pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : Module.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
⊢ ℕ

Tactic:
exact RCLike.ofReal_re_ax _

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

Goal state before:
pp: case inl
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
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
⊢ μH[d] (f ⁻¹' s) ≤ ↑0 ^ d * μH[d] s

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
⊢ μH[d] (f ⁻¹' s) ≤ ↑K ^ d * μH[d] s

Tactic:
· rcases eq_empty_or_nonempty (f ⁻¹' s) with (hs | ⟨x, hx⟩)
    · simp only [hs, measure_empty, zero_le]
    have : f ⁻¹' s = {x} := by
      have : Subsingleton X := hf.subsingleton
      have : (f ⁻¹' s).Subsingleton := subsingleton_univ.anti (subset_univ _)
      exact (subsingleton_iff_singleton hx).1 this
    rw [this]
    rcases eq_or_lt_of_le hd with (rfl | h'd)
    · simp only [ENNReal.rpow_zero, one_mul]
      rw [hausdorffMeasure_zero_singleton]
      exact one_le_hausdorffMeasure_zero_of_nonempty ⟨f x, hx⟩
    · have := nullSingletonClass_hausdorff X h'd
      simp only [zero_le, measure_singleton]

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
⊢ μH[d] (f ⁻¹' s) ≤ ↑K ^ d * μH[d] s
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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
hst : s ⊆ ⋃ n, t n
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / ↑K
⊢ ⨅ t,
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ n, t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d ≤
    ∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), ↑K ^ d * ediam (t i) ^ d

Tactic:
replace hst : f ⁻¹' s ⊆ _ := preimage_mono hst

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 ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / ↑K
hst : f ⁻¹' s ⊆ f ⁻¹' ⋃ n, t n
⊢ ⨅ t,
      ⨅ (_ : f ⁻¹' s ⊆ ⋃ n, t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d ≤
    ∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), ↑K ^ d * ediam (t i) ^ d
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)
x : E
⊢ (o.areaForm x) x = 0

Tactic:
rw [areaForm_to_volumeForm]
  refine o.volumeForm.map_eq_zero_of_eq ![x, x] ?_ (?_ : (0 : Fin 2) ≠ 1)
  · simp
  · simp

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

Goal state before:
pp: E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
⊢ nndist x y • 1 = edist x y

Tactic:
← Algebra.algebraMap_eq_smul_one

Goal state after:
E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
⊢ (algebraMap ℝ≥0 ℝ≥0∞) (nndist x y) = edist x y
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case neg.mpr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
⊢ SameRay ℝ x y → 0 ≤ ⟪x, y⟫ ∧ (o.areaForm x) y = 0

Tactic:
intro h
    obtain ⟨r, hr, rfl⟩ := h.exists_nonneg_left hx
    simp only [inner_smul_right, real_inner_self_eq_norm_sq, map_smulₛₗ, areaForm_apply_self,
      smul_eq_mul, mul_zero, and_true]
    positivity

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)
x y : E
⊢ (o.kahler x) y ≠ 0 ↔ x ≠ 0 ∧ y ≠ 0

Tactic:
by
  refine ⟨?_, fun h => o.kahler_ne_zero h.1 h.2⟩
  contrapose
  simp only [not_and_or, Classical.not_not, kahler_apply_apply, Complex.real_smul]
  rintro (rfl | rfl) <;> simp

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
⊢ mellin (fun t ↦ f (a * t)) s = ↑a ^ (-s) • mellin f s

Tactic:
simp_rw [mellin]
  have : 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) := fun t ht ↦ by
    dsimp only
    rw [ofReal_mul, mul_cpow_ofReal_nonneg ha.le (le_of_lt ht), ← mul_smul,
      (by ring : 1 - s = -(s - 1)), cpow_neg, inv_mul_cancel_left₀]
    rw [Ne, cpow_eq_zero_iff, ofReal_eq_zero, not_and_or]
    exact Or.inl ha.ne'
  rw [setIntegral_congr_fun measurableSet_Ioi this, integral_smul,
    integral_comp_mul_left_Ioi (fun u ↦ (u : ℂ) ^ (s - 1) • f u) _ ha,
    mul_zero, ← Complex.coe_smul, ← mul_smul, sub_eq_add_neg,
    cpow_add _ _ (ofReal_ne_zero.mpr ha.ne'), cpow_one, ofReal_inv,
    mul_assoc, mul_comm, inv_mul_cancel_right₀ (ofReal_ne_zero.mpr ha.ne')]

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_2.h
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
t : ℝ
hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖
ht : t ∈ Ioo 0 ε
⊢ d * (t ^ (-b) * t ^ (s - 1)) = d * t ^ (s - b - 1)

Tactic:
← rpow_add ht.1

Goal state after:
case refine_2.h
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
t : ℝ
hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖
ht : t ∈ Ioo 0 ε
⊢ d * t ^ (-b + (s - 1)) = d * t ^ (s - b - 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case refine_2
z : ℂ
hz : ‖z‖ < 1
⊢ Tendsto (fun x ↦ (logTaylor x z - log (1 + z)) / 1) atTop (nhds 0)

Tactic:
← isLittleO_iff_tendsto fun _ h ↦ (one_ne_zero h).elim

Goal state after:
case refine_2
z : ℂ
hz : ‖z‖ < 1
⊢ (fun x ↦ logTaylor x z - log (1 + z)) =o[atTop] fun x ↦ 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_9
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x ↦ x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ ↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2) =
    Complex.cos ↑x * ((fun x ↦ x ^ (n - 1)) ∘ Complex.cos) ↑x +
      Complex.sin ↑x * (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x)

Tactic:
· simp only [Complex.ofReal_cos, Complex.ofReal_sin]
      rw [mul_neg, mul_neg, ← sub_eq_add_neg, Function.comp_apply]
      congr 1
      · rw [← pow_succ', Nat.sub_add_cancel (by lia : 1 ≤ n)]
      · have : ((n - 1 : ℕ) : ℂ) = (n : ℂ) - 1 := by
          rw [Nat.cast_sub (one_le_two.trans hn), Nat.cast_one]
        rw [Nat.sub_sub, this]
        ring

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t ↦ ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t ↦ (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
⊢ MellinConvergent (fun t ↦ log t • f t) s ∧ HasDerivAt (mellin f) (mellin (fun t ↦ log t • f t) s) s

Tactic:
let bound : ℝ → ℝ := fun t : ℝ => (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t ↦ ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t ↦ (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t ↦ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
⊢ MellinConvergent (fun t ↦ log t • f t) s ∧ HasDerivAt (mellin f) (mellin (fun t ↦ log t • f t) s) s