mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: case refine_2
𝕜 : 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
⊢ Antitone ⇑Fin.revPerm

Tactic:
intro _ _ h

Goal state after:
case refine_2
𝕜 : 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
a✝ b✝ : Fin n
h : a✝ ≤ b✝
⊢ Fin.revPerm b✝ ≤ Fin.revPerm a✝
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
n k : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ ⇑({ toFun := fun f ↦ if hk : k + 1 ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0, map_add' := ⋯,
          map_smul' := ⋯ }
        f) =
    if k + 1 ≤ n then fderiv ℝ ⇑f else 0

Tactic:
split_ifs

Goal state after:
case pos
𝕜 : 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
n k : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
h✝ : k + 1 ≤ n
⊢ ⇑({ toFun := fun f ↦ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯, map_add' := ⋯, map_smul' := ⋯ } f) = fderiv ℝ ⇑f

case neg
𝕜 : 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
n k : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
h✝ : ¬k + 1 ≤ n
⊢ ⇑({ toFun := fun f ↦ 0, map_add' := ⋯, map_smul' := ⋯ } f) = 0
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
n k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
⊢ ⇑({ toFun := fun f ↦ if hi : k + ↑i ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0, map_add' := ⋯,
          map_smul' := ⋯ }
        f) =
    if k + ↑i ≤ n then iteratedFDeriv ℝ i ⇑f else 0

Tactic:
split_ifs

Goal state after:
case pos
𝕜 : 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
n k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
h✝ : k + ↑i ≤ n
⊢ ⇑({ toFun := fun f ↦ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯, map_add' := ⋯, map_smul' := ⋯ } f) =
    iteratedFDeriv ℝ i ⇑f

case neg
𝕜 : 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
n k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
h✝ : ¬k + ↑i ≤ n
⊢ ⇑({ toFun := fun f ↦ 0, map_add' := ⋯, map_smul' := ⋯ } f) = 0
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
⊢ (A ⊙ B).PosDef

Tactic:
by
  classical
  refine ⟨hA.isHermitian.hadamard hB.isHermitian, fun x hx ↦ ?_⟩
  have hAB : ((A ⊙ B).submatrix (↑) (↑) : Matrix x.support _ _).PosDef := by
    have hAs : (A.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hA.submatrix Subtype.coe_injective
    have hBs : (B.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hB.submatrix Subtype.coe_injective
    rw [submatrix_hadamard, posDef_iff_dotProduct_mulVec]
    refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y hy ↦ ?_⟩
    rw [star_dotProduct_hadamard_mulVec_eq_kronecker]
    exact (hAs.kronecker hBs).dotProduct_mulVec_pos <| by simpa
  simp_rw [RCLike.star_def, hadamard_apply, Finsupp.sum,
    ← Finset.sum_attach x.support, ← Finset.subtype_mem_eq_attach,
    ← Finsupp.subtypeDomain_apply, ← Finsupp.support_subtypeDomain]
  refine hAB.2 ?_
  simpa [← Finsupp.support_nonempty_iff] using Finsupp.support_nonempty_iff.mpr hx

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: case negSucc
A : Type u_2
inst✝¹⁰ : Ring A
inst✝⁹ : StarRing A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Algebra ℝ A
inst✝⁶ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
n : ℕ
⊢ abs ↑(Int.negSucc n) = ↑|Int.negSucc n|

Tactic:
Int.cast_negSucc,

Goal state after:
case negSucc
A : Type u_2
inst✝¹⁰ : Ring A
inst✝⁹ : StarRing A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Algebra ℝ A
inst✝⁶ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
n : ℕ
⊢ abs (-↑(n + 1)) = ↑|Int.negSucc n|
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : 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 μ)
h_two : ENNReal.toReal 2 = 2
⊢ eLpNorm (↑↑f) 2 μ ^ 2 = ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ

Tactic:
rw [← ENNReal.rpow_natCast, eLpNorm_eq_eLpNorm' two_ne_zero ENNReal.ofNat_ne_top, eLpNorm', ←
      ENNReal.rpow_mul, one_div, h_two]
    simp [enorm_eq_nnnorm]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.SmoothApprox

Goal state before:
pp: case inl
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
g : E → F
hg₁ : ContDiff ℝ ∞ g
hg₂ : ∀ (x : E), dist (g x) (f x) < ε
hg₃ : Function.support g ⊆ Function.support f
x : E
⊢ ‖(f - g) x‖ ≤ ε

Tactic:
simpa [← dist_eq_norm_sub'] using (hg₂ x).le

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.SmoothApprox

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬μ (Function.support f) = 0
hs₁ : μ (tsupport f) ≠ ∞
⊢ 0 < (μ (tsupport f)).toReal

Tactic:
exact toReal_pos (pos_mono (subset_tsupport f) (pos_of_ne_zero hf)).ne' hs₁

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
b : UnconditionalSchauderBasis β 𝕜 X
inst✝ : CompleteSpace X
C : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
hCpos : 0 ≤ C
A : Finset β
⊢ ↑((fun A ↦ ‖GeneralSchauderBasis.proj b A‖₊) A) ≤ ↑C.toNNReal

Tactic:
Real.coe_toNNReal C hCpos,

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
β : Type u_3
b : UnconditionalSchauderBasis β 𝕜 X
inst✝ : CompleteSpace X
C : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
hCpos : 0 ≤ C
A : Finset β
⊢ ↑((fun A ↦ ‖GeneralSchauderBasis.proj b A‖₊) A) ≤ C
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
b : SchauderBasis 𝕜 X
n i : ℕ
⊢ (GeneralSchauderBasis.proj b (Finset.range n)) (↑b i) = if i < n then ↑b i else 0

Tactic:
GeneralSchauderBasis.proj_apply_basis_mem

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
n i : ℕ
⊢ (if i ∈ Finset.range n then ↑b i else 0) = if i < n then ↑b i else 0
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
b : SchauderBasis 𝕜 X
inst✝ : CompleteSpace X
C : ℝ
hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C
hCpos : 0 ≤ C
n : ℕ
⊢ ↑((fun n ↦ ‖b.proj n‖₊) n) ≤ ↑C.toNNReal

Tactic:
Real.coe_toNNReal C hCpos,

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
inst✝ : CompleteSpace X
C : ℝ
hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C
hCpos : 0 ≤ C
n : ℕ
⊢ ↑((fun n ↦ ‖b.proj n‖₊) n) ≤ C
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 F
f : 𝓢(ℝ, F)
⊢ (tsupport fun x ↦ deriv (⇑f) x) ⊆ tsupport ⇑f

Tactic:
← fderiv_apply_one_eq_deriv

Goal state after:
𝕜 : Type u_2
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 F
f : 𝓢(ℝ, F)
⊢ (tsupport fun x ↦ (fderiv ℝ (⇑f) x) 1) ⊆ tsupport ⇑f
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
inst✝ : Fact (0 < T)
n : ℤ
⊢ ⨆ x, ‖(fourier n) x‖ = 1

Tactic:
have : ∀ x : AddCircle T, ‖fourier n x‖ = 1 := fun x => Circle.norm_coe _

Goal state after:
T : ℝ
inst✝ : Fact (0 < T)
n : ℤ
this : ∀ (x : AddCircle T), ‖(fourier n) x‖ = 1
⊢ ⨆ x, ‖(fourier n) x‖ = 1
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a b))
this : Fact (0 < b - a)
⊢ HasSum (fun i ↦ ‖fourierCoeffOn hab f i‖ ^ 2) ((b - a)⁻¹ • ∫ (x : ℝ) in a..b, ‖f x‖ ^ 2)

Tactic:
rw [← add_sub_cancel a b] at hL2

Goal state after:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
⊢ HasSum (fun i ↦ ‖fourierCoeffOn hab f i‖ ^ 2) ((b - a)⁻¹ • ∫ (x : ℝ) in a..b, ‖f x‖ ^ 2)
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
⊢ ‖-(2 * ↑π * I) • (L v).smulRight (f v)‖ = 2 * π * ‖L v‖ * ‖f v‖

Tactic:
norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)),

Goal state after:
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
⊢ ‖-(2 * ↑π * I)‖ * ‖(L v).smulRight (f v)‖ = 2 * π * ‖L v‖ * ‖f v‖
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
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀u : x₀ ∈ u
⊢ TendstoUniformlyOn φ 0 atTop (s \ u)

Tactic:
obtain ⟨t, t_pos, tx₀, ht⟩ : ∃ t, 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t := by
      rcases eq_empty_or_nonempty (s \ u) with (h | h)
      · exact
          ⟨0, le_rfl, hnc₀, by simp only [h, mem_empty_iff_false, IsEmpty.forall_iff, imp_true_iff]⟩
      obtain ⟨x, hx, h'x⟩ : ∃ x ∈ s \ u, ∀ y ∈ s \ u, c y ≤ c x :=
        IsCompact.exists_isMaxOn (hs.diff u_open) h (hc.mono sdiff_subset)
      refine ⟨c x, hnc x hx.1, h'c x hx.1 ?_, h'x⟩
      rintro rfl
      exact hx.2 x₀u

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
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
⊢ TendstoUniformlyOn φ 0 atTop (s \ u)
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℂ
ha : a.re < 0
c : ℝ
this : Tendsto (fun x ↦ Complex.exp (a * ↑x)) atTop (𝓝 0)
⊢ Tendsto (fun i ↦ (Complex.exp (a * ↑i) - Complex.exp (a * ↑c)) / a) atTop (𝓝 (-Complex.exp (a * ↑c) / a))

Tactic:
by
    simpa using this.sub_const _ |>.div_const _

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

Goal state before:
pp: a : ℝ
ha : a < 0
c : ℝ
⊢ (-Complex.exp (↑a * ↑c)).re / a = -(Complex.exp (↑a * ↑c)).re / a

pp: a : ℝ
ha : a < 0
c : ℝ
⊢ Integrable (fun x ↦ Complex.exp (↑a * ↑x)) (volume.restrict (Ioi c))

Tactic:
Complex.neg_re

Goal state after:
a : ℝ
ha : a < 0
c : ℝ
⊢ -(Complex.exp (↑a * ↑c)).re / a = -(Complex.exp (↑a * ↑c)).re / a

a : ℝ
ha : a < 0
c : ℝ
⊢ Integrable (fun x ↦ Complex.exp (↑a * ↑x)) (volume.restrict (Ioi c))
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: c : ℝ
hc : 1 < c
⊢ ∫ (t : ℝ) in Ioi c, t⁻¹ / log t ^ 2 = (log c)⁻¹

Tactic:
convert! integral_Ioi_of_hasDerivAt_of_tendsto' (m := 0) (f := fun t ↦ -(log t)⁻¹) ?_
    (integrableOn_inv_div_log_sq_Ioi hc) ?_ using 1
  · simp
  · intro t _
    convert! (hasDerivAt_inv_log (by grind : t ≠ 0) (by grind) (by grind)).neg using 1
    field
  convert! tendsto_log_atTop.inv_tendsto_atTop.neg using 1
  simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖(-a) ^ s * rexp (-b * a ^ 2)‖ ≤ a ^ s * rexp (-b * a ^ 2)

Tactic:
have : MeasurableSet (Ioi (0 : ℝ)) := measurableSet_Ioi

Goal state after:
case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖(-a) ^ s * rexp (-b * a ^ 2)‖ ≤ a ^ s * rexp (-b * a ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: p : ℝ × ℝ
⊢ (fderivPolarCoordSymm p).det = p.1

Tactic:
conv_rhs => rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]
  unfold fderivPolarCoordSymm
  simp only [neg_mul, LinearMap.det_toContinuousLinearMap, LinearMap.det_toLin,
    Matrix.det_fin_two_of, sub_neg_eq_add]
  ring

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

Goal state before:
pp: a : ℂ
⊢ ↑Complex.polarCoord a = (‖a‖, a.arg)

Tactic:
simp_rw [Complex.norm_def, Complex.normSq_apply, ← pow_two]

Goal state after:
a : ℂ
⊢ ↑Complex.polarCoord a = (√(a.re ^ 2 + a.im ^ 2), a.arg)
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : RCLike 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
⊢ ∫ (x : (i : ι) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i

Tactic:
let e := (equivFin ι).symm
  rw [← (measurePreserving_piCongrLeft _ e).integral_comp']
  simp_rw [← e.prod_comp, MeasurableEquiv.coe_piCongrLeft, Equiv.piCongrLeft_apply_apply,
    MeasureTheory.integral_fin_nat_prod_eq_prod]

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

Goal state before:
pp: case zero.hb
s : ℂ
h1 : s = 0
⊢ s.re ≤ 0

Tactic:
h1

Goal state after:
case zero.hb
s : ℂ
h1 : s = 0
⊢ re 0 ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: n : ℕ
⊢ (Complex.Gamma (↑n + 1)).re = ↑n !

Tactic:
Complex.Gamma_nat_eq_factorial,

Goal state after:
n : ℕ
⊢ (↑n !).re = ↑n !
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
w : V
⊢ 𝓕 (fun v ↦ cexp (-b * ↑‖v‖ ^ 2)) w = (↑π / b) ^ (↑(Module.finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑‖w‖ ^ 2 / b)

Tactic:
simpa using fourier_gaussian_innerProductSpace' hb 0 w

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

Goal state before:
pp: V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : FiniteDimensional ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
H : Type u_4
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
f : 𝓢(V, H)
⊢ ∫ (ξ : V), ‖(𝓕 f) ξ‖ ^ 2 = ∫ (x : V), ‖f x‖ ^ 2

Tactic:
by
  apply Complex.ofRealLI.injective
  simpa [← LinearIsometry.integral_comp_comm, inner_self_eq_norm_sq_to_K] using
    integral_inner_fourier_fourier f f

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
g : 𝓢(E, ℂ)
⊢ (toTemperedDistribution f) g = ∫ (x : E), g x • ↑↑f x ∂μ

Tactic:
simp only [toTemperedDistribution, toPointwiseConvergenceCLM_apply, comp_apply _, toLpCLM_apply,
    lpPairing_eq_integral, lsmul_flip_apply, toSpanSingleton_apply]
  apply integral_congr_ae
  filter_upwards [g.coeFn_toLp (1 - p⁻¹)⁻¹ μ] with x hg
  rw [hg]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
he' : e ≠ 1
hL : Continuous fun p ↦ (L p.1) p.2
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
v v' : V
h : ∀ (w : W), (char he hL w) v = (char he hL w) v'
⊢ v = v'

Tactic:
by
  contrapose! h
  obtain ⟨w, hw⟩ := DFunLike.ne_iff.mp (hL' (v - v') (sub_ne_zero_of_ne h))
  obtain ⟨a, ha⟩ := DFunLike.ne_iff.mp he'
  use (a / (L (v - v') w)) • w
  simp only [map_sub, LinearMap.sub_apply, char_apply, ne_eq]
  rw [← div_eq_one_iff_eq (Circle.coe_ne_zero _), div_eq_inv_mul, ← Metric.unitSphere.coe_inv,
    ← e.map_neg_eq_inv, ← Submonoid.coe_mul, ← e.map_add_eq_mul, OneMemClass.coe_eq_one]
  simp only [map_sub, LinearMap.sub_apply, LinearMap.zero_apply, AddChar.one_apply,
    map_smul, smul_eq_mul] at ha hw ⊢
  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
  canonicalizer; a minimization would help. The original proof was: `grind` -/
  ring_nf
  field_simp
  assumption

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
⊢ MemSobolev (s - 2) 2 (Δ f)

Tactic:
rw [SubNegMonoid.sub_eq_add_neg s 2, add_comm, ← memSobolev_besselPotential_iff,
    besselPotential_neg_two_laplacian_eq f]

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
⊢ MemSobolev s 2 (-(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(‖x‖ ^ 2 * (1 + ‖x‖ ^ 2) ^ (-1))) f)
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: n : ℕ
⊢ (if Squarefree n then (-1) ^ cardFactors n else 0) = 0 ∨
    (if Squarefree n then (-1) ^ cardFactors n else 0) = 1 ∨ (if Squarefree n then (-1) ^ cardFactors n else 0) = -1

Tactic:
split_ifs

Goal state after:
case pos
n : ℕ
h✝ : Squarefree n
⊢ (-1) ^ cardFactors n = 0 ∨ (-1) ^ cardFactors n = 1 ∨ (-1) ^ cardFactors n = -1

case neg
n : ℕ
h✝ : ¬Squarefree n
⊢ 0 = 0 ∨ 0 = 1 ∨ False
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: l : ℕ
hl : Squarefree l
⊢ 1 ^ cardFactors l = 1

Tactic:
one_pow

Goal state after:
l : ℕ
hl : Squarefree l
⊢ 1 = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
⊢ μ (p ^ k) = if k = 1 then -1 else 0

Tactic:
split_ifs with h
  · rw [h, pow_one, moebius_apply_prime hp]
  rw [moebius_eq_zero_of_not_squarefree]
  rw [squarefree_pow_iff hp.ne_one hk, not_and_or]
  exact Or.inr h

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
let f' : ArithmeticFunction R := ⟨fun x => if x = 0 then 0 else f x, if_pos rfl⟩
  let g' : ArithmeticFunction R := ⟨fun x => if x = 0 then 0 else g x, if_pos rfl⟩
  trans (ζ : ArithmeticFunction ℤ) • f' = g'
  · rw [ArithmeticFunction.ext_iff]
    apply forall_congr'
    intro n
    cases n with
    | zero => simp
    | succ n =>
      rw [coe_zeta_smul_apply]
      simp only [forall_prop_of_true, succ_pos', f', g', coe_mk, succ_ne_zero, ite_false]
      rw [sum_congr rfl fun x hx => if_neg (pos_of_mem_divisors hx).ne']
  trans μ • g' = f'
  · constructor <;> intro h <;>
      simp only [← h, ← mul_smul, moebius_mul_coe_zeta, coe_zeta_mul_moebius, one_smul]
  · rw [ArithmeticFunction.ext_iff]
    apply forall_congr'
    intro n
    cases n with
    | zero => simp
    | succ n =>
      simp only [forall_prop_of_true, succ_pos', smul_apply, f', g', coe_mk, succ_ne_zero,
        ite_false]
      rw [sum_congr rfl fun x hx => ?_]
      rw [if_neg (pos_of_mem_divisors (snd_mem_divisors_of_mem_antidiagonal hx)).ne']

Goal state after: