mathlib-initiative/mathlib-tactics huggingface dataset:
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
m x : E
h₁ : |(1 + ‖x‖ ^ 2) ^ (-1 / 2)| ^ 2 = (1 + ‖x‖ ^ 2)⁻¹
⊢ ‖m‖ ^ 2 * ‖x‖ ^ 2 ≤ ‖m‖ ^ 2 * (1 + ‖x‖ ^ 2)

Tactic:
]

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
m x : E
h₁ : |(1 + ‖x‖ ^ 2) ^ (-1 / 2)| ^ 2 = (1 + ‖x‖ ^ 2)⁻¹
⊢ ‖m‖ ^ 2 * ‖x‖ ^ 2 ≤ ‖m‖ ^ 2 * (1 + ‖x‖ ^ 2)
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
m x : E
h₁ : |(1 + ‖x‖ ^ 2) ^ (-1 / 2)| ^ 2 = (1 + ‖x‖ ^ 2)⁻¹
h₂ : |inner ℝ x m| ^ 2 ≤ ‖m‖ ^ 2 * (1 + ‖x‖ ^ 2)
⊢ ‖m‖ ^ 2 * (1 + ‖x‖ ^ 2) * (1 + ‖x‖ ^ 2)⁻¹ ≤ ‖m‖ ^ 2

Tactic:
]

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
m x : E
h₁ : |(1 + ‖x‖ ^ 2) ^ (-1 / 2)| ^ 2 = (1 + ‖x‖ ^ 2)⁻¹
h₂ : |inner ℝ x m| ^ 2 ≤ ‖m‖ ^ 2 * (1 + ‖x‖ ^ 2)
⊢ ‖m‖ ^ 2 * (1 + ‖x‖ ^ 2) * (1 + ‖x‖ ^ 2)⁻¹ ≤ ‖m‖ ^ 2
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ fourierCoeff ⋯.lift m = ∫ (x : ℝ) in 0..1, e x * (∑' (n : ℤ), f.comp (ContinuousMap.addRight ↑n)) x

Tactic:
by
      simp_rw [fourierCoeff_eq_intervalIntegral _ m 0, div_one, one_smul, zero_add, e, comp_apply,
        coe_mk, Periodic.lift_coe, zsmul_one, smul_eq_mul]

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 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(‖x‖ ^ 2 * (1 + ‖x‖ ^ 2) ^ (-1))) f)

Tactic:
]

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.Analysis.Fourier.PoissonSummation

Goal state before:
pp: f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ), e x * f x = ∫ (v : ℝ), cexp (↑(-2 * π * v * ↑m) * I) • f v

Tactic:
]

Goal state after:
f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ), e x * f x = ∫ (v : ℝ), cexp (↑(-2 * π * v * ↑m) * I) • f v
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case h
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
x : E
⊢ ‖↑(‖x‖ ^ 2 * ((1 + ‖x‖ ^ 2) ^ 1)⁻¹)‖ ≤ 1

Tactic:
]

Goal state after:
case h
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
x : E
⊢ ‖↑(‖x‖ ^ 2 * ((1 + ‖x‖ ^ 2) ^ 1)⁻¹)‖ ≤ 1
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
⊢ 1 / 2 = 1 / 2

pp: case h
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
⊢ ‖w‖ ^ 2 ≠ 0

Tactic:
]

Goal state after:
case h
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
⊢ ‖w‖ ^ 2 ≠ 0
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: case h
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
⊢ ¬w = 0

Tactic:
]

Goal state after:
case h
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
⊢ ¬w = 0
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case e_f
f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
x : ℝ
⊢ cexp (2 * ↑π * I * ↑(-m) * ↑x / ↑1) * f x = cexp (↑(-2 * π * x * ↑m) * I) * f x

Tactic:
]

Goal state after:
case e_f
f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
x : ℝ
⊢ cexp (2 * ↑π * I * ↑(-m) * ↑x / ↑1) * f x = cexp (↑(-2 * π * x * ↑m) * I) * f x
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case h
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
x : E
⊢ ‖x‖ ^ 2 ≤ 1 * (1 + ‖x‖ ^ 2) ^ 1

Tactic:
]

Goal state after:
case h
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
x : E
⊢ ‖x‖ ^ 2 ≤ 1 * (1 + ‖x‖ ^ 2) ^ 1
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: n m : ℕ+
h : 0 < (↑n).lcm ↑m * (↑n).gcd ↑m
⊢ 0 < (↑n).lcm ↑m

Tactic:
]

Goal state after:
n m : ℕ+
h : 0 < (↑n).lcm ↑m * (↑n).gcd ↑m
⊢ 0 < (↑n).lcm ↑m
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: n : ℕ+
⊢ n = 1 → n = 1

Tactic:
]

Goal state after:
n : ℕ+
⊢ n = 1 → n = 1
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: p m : ℕ+
pp : p.Prime
⊢ ↑m ∣ ↑p ↔ m = 1 ∨ m = p

Tactic:
]

Goal state after:
p m : ℕ+
pp : p.Prime
⊢ ↑m ∣ ↑p ↔ m = 1 ∨ m = p
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: p m : ℕ+
pp : p.Prime
⊢ ↑m = 1 ∨ ↑m = ↑p ↔ m = 1 ∨ m = p

Tactic:
]

Goal state after:
p m : ℕ+
pp : p.Prime
⊢ ↑m = 1 ∨ ↑m = ↑p ↔ m = 1 ∨ m = p
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: p : ℕ+
pp : p.Prime
contra : p = 1
⊢ p = 1

Tactic:
]

Goal state after:
p : ℕ+
pp : p.Prime
contra : p = 1
⊢ p = 1
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: p : ℕ+
pp : p.Prime
⊢ ¬↑p ∣ ↑1

Tactic:
]

Goal state after:
p : ℕ+
pp : p.Prime
⊢ ¬↑p ∣ ↑1
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime ⟨p, ⋯⟩ ∧ ↑⟨p, ⋯⟩ ∣ ↑n

Tactic:
]

Goal state after:
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime ⟨p, ⋯⟩ ∧ ↑⟨p, ⋯⟩ ∣ ↑n
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n : ℕ+
⊢ (↑m).gcd ↑n = 1 ↔ ↑(m.gcd n) = ↑1

Tactic:
]

Goal state after:
m n : ℕ+
⊢ (↑m).gcd ↑n = 1 ↔ ↑(m.gcd n) = ↑1
Module: Mathlib.Data.PNat.Prime

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

Tactic:
]

Goal state after:
k m n : ℕ+
⊢ (↑m).Coprime ↑k → n.Coprime k → (m * n).Coprime k
Module: Mathlib.Data.PNat.Prime

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

Tactic:
]

Goal state after:
k m n : ℕ+
⊢ (↑m).Coprime ↑k → (↑n).Coprime ↑k → (m * n).Coprime k
Module: Mathlib.Data.PNat.Prime

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

Tactic:
]

Goal state after:
k m n : ℕ+
⊢ (↑m).Coprime ↑k → (↑n).Coprime ↑k → (↑(m * n)).Coprime ↑k
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
⊢ (-1)⁻¹ = (-1)⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Data.PNat.Prime

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

Tactic:
]

Goal state after:
k m n : ℕ+
⊢ (↑m).Coprime ↑k → (↑n).Coprime ↑k → (↑m * ↑n).Coprime ↑k
Module: Mathlib.Data.PNat.Prime

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

Tactic:
]

Goal state after:
k m n : ℕ+
⊢ (↑k).Coprime ↑m → k.Coprime n → k.Coprime (m * n)
Module: Mathlib.Data.PNat.Prime

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

Tactic:
]

Goal state after:
k m n : ℕ+
⊢ (↑k).Coprime ↑m → (↑k).Coprime ↑n → k.Coprime (m * n)
Module: Mathlib.Data.PNat.Prime

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

Tactic:
]

Goal state after:
k m n : ℕ+
⊢ (↑k).Coprime ↑m → (↑k).Coprime ↑n → (↑k).Coprime ↑(m * n)
Module: Mathlib.Data.PNat.Prime

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

Tactic:
]

Goal state after:
k m n : ℕ+
⊢ (↑k).Coprime ↑m → (↑k).Coprime ↑n → (↑k).Coprime (↑m * ↑n)
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n : ℕ+
⊢ ↑(m.gcd n) = ↑m ↔ (↑m).gcd ↑n = ↑m

Tactic:
]

Goal state after:
m n : ℕ+
⊢ ↑(m.gcd n) = ↑m ↔ (↑m).gcd ↑n = ↑m
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
this : (fun v ↦ 𝐞 (-⟪v, w⟫) • f (v + i w)) = fun v ↦ (fun x ↦ -(𝐞 (-⟪x, w⟫) • f x)) (v + i w)
⊢ ∫ (x : V), -(𝐞 (-⟪x, w⟫) • f x) ∂volume = -∫ (v : V), 𝐞 (-⟪v, w⟫) • f v

Tactic:
]

Goal state after:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
this : (fun v ↦ 𝐞 (-⟪v, w⟫) • f (v + i w)) = fun v ↦ (fun x ↦ -(𝐞 (-⟪x, w⟫) • f x)) (v + i w)
⊢ ∫ (x : V), -(𝐞 (-⟪x, w⟫) • f x) ∂volume = -∫ (v : V), 𝐞 (-⟪v, w⟫) • f v
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n : ℕ+
⊢ m.gcd n = m ↔ m ∣ n

Tactic:
]

Goal state after:
m n : ℕ+
⊢ m.gcd n = m ↔ m ∣ n
Module: Mathlib.Data.PNat.Prime

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

Tactic:
]

Goal state after:
m n k : ℕ+
⊢ k.Coprime n → (k * m).gcd n = m.gcd n
Module: Mathlib.Data.PNat.Prime

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

Tactic:
]

Goal state after:
m n k : ℕ+
h : k.Coprime m
⊢ (k * n).gcd m = m.gcd n
Module: Mathlib.Data.PNat.Prime

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

Tactic:
]

Goal state after:
m n k : ℕ+
h : k.Coprime m
⊢ n.gcd m = (k * n).gcd m
Module: Mathlib.Data.PNat.Prime

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

Tactic:
]

Goal state after:
m n k : ℕ+
⊢ k.Coprime m → m.gcd (k * n) = m.gcd n
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: n : ℕ+
⊢ 1 ∣ n

Tactic:
]

Goal state after:
n : ℕ+
⊢ 1 ∣ n
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: n : ℕ+
⊢ gcd 1 n = 1

Tactic:
]

Goal state after:
n : ℕ+
⊢ gcd 1 n = 1
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n : ℕ+
⊢ n.gcd m = 1 → n.gcd m = 1

Tactic:
]

Goal state after:
m n : ℕ+
⊢ n.gcd m = 1 → n.gcd m = 1
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m k n : ℕ+
⊢ ↑m ∣ ↑k → k.Coprime n → m.Coprime n

Tactic:
]

Goal state after:
m k n : ℕ+
⊢ ↑m ∣ ↑k → k.Coprime n → m.Coprime n
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m k n : ℕ+
⊢ ↑m ∣ ↑k → (↑k).Coprime ↑n → m.Coprime n

Tactic:
]

Goal state after:
m k n : ℕ+
⊢ ↑m ∣ ↑k → (↑k).Coprime ↑n → m.Coprime n
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m k n : ℕ+
⊢ ↑m ∣ ↑k → (↑k).Coprime ↑n → (↑m).Coprime ↑n

Tactic:
]

Goal state after:
m k n : ℕ+
⊢ ↑m ∣ ↑k → (↑k).Coprime ↑n → (↑m).Coprime ↑n
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ a = (a * b).gcd m

Tactic:
]

Goal state after:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ a = (a * b).gcd m
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)

Tactic:
]

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ (a * b).gcd m = a.gcd m

Tactic:
]

Goal state after:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ (a * b).gcd m = a.gcd m
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (a * b).gcd m

Tactic:
]

Goal state after:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (a * b).gcd m
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (b * a).gcd m

Tactic:
]

Goal state after:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (b * a).gcd m
Module: Mathlib.Data.PNat.Prime

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

Tactic:
]

Goal state after:
k m n : ℕ+
h : (↑m).Coprime ↑n
⊢ k.gcd (m * n) = k.gcd m * k.gcd n
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ y ^ (-b) ≤ (1 / 2 * x) ^ (-b)

pp: case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 0 ≤ 1 / 2

pp: case hy
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 0 ≤ x

Tactic:
]

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ y ^ (-b) ≤ (1 / 2 * x) ^ (-b)

case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 0 ≤ 1 / 2

case hy
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 0 ≤ x
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n : ℕ+
k l : ℕ
h : (↑m).Coprime ↑n
⊢ (↑m ^ k).Coprime (↑n ^ l)

Tactic:
]

Goal state after:
m n : ℕ+
k l : ℕ
h : (↑m).Coprime ↑n
⊢ (↑m ^ k).Coprime (↑n ^ l)
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

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

Tactic:
]

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

Goal state before:
pp: n : ℕ
⊢ if Squarefree n then 1 ≤ 1 else 0 ≤ 1

Tactic:
]

Goal state after:
n : ℕ
⊢ if Squarefree n then 1 ≤ 1 else 0 ≤ 1
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v = (1 / 2 * 2) • ∫ (a : V), 𝐞 (-⟪a, w⟫) • f a

pp: case hf
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ Integrable (fun v ↦ 𝐞 (-⟪v, w⟫) • f v) volume

pp: case hg
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ Integrable (fun v ↦ 𝐞 (-⟪v, w⟫) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w)) volume

Tactic:
]

Goal state after:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v = (1 / 2 * 2) • ∫ (a : V), 𝐞 (-⟪a, w⟫) • f a

case hf
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ Integrable (fun v ↦ 𝐞 (-⟪v, w⟫) • f v) volume

case hg
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hf : Integrable f volume
⊢ Integrable (fun v ↦ 𝐞 (-⟪v, w⟫) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w)) volume
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
⊢ -1 = -1

Tactic:
]

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

Goal state before:
pp: case pos
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : k = 1
⊢ -1 = -1

Tactic:
]

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

Goal state before:
pp: case neg
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ 0 = 0

pp: case neg
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree (p ^ k)

Tactic:
]

Goal state after:
case neg
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree (p ^ k)
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case neg
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree p ∨ ¬k = 1

Tactic:
]

Goal state after:
case neg
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree p ∨ ¬k = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Nat.Prime (p ^ k)
⊢ 0 = 0

pp: case hnc
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Nat.Prime (p ^ k)
⊢ ¬k = 1

Tactic:
]

Goal state after:
case hnc
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Nat.Prime (p ^ k)
⊢ ¬k = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: ⊢ μ 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → μ (m * n) = μ m * μ n

Tactic:
]

Goal state after:
⊢ μ 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → μ (m * n) = μ m * μ n
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 + f p = 1 + f p

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∑ i ∈ n.divisors, f i = ∑ d ∈ n.divisors, f d

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 - f p = 1 + ↑(-1) * f p

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 - f p = 1 + ↑(-1) * f p
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∑ d ∈ n.divisors, ((↑μ).pmul f) d = ∑ d ∈ n.divisors, ↑(μ d) * f d

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∑ d ∈ n.divisors, ((↑μ).pmul f) d = ∑ d ∈ n.divisors, ↑(μ d) * f d
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case zero
⊢ 0 = 0

Tactic:
]

Goal state after: