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

Goal state before:
pp: case pos
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s).Nonempty
hx : x ∈ s
⊢ IsPreconnected {y | s.SOppSide x y}

Tactic:
simp only [hx, SOppSide, not_true, false_and, and_false]
      exact isPreconnected_empty

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

Goal state before:
pp: case inl
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₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
hj' : s.points j ∈ affineSpan R (Set.range (s.faceOpposite i).points)
w₃ : Fin (n + 1) → R := w₂ - w₂ i • (w₁ i)⁻¹ • (w₁ - Pi.single j 1)
hw₃1 : ∑ k, w₃ k = 1
hw₃i : w₃ i = 0
h : w₁ i < 0
⊢ 0 ≤ w₂ i * (w₁ i)⁻¹

Tactic:
rw [sign_neg h, eq_comm, sign_eq_neg_one_iff] at hs
    exact (mul_pos_of_neg_of_neg hs (inv_neg''.2 h)).le

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

Goal state before:
pp: case refine_1
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₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
h :
  (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)
⊢ SignType.sign (w₁ i) = SignType.sign (w₂ i) ∨ w₁ i = 0 ∨ w₂ i = 0

Tactic:
by_cases h0 : w₁ i = 0
    · simp [h0]
    by_cases h0' : w₂ i = 0
    · simp [h0']
    exact .inl ((s.sSameSide_affineSpan_faceOpposite_iff hw₁ hw₂).1 ⟨h,
      (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).not.2 h0,
      (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₂).not.2 h0'⟩).1

Goal state after:
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
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0
t : ℝ
ht : g t = 0 t
⊢ μ {a | t ≤ f a} * ENNReal.ofReal (g t) = 0 t

Tactic:
by simp [ht]

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

Goal state before:
pp: case hf
α : 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} = ∞
I_pos : ∫⁻ (a : ℝ) in Ioc 0 s, ENNReal.ofReal (g a) ≠ 0
⊢ Measurable fun t ↦ ENNReal.ofReal (g t)

Tactic:
exact ENNReal.measurable_ofReal.comp g_mble

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

Goal state before:
pp: case inl
α : 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
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
a : α
ha : f a ≤ M
⊢ a ∈ ⋃ i, {a | f a ≤ M} ∪ {a | u i < f a}

Tactic:
exact mem_iUnion.2 ⟨0, Or.inl ha⟩

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

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
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
n : ℕ
g : E → ℝ := fun x ↦ ‖iteratedFDeriv ℝ n f x‖
hg : Continuous g
x₀ : E
hx₀ : ∀ (y : E), g y ≤ g x₀
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C * (1 + ‖x‖) ^ k

Tactic:
refine ⟨0, g x₀, fun x ↦ ?_⟩

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
n : ℕ
g : E → ℝ := fun x ↦ ‖iteratedFDeriv ℝ n f x‖
hg : Continuous g
x₀ : E
hx₀ : ∀ (y : E), g y ≤ g x₀
x : E
⊢ ‖iteratedFDeriv ℝ n f x‖ ≤ g x₀ * (1 + ‖x‖) ^ 0
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: case e'_3.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ∞
⊢ AEStronglyMeasurable (fun t ↦ μ.real {a | t < f a}) (volume.restrict (Ioi 0))

Tactic:
apply Measurable.aestronglyMeasurable
      refine Measurable.ennreal_toReal ?_
      exact Antitone.measurable (fun _ _ hst ↦ measure_mono (fun _ h ↦ lt_of_le_of_lt hst h))

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
⊢ HasTemperateGrowth fun x ↦ (1 + ‖x‖ ^ 2) ^ r

Tactic:
have hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t :=
    contDiffOn_fun_id.rpow_const_of_ne fun x hx ↦ (lt_trans (by norm_num) hx).ne'

Goal state after:
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
⊢ HasTemperateGrowth fun x ↦ (1 + ‖x‖ ^ 2) ^ r
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: case pos
𝕜 : 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
μ : 𝕜
hμ : HasEigenvalue T μ
⊢ {i | ↑(hT.unsortedEigenvalues hn i) = μ}.card = finrank 𝕜 ↥(eigenspace T μ)

pp: case neg
𝕜 : 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
μ : 𝕜
hμ : ¬HasEigenvalue T μ
⊢ {i | ↑(hT.unsortedEigenvalues hn i) = μ}.card = finrank 𝕜 ↥(eigenspace T μ)

Tactic:
· convert!
      hT.direct_sum_isInternal.card_filter_subordinateOrthonormalBasisIndex_eq hn
        hT.orthogonalFamily_eigenspaces' ⟨μ, hμ⟩ with i
    unfold unsortedEigenvalues
    let ⟨x, hx⟩ := hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i
      hT.orthogonalFamily_eigenspaces'
    rw [Eigenvalues.val_mk, RCLike.conj_eq_iff_re.mp (hT.conj_eigenvalue_eq_self hx)]
    exact Subtype.mk_eq_mk.symm

Goal state after:
case neg
𝕜 : 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
μ : 𝕜
hμ : ¬HasEigenvalue T μ
⊢ {i | ↑(hT.unsortedEigenvalues hn i) = μ}.card = finrank 𝕜 ↥(eigenspace T μ)
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
μ : 𝕜
⊢ {i | ↑(hT.unsortedEigenvalues hn i) = μ}.card = finrank 𝕜 ↥(eigenspace T μ)

Tactic:
by
  by_cases hμ : HasEigenvalue T μ
  · convert!
      hT.direct_sum_isInternal.card_filter_subordinateOrthonormalBasisIndex_eq hn
        hT.orthogonalFamily_eigenspaces' ⟨μ, hμ⟩ with i
    unfold unsortedEigenvalues
    let ⟨x, hx⟩ := hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i
      hT.orthogonalFamily_eigenspaces'
    rw [Eigenvalues.val_mk, RCLike.conj_eq_iff_re.mp (hT.conj_eigenvalue_eq_self hx)]
    exact Subtype.mk_eq_mk.symm
  · rw [Module.End.hasEigenvalue_iff.not_left.mp hμ, finrank_bot, Finset.card_filter_eq_zero_iff]
    intro i _ rfl
    exact hμ (hT.hasEigenvalue_unsortedEigenvalues hn i)

Goal state after:
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
⊢ (((toLinearMap₂' 𝕜) A) (star x)) x = 0 ↔ A *ᵥ x = 0

Tactic:
simpa only [toLinearMap₂'_apply'] using hA.dotProduct_mulVec_zero_iff x

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓_{K}(E, F)
⊢ (True → ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C) ↔ ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C

Tactic:
forall_const

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

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
h_gram : (gram 𝕜 v).PosDef
this : Fintype n
⊢ LinearIndependent 𝕜 v

Tactic:
rw [Fintype.linearIndependent_iff]

Goal state after:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
h_gram : (gram 𝕜 v).PosDef
this : Fintype n
⊢ ∀ (g : n → 𝕜), ∑ i, g i • v i = 0 → ∀ (i : n), g i = 0
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ∀ᵐ (x : α) ∂μ, ‖↑↑⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩ x‖₊ ≤ ‖f‖₊

Tactic:
refine (f.toContinuousMap.coeFn_toAEEqFun μ).mono ?_

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ∀ (x : α),
    ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = f.toContinuousMap x →
      ‖↑↑⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩ x‖₊ ≤ ‖f‖₊
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: case e_f
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
x : α
h_two : 2 = ↑2
⊢ ENNReal.ofReal (‖↑↑f x‖ ^ 2) = ↑(‖↑↑f x‖₊ ^ 2)

Tactic:
← Real.rpow_natCast _ 2,

Goal state after:
case e_f
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
x : α
h_two : 2 = ↑2
⊢ ENNReal.ofReal (‖↑↑f x‖ ^ ↑2) = ↑(‖↑↑f x‖₊ ^ 2)
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
⊢ Continuous ⇑(fderivLM 𝕜 n k)

Tactic:
refine continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..)
      (ContDiffMapSupportedIn.withSeminorms ..) _ (fun i ↦ ⟨{i+1}, 1, fun f ↦ ?_⟩)
    simpa using seminorm_fderivLM_le 𝕜 f

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
⊢ LinearIndependent 𝕜 ↑b

Tactic:
classical
  refine linearIndependent_iff.mpr (fun l hl ↦ l.ext ?_)
  simpa [l.linearCombination_apply, Finsupp.sum, b.ortho, Pi.single_apply] using
    fun i ↦ congr_arg (b.coord i) hl

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)
f g : ↥(lp G 2)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by congr

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)
f₁ f₂ g : ↥(lp G 2)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by congr

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

Goal state before:
pp: T : ℝ
n : ℤ
x : ℝ
⊢ Complex.exp (↑2 * ↑π / ↑T * ↑(n • x) * Complex.I) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)

Tactic:
zsmul_eq_mul,

Goal state after:
T : ℝ
n : ℤ
x : ℝ
⊢ Complex.exp (↑2 * ↑π / ↑T * ↑(↑n * x) * Complex.I) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
x : X
⊢ HasSum
    (fun i ↦ ({ toFun := coeff i, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (‖succSub D.P i‖ / ‖D.e i‖) ⋯) x • D.e i)
    x (SummationFilter.conditional ℕ)

Tactic:
HasSum,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
x : X
⊢ Tendsto
    (fun s ↦
      ∑ b ∈ s,
        ({ toFun := coeff b, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (‖succSub D.P b‖ / ‖D.e b‖) ⋯) x • D.e b)
    (SummationFilter.conditional ℕ).filter (𝓝 x)
Module: Mathlib.Analysis.Fourier.AddCircle

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

Tactic:
zsmul_eq_mul,

Goal state after:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑(toCircle ↑(↑n * (T / 2 / ↑n))) = -1
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a : ℝ
this : ∀ (x : ℝ), (fourier (-n)) ↑x • f ↑x = (fun z ↦ (fourier (-n)) z • f z) ↑x
⊢ ∫ (t : AddCircle T), (fourier (-n)) t • f t ∂haarAddCircle =
    (1 / T * T) • ∫ (x : AddCircle T), (fourier (-n)) x • f x ∂haarAddCircle

Tactic:
one_div_mul_cancel hT.out.ne',

Goal state after:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a : ℝ
this : ∀ (x : ℝ), (fourier (-n)) ↑x • f ↑x = (fun z ↦ (fourier (-n)) z • f z) ↑x
⊢ ∫ (t : AddCircle T), (fourier (-n)) t • f t ∂haarAddCircle =
    1 • ∫ (x : AddCircle T), (fourier (-n)) x • f x ∂haarAddCircle
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
⊢ ‖fourierSMulRight L f v‖ = 2 * π * ‖L v‖ * ‖f v‖

Tactic:
by
  rw [fourierSMulRight, norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)),
    norm_neg, norm_mul, norm_mul, norm_I, mul_one, Complex.norm_of_nonneg pi_pos.le,
    Complex.norm_two, ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]

Goal state after:
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₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
⊢ (smulLeftCLM F g₁ ∘SL smulLeftCLM F g₂) f = (smulLeftCLM F (g₁ * g₂)) f

Tactic:
exact smulLeftCLM_smulLeftCLM_apply hg₁ hg₂ f

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

Goal state before:
pp: case hiφ
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
this : Tendsto (fun c ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
⊢ (fun c ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) =ᶠ[atTop] fun i ↦
    ∫ (x : F) in closedBall 0 1, i ^ finrank ℝ F * φ (i • x) ∂μ

Tactic:
filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)

Goal state after:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
this : Tendsto (fun c ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
c : ℝ
hc : 0 < c
⊢ ∫ (x : F) in closedBall 0 c, φ x ∂μ = ∫ (x : F) in closedBall 0 1, c ^ finrank ℝ F * φ (c • x) ∂μ
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: case h'iφ
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
⊢ ∀ᶠ (i : ℝ) in atTop, AEStronglyMeasurable (fun x ↦ i ^ finrank ℝ F * φ (i • x)) μ

Tactic:
filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)

Goal state after:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
c : ℝ
hc : 0 < c
⊢ AEStronglyMeasurable (fun x ↦ c ^ finrank ℝ F * φ (c • x)) μ
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
t : ℝ
ht : t ∈ Ioi c
⊢ ContinuousWithinAt (fun t ↦ ↑t ^ a) (Ioi c) t

Tactic:
exact (Complex.continuousAt_ofReal_cpow_const _ _ (Or.inr (hc.trans ht).ne')).continuousWithinAt

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (fderiv ℝ f) volume
⊢ 𝓕 (fderiv ℝ f) = fourierSMulRight (-innerSL ℝ) (𝓕 f)

Tactic:
rw [← flip_innerSL_real V]
  exact VectorFourier.fourierIntegral_fderiv (innerSL ℝ) hf h'f hf'

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: case inr
s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re < 0
⊢ IntegrableOn (fun x ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume

Tactic:
replace hs : s.re - 1 < -1 := by rwa [sub_lt_iff_lt_add, neg_add_cancel]
    exact (integrableOn_Ioi_rpow_of_lt hs ht).const_mul s.re

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

Goal state before:
pp: case hf
V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
f g : ↥(Lp E 1 volume)
x : V
⊢ Integrable (↑↑f) volume

Tactic:
exact L1.integrable_coeFn f

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case left
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2

Tactic:
rcases hxy with hxy | hxy

Goal state after:
case left.inl
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1}
⊢ 0 < x ^ 2 + y ^ 2

case left.inr
x y : ℝ
hxy : (x, y) ∈ {q | q.2 ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case right
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
⊢ 0 ≤ (Complex.equivRealProd.symm (x, y)).re ∨ (Complex.equivRealProd.symm (x, y)).im ≠ 0

Tactic:
rcases hxy with hxy | hxy

Goal state after:
case right.inl
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1}
⊢ 0 ≤ (Complex.equivRealProd.symm (x, y)).re ∨ (Complex.equivRealProd.symm (x, y)).im ≠ 0

case right.inr
x y : ℝ
hxy : (x, y) ∈ {q | q.2 ≠ 0}
⊢ 0 ≤ (Complex.equivRealProd.symm (x, y)).re ∨ (Complex.equivRealProd.symm (x, y)).im ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this : IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
⊢ 0 = b ^ (-p⁻¹) * 0

Tactic:
rw [mul_zero]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n✝ : ℕ
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedDeriv n f) volume
hn✝ : ↑n✝ ≤ N
x : ℝ
n : ℕ
hn : ↑n ≤ N
⊢ Integrable (⇑(ContinuousMultilinearMap.piFieldEquiv ℝ (Fin n) E) ∘ iteratedDeriv n f) volume

Tactic:
exact (LinearIsometryEquiv.integrable_comp_iff _).2 (h'f n hn)

Goal state after: