mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : ∑ j, w j = 1
i : Fin (n + 1)
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide (s.points i)
      ((Finset.affineCombination R Finset.univ s.points) w) ↔
    0 ≤ w i

Tactic:
← Finset.univ.affineCombination_piSingle R s.points (Finset.mem_univ i),

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : ∑ j, w j = 1
i : Fin (n + 1)
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide
      ((Finset.affineCombination R Finset.univ s.points) (Pi.single i 1))
      ((Finset.affineCombination R Finset.univ s.points) w) ↔
    0 ≤ w i
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : ∑ j, w j = 1
i : Fin (n + 1)
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide (s.points i)
      ((Finset.affineCombination R Finset.univ s.points) w) ↔
    0 ≤ w i

Tactic:
by
  rw [← Finset.univ.affineCombination_piSingle R s.points (Finset.mem_univ i),
    s.wSameSide_affineSpan_faceOpposite_iff (Fintype.sum_pi_single' _ _) hw, eq_comm]
  simp [sign_eq_one_iff, le_iff_eq_or_lt', or_comm]

Goal state after:
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : ∑ j, w j = 1
i : Fin (n + 1)
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).WOppSide (s.points i)
      ((Finset.affineCombination R Finset.univ s.points) w) ↔
    w i ≤ 0

Tactic:
← Finset.univ.affineCombination_piSingle R s.points (Finset.mem_univ i),

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : ∑ j, w j = 1
i : Fin (n + 1)
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).WOppSide
      ((Finset.affineCombination R Finset.univ s.points) (Pi.single i 1))
      ((Finset.affineCombination R Finset.univ s.points) w) ↔
    w i ≤ 0
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
by_cases! H2 : ∃ s > 0, 0 < ∫ t in 0..s, g t ∧ μ {a : α | s < f a} = ∞

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
H2 : ∃ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t ∧ μ {a | s < f a} = ∞
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

case neg
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ∞
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
have A : ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t) = ∞ := by
      rw [eq_top_iff]
      calc
      ∞ = ∫⁻ t in Ioc 0 s, ∞ * ENNReal.ofReal (g t) := by
          have I_pos : ∫⁻ (a : ℝ) in Ioc 0 s, ENNReal.ofReal (g a) ≠ 0 := by
            rw [← ofReal_integral_eq_lintegral_ofReal (g_intble s s_pos).1]
            · simpa only [not_lt, ne_eq, ENNReal.ofReal_eq_zero, not_le] using hs
            · filter_upwards [ae_restrict_mem measurableSet_Ioc] with t ht using g_nn _ ht.1
          rw [lintegral_const_mul, ENNReal.top_mul I_pos]
          exact ENNReal.measurable_ofReal.comp g_mble
      _ ≤ ∫⁻ t in Ioc 0 s, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t) := by
          apply setLIntegral_mono' measurableSet_Ioc (fun x hx ↦ ?_)
          rw [← h's]
          gcongr
          exact fun ha ↦ hx.2.trans (le_of_lt ha)
      _ ≤ ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t) :=
          lintegral_mono_set Ioc_subset_Ioi_self

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ∞
A : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ∞
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
⊢ g =ᵐ[volume.restrict (Ioc 0 M)] 0

Tactic:
← restrict_Ioo_eq_restrict_Ioc

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
⊢ g =ᵐ[volume.restrict (Ioo 0 M)] 0
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: R : Type u_3
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedRing R
inst✝ : NormedAlgebra ℝ R
f : E → R
hf : HasTemperateGrowth f
k : ℕ
⊢ HasTemperateGrowth (f ^ k)

Tactic:
induction k with

Goal state after:
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
y : H
⊢ 1 / 2 < 1 + 0

Tactic:
by norm_num

Goal state after:
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
x : ℝ
hx : x ∈ t
⊢ 0 < 1 / 2

Tactic:
by norm_num

Goal state after:
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
⊢ 0 < 1 / 2

Tactic:
by norm_num

Goal state after:
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
⊢ 0 < 1 / 2

Tactic:
by norm_num

Goal state after:
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
this : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h✝ : r - ↑n < 0
h : 0 < ↑n - r
hx : 2⁻¹ < x
⊢ 0 < 2

Tactic:
by norm_num

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ¬HasEigenvalue (↑T) μ
⊢ ∃ c > 0, ∀ (x : X), c * ‖x‖ ≤ ‖(T - μ • 1) x‖

Tactic:
contrapose! h

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
⊢ HasEigenvalue (↑T) μ
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : f ∘ ⇑σ ≠ f ∘ ⇑(sort f)
⊢ ∃ i j, i < j ∧ (f ∘ ⇑σ) j < (f ∘ ⇑σ) i

Tactic:
contrapose! h

Goal state after:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : ∀ (i j : Fin n), i < j → (f ∘ ⇑σ) i ≤ (f ∘ ⇑σ) j
⊢ f ∘ ⇑σ = f ∘ ⇑(sort f)
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ ((↑(List.map (fun x ↦ RCLike.re x) (List.ofFn (RCLike.ofReal ∘ hA.eigenvalues₀)))).sort fun x1 x2 ↦ x1 ≥ x2) =
    List.ofFn hA.eigenvalues₀

Tactic:
List.map_ofFn,

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ ((↑(List.ofFn ((fun x ↦ RCLike.re x) ∘ RCLike.ofReal ∘ hA.eigenvalues₀))).sort fun x1 x2 ↦ x1 ≥ x2) =
    List.ofFn hA.eigenvalues₀
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ hA.cfcAux (ContinuousMap.restrict (spectrum ℝ A) (ContinuousMap.id ℝ)) = A

Tactic:
conv_rhs => rw [hA.spectral_theorem]

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ hA.cfcAux (ContinuousMap.restrict (spectrum ℝ A) (ContinuousMap.id ℝ)) =
    ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (diagonal (RCLike.ofReal ∘ hA.eigenvalues))
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: case a
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C(↑(spectrum ℝ a), ℝ)
⊢ spectrum ℝ (ha.cfcAux f) ⊆ spectrum ℝ f

Tactic:
apply AlgHom.spectrum_apply_subset

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
⊢ eigenspace (T.restrict ⋯) μ = ⊥

Tactic:
(Mathlib.Tactic.setTactic
 "set"
 []
 (Mathlib.Tactic.setArgsRest
  (Lean.binderIdent `p)
  [":" (Term.app `Submodule [`𝕜 `E])]
  ":="
  (choice
   (ClosedSubmodule.«term_ᗮ»
    (Term.paren
     (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
     («term⨆_,_»
      "⨆"
      (Batteries.ExtendedBinder.extBinders (Batteries.ExtendedBinder.extBinder (Lean.binderIdent `μ) []))
      ","
      (Term.app `eigenspace [`T `μ]))
     ")")
    "ᗮ")
   (Submodule.«term_ᗮ»
    (Term.paren
     (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
     («term⨆_,_»
      "⨆"
      (Batteries.ExtendedBinder.extBinders (Batteries.ExtendedBinder.extBinder (Lean.binderIdent `μ) []))
      ","
      (Term.app `eigenspace [`T `μ]))
     ")")
    "ᗮ"))
  []))

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
p : Submodule 𝕜 E := (⨆ μ, eigenspace T μ)ᗮ
⊢ eigenspace (T.restrict ⋯) μ = ⊥
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
⊢ ((↑(List.map (fun x ↦ RCLike.re x) (List.ofFn (RCLike.ofReal ∘ hT.eigenvalues ⋯)))).sort fun x1 x2 ↦ x1 ≥ x2) =
    List.ofFn (hT.eigenvalues hn)

Tactic:
List.map_ofFn,

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
⊢ ((↑(List.ofFn ((fun x ↦ RCLike.re x) ∘ RCLike.ofReal ∘ hT.eigenvalues ⋯))).sort fun x1 x2 ↦ x1 ≥ x2) =
    List.ofFn (hT.eigenvalues hn)
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
⊢ T.charpoly.Splits

Tactic:
refine Polynomial.splits_iff_card_roots.mpr ?_
  simp [hT.roots_charpoly_eq_eigenvalues rfl, LinearMap.charpoly_natDegree]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
⊢ ∃ g,
    HasCompactSupport g ∧
      ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧
        Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g (ENNReal.ofReal p) μ

Tactic:
have I : 0 < ε ^ (1 / p) := Real.rpow_pos_of_pos hε _
  have A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0 := by
    simp only [Ne, ENNReal.ofReal_eq_zero, not_le, I]
  have B : ENNReal.ofReal p ≠ 0 := by simpa only [Ne, ENNReal.ofReal_eq_zero, not_le] using hp
  rcases hf.exists_hasCompactSupport_eLpNorm_sub_le ENNReal.coe_ne_top A with
    ⟨g, g_support, hg, g_cont, g_mem⟩
  change eLpNorm _ (ENNReal.ofReal p) _ ≤ _ at hg
  refine ⟨g, g_support, ?_, g_cont, g_mem⟩
  rwa [(hf.sub g_mem).eLpNorm_eq_integral_rpow_norm B ENNReal.coe_ne_top,
    ENNReal.ofReal_le_ofReal_iff I.le, one_div, ENNReal.toReal_ofReal hp.le,
    Real.rpow_le_rpow_iff _ hε.le (inv_pos.2 hp)] at hg
  positivity

Goal state after:
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
n : ℤ
x : AddCircle T
⊢ ↑(-(n • x)).toCircle = (starRingEnd ℂ) ((fourier n) x)

Tactic:
← neg_smul,

Goal state after:
T : ℝ
n : ℤ
x : AddCircle T
⊢ ↑(-n • x).toCircle = (starRingEnd ℂ) ((fourier n) x)
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑(n • (x + ↑(T / 2 / ↑n))).toCircle = -(fourier n) x

Tactic:
zsmul_add,

Goal state after:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑(n • x + n • ↑(T / 2 / ↑n)).toCircle = -(fourier n) x
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: case refine_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : ↥(lp G 2)
s : Finset ι
i : ι
a✝ : i ∈ s
⊢ (V i) (↑f i) ∈ (V i).range

Tactic:
exact LinearMap.mem_range_self _ (f i)

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝² : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(hV.linearIsometryEquiv (W₀.sum fun a ↦ ⇑(V a))) = ⇑W₀

Tactic:
← hV.linearIsometryEquiv_symm_apply_dfinsupp_sum_single

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝² : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(hV.linearIsometryEquiv (hV.linearIsometryEquiv.symm (W₀.sum (lp.single 2)))) = ⇑W₀
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ fourierCoeff (liftIco T a f) n = fourierCoeffOn ⋯ f n

Tactic:
by
  rw [fourierCoeffOn_eq_integral, fourierCoeff_eq_intervalIntegral _ _ a, add_sub_cancel_left a T]
  congr 1
  refine intervalIntegral.integral_congr_Ioo_of_le (le_add_of_nonneg_right hT.out.le) fun x hx => ?_
  rw [liftIco_coe_apply (Ioo_subset_Ico_self hx)]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝³] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball 0 δ
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn (fun x ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
⊢ ∫ (x : α) in t, φ i x * δ ∂μ = (∫ (x : α) in t, φ i x ∂μ) * δ

Tactic:
rw [integral_mul_const]

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : 𝓢(E, F)
inst✝ : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -↑k ≤ s
x : ℝ
hx : 1 ≤ x
⊢ x ^ (-↑k) ≤ x ^ s

Tactic:
exact Real.rpow_le_rpow_of_exponent_le hx hk

Goal state after:
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst✝⁶] u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
⊢ Tendsto (fun n ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
have hnφ : ∀ n, ∀ x ∈ s, 0 ≤ φ n x := by
    intro n x hx
    apply mul_nonneg (inv_nonneg.2 _) (pow_nonneg (hnc x hx) _)
    exact setIntegral_nonneg hs.measurableSet fun x hx => pow_nonneg (hnc x hx) _

Goal state after:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst✝⁶] u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
⊢ Tendsto (fun n ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
x : E
⊢ ((smulLeftCLM F g) f) x = g x • f x

Tactic:
simp [smulLeftCLM_apply hg]

Goal state after: