mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc : ∀ ε > 0, ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : ℕ → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), ‖(T - μ • 1) (x n)‖ < φ n
hx_lim : Tendsto (fun n ↦ (T - μ • 1) (x n)) atTop (𝓝 0)
y_ : ℕ → X := fun n ↦ T (x n)
hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
K : Set X
hK : IsCompact K
hK' : ⇑↑T '' Metric.closedBall 0 1 ⊆ K
n : ℕ
⊢ x n ∈ Metric.closedBall 0 1

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone graph.proj

Tactic:
rintro ⟨⟨x, i⟩, hx⟩ ⟨⟨y, j⟩, hy⟩ (_ | h)
  · exact le_of_lt ‹_›
  · simp [graph.proj]

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
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T) μ
S : X →L[𝕜] X := T - μ • 1
K✝ : NNReal
hK✝ : AntilipschitzWith K✝ ⇑S
h₂ : ¬Function.Surjective ⇑S
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range (↑S ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ}, m ≤ n → f n ∈ (↑S ^ m).range
hf_mem' : ∀ {n m : ℕ}, m ≤ n → S (f n) ∈ (↑S ^ (m + 1)).range
hp : Pairwise fun x₁ x₂ ↦ ‖μ‖ ≤ ‖T (f x₁) - T (f x₂)‖
K : Set X
hK : IsCompact K
hK' : ⇑↑T '' Metric.closedBall 0 (‖c‖ + 1) ⊆ K
n : ℕ
⊢ f n ∈ Metric.closedBall 0 (‖c‖ + 1)

Tactic:
by simp [*]

Goal state after:
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 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
⊢ ∃ v t, t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v

Tactic:
have : hA.eigenvalues ≠ 0 := by
    contrapose h_ne
    have := hA.spectral_theorem
    rwa [h_ne, Pi.comp_zero, RCLike.ofReal_zero, (by rfl : Function.const n (0 : 𝕜) = fun _ ↦ 0),
      diagonal_zero, map_zero] at this

Goal state after:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_2
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
this : hA.eigenvalues ≠ 0
⊢ ∃ v t, t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
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
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C(↑(spectrum ℝ a), ℝ)
⊢ spectrum ℝ (ha.cfcAux f) = Set.range ⇑f

Tactic:
case =>

Goal state after:
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
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C(↑(spectrum ℝ a), ℝ)
⊢ IsSelfAdjoint (ha.cfcAux f)

Tactic:
case =>

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✝ : IsSelfAdjoint A
hA : A.IsHermitian
⊢ Isometry ⇑(cfcHom hA✝)

Tactic:
IsHermitian.cfcHom_eq_cfcAux hA,

Goal state after:
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA✝ : IsSelfAdjoint A
hA : A.IsHermitian
⊢ Isometry ⇑hA.cfcAux
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
hf : Integrable f μ
c : E
⊢ Integrable (fun x ↦ ⟪f x, c⟫) μ

Tactic:
by
  rw [← memLp_one_iff_integrable] at hf ⊢; exact hf.inner_const c

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

Goal state before:
pp: case refine_3
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
h : ∀ (x : α), ‖⟪↑↑f x, ↑↑g x⟫‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
⊢ eLpNorm (fun a ↦ ‖↑↑f a‖ ^ 2) 1 μ < ∞ ∧ eLpNorm (fun a ↦ ‖↑↑g a‖ ^ 2) 1 μ < ∞

Tactic:
exact ⟨eLpNorm_rpow_two_norm_lt_top f, eLpNorm_rpow_two_norm_lt_top g⟩

Goal state after:
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
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
G : Type u_8
inst✝⁹ : NormedAlgebra ℝ 𝕜
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace 𝕜 F₁
inst✝⁶ : NormedSpace ℝ F₁
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
inst✝³ : NormedSpace ℝ F₂
inst✝² : NormedAddCommGroup F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℝ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
g : E → F₂
hg : ContDiff ℝ (↑n) g
⊢ ∀ (f g_1 : 𝓓^{n}_{K}(E, F₁)) (x : E), (B ((f + g_1) x)) (g x) = (B (f x)) (g x) + (B (g_1 x)) (g x)

Tactic:
case =>

Goal state after:
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
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
G : Type u_8
inst✝⁹ : NormedAlgebra ℝ 𝕜
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace 𝕜 F₁
inst✝⁶ : NormedSpace ℝ F₁
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
inst✝³ : NormedSpace ℝ F₂
inst✝² : NormedAddCommGroup F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℝ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
g : E → F₂
hg : ContDiff ℝ (↑n) g
⊢ ∀ (c : 𝕜) (f : 𝓓^{n}_{K}(E, F₁)) (x : E), (B ((c • f) x)) (g x) = c • (B (f x)) (g x)

Tactic:
case =>

Goal state after:
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
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
G : Type u_8
inst✝⁹ : NormedAlgebra ℝ 𝕜
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace 𝕜 F₁
inst✝⁶ : NormedSpace ℝ F₁
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
inst✝³ : NormedSpace ℝ F₂
inst✝² : NormedAddCommGroup F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℝ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
g : E → F₂
hg : ContDiff ℝ (↑n) g
φ : 𝓓^{n}_{K}(E, F₁)
⊢ ContDiff ℝ ↑n fun x ↦ (B (φ x)) (g x)

Tactic:
case =>

Goal state after:
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
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
G : Type u_8
inst✝⁹ : NormedAlgebra ℝ 𝕜
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace 𝕜 F₁
inst✝⁶ : NormedSpace ℝ F₁
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
inst✝³ : NormedSpace ℝ F₂
inst✝² : NormedAddCommGroup F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℝ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
g : E → F₂
hg : ContDiff ℝ (↑n) g
φ : 𝓓^{n}_{K}(E, F₁)
x : E
hx : x ∈ (↑K)ᶜ
⊢ (fun x ↦ (B (φ x)) (g x)) x = 0 x

Tactic:
case =>

Goal state after:
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
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
G : Type u_8
inst✝⁹ : NormedAlgebra ℝ 𝕜
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace 𝕜 F₁
inst✝⁶ : NormedSpace ℝ F₁
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
inst✝³ : NormedSpace ℝ F₂
inst✝² : NormedAddCommGroup F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℝ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
g : E → F₂
hg : ContDiff ℝ (↑n) g
k : ℕ
hk : ↑k ≤ n
⊢ ∃ s C,
    0 ≤ C ∧
      ∀ (f : 𝓓^{n}_{K}(E, F₁)),
        ∀ x ∈ K,
          ‖iteratedFDeriv ℝ k (fun x ↦ (B (f x)) (g x)) x‖ ≤
            C * (s.sup fun j ↦ ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K j) f

Tactic:
case =>

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
A : Finset β
⊢ Fintype.card ↑↑A = A.card

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
A : Finset β
⊢ LinearIndependent 𝕜 fun (x : ↑↑A) ↦ ↑b ↑x

Tactic:
· exact Fintype.card_coe A

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
⊢ LinearIndependent 𝕜 fun (x : ↑↑A) ↦ ↑b ↑x
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(⋯.lift (-n • ↑z✝)) = (starRingEnd ℂ) ↑(⋯.lift (n • ↑z✝))

Tactic:
rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_zsmul]

Goal state after:
case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(⋯.lift ↑(-n • z✝)) = (starRingEnd ℂ) ↑(⋯.lift ↑(n • z✝))
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
m n : ℤ
x : AddCircle T
⊢ (fourier (m + n)) x = (fourier m) x * (fourier n) x

Tactic:
simp_rw [fourier_apply, add_zsmul, toCircle_add, Circle.coe_mul]

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 : 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
n : ℕ
⊢ (D.P n) x = (∑ i ∈ Finset.range n, succSub D.P i) x

Tactic:
sum_succSub D.P D.proj_zero

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
n : ℕ
⊢ (D.P n) x = (D.P n) x
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: 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)

Tactic:
have h := hL2.memLp_liftIoc.haarAddCircle

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)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ HasSum (fun i ↦ ‖fourierCoeffOn hab f i‖ ^ 2) ((b - a)⁻¹ • ∫ (x : ℝ) in a..b, ‖f x‖ ^ 2)
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case e'_6
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ (b - a)⁻¹ • ∫ (x : ℝ) in a..a + (b - a), ‖f x‖ ^ 2 =
    ∫ (t : AddCircle (b - a)), ‖↑↑(MemLp.toLp (liftIoc (b - a) a f) h) t‖ ^ 2 ∂haarAddCircle

Tactic:
← AddCircle.integral_liftIoc_eq_intervalIntegral,

Goal state after:
case e'_6
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ (b - a)⁻¹ • ∫ (a_1 : AddCircle (b - a)), liftIoc (b - a) a (fun x ↦ ‖f x‖ ^ 2) a_1 =
    ∫ (t : AddCircle (b - a)), ‖↑↑(MemLp.toLp (liftIoc (b - a) a f) h) t‖ ^ 2 ∂haarAddCircle
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
f : 𝓢(E, F →L[ℝ] G)
x : E
⊢ ‖x‖ ^ k * (‖m‖ * ‖iteratedFDeriv ℝ n (⇑f) x‖) ≤ ‖m‖ * (SchwartzMap.seminorm 𝕜 k n) f

Tactic:
by
      move_mul [‖m‖]
      gcongr
      apply le_seminorm

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

Goal state before:
pp: 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 φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
⊢ ∃ M > 0, ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε

Tactic:
refine ⟨max M 1, zero_lt_one.trans_le (le_max_right _ _), fun x hx ↦ hM ?_⟩

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 φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
x : F
hx : x ∈ (closedBall 0 (max M 1))ᶜ
⊢ x ∈ (closedBall 0 M)ᶜ
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x ↦ x ^ s) (Ioi (max 1 t)) volume
x : ℝ
hx : x ∈ Ioi (max 1 t)
x_one : 1 ≤ x
⊢ x⁻¹ ≤ x ^ s

Tactic:
← Real.rpow_neg_one x

Goal state after:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x ↦ x ^ s) (Ioi (max 1 t)) volume
x : ℝ
hx : x ∈ Ioi (max 1 t)
x_one : 1 ≤ x
⊢ x ^ (-1) ≤ x ^ s
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
⊢ ∀ x ∈ uIoc 0 c,
    ‖I * (cexp (-b * (↑T + ↑x * I) ^ 2) - cexp (-b * (↑T - ↑x * I) ^ 2))‖ ≤
      2 * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))

Tactic:
intro y hy
    have absy : |y| ≤ |c| := by
      simpa using abs_sub_left_of_mem_uIcc (uIoc_subset_uIcc hy)
    rw [norm_mul, norm_I, one_mul, two_mul]
    refine (norm_sub_le _ _).trans (add_le_add (vert_norm_bound hT absy) ?_)
    rw [← abs_neg y] at absy
    simpa only [neg_mul, ofReal_neg] using! vert_norm_bound hT absy

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

Goal state before:
pp: case a
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
⊢ -↑n✝ < s + 1

Tactic:
rw [Nat.cast_add, Nat.cast_one, neg_add] at hs'
        linarith

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

Goal state before:
pp: case h
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
B :
  Tendsto
    (fun x ↦
      π ^ (-↑(finrank ℝ V) / 2) * ((fun x ↦ x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w ↦ π ^ 2 * ‖w‖ ^ 2) x)
    (cobounded V) (𝓝 0)
⊢ Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ V * φ x) (cobounded V) (𝓝 0)

Tactic:
convert! B using 2 with x

Goal state after:
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
B :
  Tendsto
    (fun x ↦
      π ^ (-↑(finrank ℝ V) / 2) * ((fun x ↦ x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w ↦ π ^ 2 * ‖w‖ ^ 2) x)
    (cobounded V) (𝓝 0)
x : V
⊢ ‖x‖ ^ finrank ℝ V * φ x =
    π ^ (-↑(finrank ℝ V) / 2) * ((fun x ↦ x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w ↦ π ^ 2 * ‖w‖ ^ 2) x
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)
⊢ ‖(𝓕 f).toLp 2 volume‖ = ‖f.toLp 2 volume‖

Tactic:
simp_rw [norm_eq_sqrt_re_inner (𝕜 := ℂ), inner_fourier_toL2_eq]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst✝³ : FunLike F α β
inst✝² : TopologicalSpace α
inst✝¹ : Zero β
inst✝ : Zero V
f : F → V
ι : Sort u_11
p : ι → Prop
s : ι → Set α
x : α
hl : (𝓝 x).HasBasis p s
⊢ (∃ᶠ (u : Set α) in (𝓝 x).smallSets, ¬IsVanishingOn f u) ↔ ∀ (i : ι), p i → ¬IsVanishingOn f (s i)

Tactic:
exact hl.frequently_smallSets not_isVanishingOn_mono

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

Goal state before:
pp: case left
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 : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
⊢ AEStronglyMeasurable (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) volume

Tactic:
have : (fun x : E ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)).HasTemperateGrowth := by
        fun_prop

Goal state after:
case left
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 : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
this : Function.HasTemperateGrowth fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)
⊢ AEStronglyMeasurable (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) volume
Module: Mathlib.Analysis.RCLike.Inner

Goal state before:
pp: ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ ↦ ⟪f k₁, f k₂⟫ₙ_[𝕜] = 0
h✝ : Nonempty ι
⊢ Pairwise fun k₁ k₂ ↦ ⟪f k₁, f k₂⟫_[𝕜] = 0

Tactic:
by
      simpa [wInner_cWeight_eq_smul_wInner_one, ← NNRat.cast_smul_eq_nnqsmul 𝕜] using hinner

Goal state after:
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
ι : Type
w✝ : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
hn' : ∀ (i : ι), NeZero (n i)
f : α → AddChar α ℂ := fun a ↦ coeHom.compAddChar ((mkZModAux n ⇑(e a)).compAddMonoidHom ↑e)
⊢ Fintype.card (AddChar α ℂ) = Fintype.card α

Tactic:
have hf : Injective f := circleEquivComplex.injective.comp
    ((compAddMonoidHom_injective_left _ e.surjective).comp <| mkZModAux_injective.comp <|
      DFunLike.coe_injective.comp <| e.injective.comp Additive.ofMul.injective)

Goal state after:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
ι : Type
w✝ : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
hn' : ∀ (i : ι), NeZero (n i)
f : α → AddChar α ℂ := fun a ↦ coeHom.compAddChar ((mkZModAux n ⇑(e a)).compAddMonoidHom ↑e)
hf : Injective f
⊢ Fintype.card (AddChar α ℂ) = Fintype.card α
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n k : ℕ+
⊢ k.Coprime n → (k * m).gcd n = m.gcd n

Tactic:
apply Coprime.gcd_mul_left_cancel

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ n + 1 > 0 → ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔ (↑ζ • f') (n + 1) = g' (n + 1)

Tactic:
rw [coe_zeta_smul_apply]

Goal state after:
case succ
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ n + 1 > 0 → ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔ ∑ i ∈ (n + 1).divisors, f' i = g' (n + 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ ↑ζ • f' = g' ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
trans μ • g' = f'

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ ↑ζ • f' = g' ↔ μ • g' = f'

R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ μ • g' = f' ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n