mathlib-initiative/mathlib-tactics huggingface dataset:
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
hL : Continuous fun p ↦ (L p.1) p.2
⊢ char he hL 0 = 1

Tactic:
ext

Goal state after:
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
hL : Continuous fun p ↦ (L p.1) p.2
x✝ : V
⊢ (char he hL 0) x✝ = 1 x✝
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
hL : Continuous fun p ↦ (L p.1) p.2
x y : W
⊢ char he hL (x + y) = char he hL x * char he hL y

Tactic:
ext

Goal state after:
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
hL : Continuous fun p ↦ (L p.1) p.2
x y : W
x✝ : V
⊢ (char he hL (x + y)) x✝ = (char he hL x * char he hL y) x✝
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
hL : Continuous fun p ↦ (L p.1) p.2
w : W
⊢ char he hL (-w) = star (char he hL w)

Tactic:
ext

Goal state after:
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
hL : Continuous fun p ↦ (L p.1) p.2
w : W
x✝ : V
⊢ (char he hL (-w)) x✝ = (star (char he hL w)) x✝
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this✝ :
  (fourier (Pi.single i 1 i)) (z i) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1, (fourier (Pi.single i 1 i_1)) (z i_1)
this : (fourier (Pi.single i 1 i)) (z i) * {i}ᶜ.prod ?m.57 = ∏ i_1, (fourier (Pi.single i 1 i_1)) (z i_1)
⊢ (fourier (Pi.single i 1 i)) (z i) * {i}ᶜ.prod ?m.57 = (fourier 1) (z i)

Tactic:
Finset.prod_const_one,

Goal state after:
d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this✝ :
  (fourier (Pi.single i 1 i)) (z i) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1, (fourier (Pi.single i 1 i_1)) (z i_1)
this : (fourier (Pi.single i 1 i)) (z i) * ∏ _x ∈ {i}ᶜ, 1 = ∏ i_1, (fourier (Pi.single i 1 i_1)) (z i_1)
⊢ (fourier (Pi.single i 1 i)) (z i) * 1 = (fourier 1) (z i)
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
hL : Continuous fun p ↦ (L p.1) p.2
y : AddMonoidAlgebra ℂ W
z : AddMonoidAlgebra ℂ W := AddMonoidAlgebra.map (starRingEnd ℂ).toAddMonoidHom y
⊢ ∃ x, (charAlgHom he hL) x = star ((charAlgHom he hL) y)

Tactic:
let f : W ↪ W := ⟨fun x ↦ -x, (fun _ _ ↦ neg_inj.mp)⟩

Goal state after:
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
hL : Continuous fun p ↦ (L p.1) p.2
y : AddMonoidAlgebra ℂ W
z : AddMonoidAlgebra ℂ W := AddMonoidAlgebra.map (starRingEnd ℂ).toAddMonoidHom y
f : W ↪ W := { toFun := fun x ↦ -x, inj' := ⋯ }
⊢ ∃ x, (charAlgHom he hL) x = star ((charAlgHom he hL) y)
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
hL : Continuous fun p ↦ (L p.1) p.2
y : AddMonoidAlgebra ℂ W
z : AddMonoidAlgebra ℂ W := AddMonoidAlgebra.map (starRingEnd ℂ).toAddMonoidHom y
f : W ↪ W := { toFun := fun x ↦ -x, inj' := ⋯ }
⊢ (charAlgHom he hL) (AddMonoidAlgebra.ofCoeff (Finsupp.embDomain f z.coeff)) = star ((charAlgHom he hL) y)

Tactic:
ext

Goal state after:
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
hL : Continuous fun p ↦ (L p.1) p.2
y : AddMonoidAlgebra ℂ W
z : AddMonoidAlgebra ℂ W := AddMonoidAlgebra.map (starRingEnd ℂ).toAddMonoidHom y
f : W ↪ W := { toFun := fun x ↦ -x, inj' := ⋯ }
x✝ : V
⊢ ((charAlgHom he hL) (AddMonoidAlgebra.ofCoeff (Finsupp.embDomain f z.coeff))) x✝ = (star ((charAlgHom he hL) y)) x✝
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
hL : Continuous fun p ↦ (L p.1) p.2
w : W
⊢ (charAlgHom he hL).toRingHom (AddMonoidAlgebra.single w 1) = char he hL w

Tactic:
ext

Goal state after:
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
hL : Continuous fun p ↦ (L p.1) p.2
w : W
x✝ : V
⊢ ((charAlgHom he hL).toRingHom (AddMonoidAlgebra.single w 1)) x✝ = (char he hL w) x✝
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢'(E, F)
⊢ (smulLeftCLM F g₂) ((smulLeftCLM F g₁) f) = (smulLeftCLM F (g₁ * g₂)) f

Tactic:
ext

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢'(E, F)
x✝ : 𝓢(E, ℂ)
⊢ ((smulLeftCLM F g₂) ((smulLeftCLM F g₁) f)) x✝ = ((smulLeftCLM F (g₁ * g₂)) f) x✝
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)
⊢ MemSobolev s 2 f ↔ ∃ f', (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'

Tactic:
constructor

Goal state after:
case mp
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)
⊢ MemSobolev s 2 f → ∃ f', (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'

case mpr
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)
⊢ (∃ f', (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f') → MemSobolev s 2 f
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
f : 𝓢'(E, F)
⊢ 𝓕⁻ (𝓕 f) = f

Tactic:
ext

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
f : 𝓢'(E, F)
x✝ : 𝓢(E, ℂ)
⊢ (𝓕⁻ (𝓕 f)) x✝ = f x✝
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
f : 𝓢'(E, F)
⊢ 𝓕 (𝓕⁻ f) = f

Tactic:
ext

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
f : 𝓢'(E, F)
x✝ : 𝓢(E, ℂ)
⊢ (𝓕 (𝓕⁻ f)) x✝ = f x✝
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 : ℝ
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
⊢ MemLp (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume

Tactic:
constructor

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
⊢ AEStronglyMeasurable (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) volume

case right
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
⊢ eLpNorm (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume < ∞
Module: Mathlib.Analysis.RCLike.Inner

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
w f g : ι → ℝ
hw : 0 ≤ w
⊢ |⟪f, g⟫_[ℝ, w]| ≤ ⟪|f|, |g|⟫_[ℝ, w]

Tactic:
by
  simpa using! norm_wInner_le (𝕜 := ℝ) hw

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
n✝ : ℕ
a b : α
n : ℕ
inst✝ : NeZero n
⊢ Bijective ⇑(circleEquivComplex.toAddMonoidHom.comp zmodHom.toAddMonoidHom)

Tactic:
Fintype.bijective_iff_injective_and_card,

Goal state after:
α : Type u_1
inst✝¹ : AddCommGroup α
n✝ : ℕ
a b : α
n : ℕ
inst✝ : NeZero n
⊢ Injective ⇑(circleEquivComplex.toAddMonoidHom.comp zmodHom.toAddMonoidHom) ∧
    Fintype.card (ZMod n) = Fintype.card (AddChar (ZMod n) ℂ)
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
n✝ : ℕ
a b : α
n : ℕ
inst✝ : NeZero n
⊢ ZMod n ≃+ AddChar (ZMod n) ℂ

Tactic:
refine AddEquiv.ofBijective
    (circleEquivComplex.toAddMonoidHom.comp <| AddChar.toAddMonoidHom zmodHom) ?_
  rw [Fintype.bijective_iff_injective_and_card, card_eq]
  exact ⟨circleEquivComplex.injective.comp zmod_injective, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Finite α
ψ : AddChar α ℂ
⊢ (complexBasis α) ψ = ⇑ψ

Tactic:
by rw [coe_complexBasis]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ (∃ ψ, ψ a ≠ 1) → a ≠ 0

Tactic:
rintro ⟨ψ, hψ⟩ rfl

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Finite α
ψ : AddChar α ℂ
hψ : ψ 0 ≠ 1
⊢ False
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: n : ℕ
⊢ μ n ≠ 0 ↔ Squarefree n

Tactic:
constructor

Goal state after:
case mp
n : ℕ
⊢ μ n ≠ 0 → Squarefree n

case mpr
n : ℕ
⊢ Squarefree n → μ n ≠ 0
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' ↔ μ • g' = f'

Tactic:
constructor

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

case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ μ • g' = f' → ↑ζ • f' = g'
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ × ℕ
hx : x ∈ n.divisorsAntidiagonal
⊢ ↑(Units.mk0 (g x.2) ⋯ ^ μ x.1) = g x.2 ^ μ x.1

Tactic:
Units.val_zpow_eq_zpow_val,

Goal state after:
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ × ℕ
hx : x ∈ n.divisorsAntidiagonal
⊢ ↑(Units.mk0 (g x.2) ⋯) ^ μ x.1 = g x.2 ^ μ x.1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

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

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) → ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n) → ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
F : ℕ → R := fun n ↦ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d ∈ n.divisors, F d = g n
⊢ ∑ i ∈ n.divisors, f i = g n

Tactic:
rw [← this, sum_congr rfl]

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
F : ℕ → R := fun n ↦ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d ∈ n.divisors, F d = g n
⊢ ∀ x ∈ n.divisors, f x = F x
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ × ℕ
hx : x ∈ n.divisorsAntidiagonal
⊢ ↑(Units.mk0 (g x.2) ⋯ ^ μ x.1) = g x.2 ^ μ x.1

Tactic:
Units.val_zpow_eq_zpow_val,

Goal state after:
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ × ℕ
hx : x ∈ n.divisorsAntidiagonal
⊢ ↑(Units.mk0 (g x.2) ⋯) ^ μ x.1 = g x.2 ^ μ x.1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
⊢ IsPrimitiveRoot ζ k

Tactic:
by
  refine ⟨h1, fun l hl ↦ ?_⟩
  suffices k.gcd l = k from this ▸ k.gcd_dvd_right l
  refine (Nat.le_of_dvd hk (k.gcd_dvd_left l)).eq_of_not_lt fun h' ↦ ?_
  exact h _ (Nat.gcd_pos_of_pos_left _ hk) h' (by simp [h1, hl])

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖ ≤ ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (⇑f =O[atBot] fun x ↦ |x| ^ (-b)) ∧ ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
⊢ ((fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[atBot] fun x ↦ |x| ^ (-b)) ∧
    (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[atTop] fun x ↦ |x| ^ (-b)

Tactic:
constructor

Goal state after:
case left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖ ≤ ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (⇑f =O[atBot] fun x ↦ |x| ^ (-b)) ∧ ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
⊢ (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[atBot] fun x ↦ |x| ^ (-b)

case right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖ ≤ ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (⇑f =O[atBot] fun x ↦ |x| ^ (-b)) ∧ ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
⊢ (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[atTop] fun x ↦ |x| ^ (-b)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ζ : M
⊢ IsPrimitiveRoot ζ 1 ↔ ζ = 1

Tactic:
constructor

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoid M
ζ : M
⊢ IsPrimitiveRoot ζ 1 → ζ = 1

case mpr
M : Type u_1
inst✝ : CommMonoid M
ζ : M
⊢ ζ = 1 → IsPrimitiveRoot ζ 1
Module: Mathlib.Topology.ContinuousMap.Periodic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p : X
⊢ Function.Periodic (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)))) p

Tactic:
by
  intro x
  by_cases h : Summable fun n : ℤ => f.comp (ContinuousMap.addRight (n • p))
  · convert! congr_arg (fun f : C(X, Y) => f x) ((Equiv.addRight (1 : ℤ)).tsum_eq _) using 1
    -- This `have` unfolds the function composition in `Equiv.summable_iff`.

    -- This `have` unfolds the function composition in `Equiv.summable_iff`.
    have : Summable fun (c : ℤ) => f.comp (ContinuousMap.addRight (Equiv.addRight 1 c • p)) :=
      (Equiv.addRight (1 : ℤ)).summable_iff.mpr h
    simp_rw [← tsum_apply h, ← tsum_apply this]
    simp [Equiv.coe_addRight, comp_apply, add_one_zsmul, add_comm (_ • p) p, ← add_assoc]
  · rw [tsum_eq_zero_of_not_summable h]
    simp only [coe_zero, Pi.zero_apply]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
⊢ (∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) ∧
    ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l

Tactic:
constructor

Goal state after:
case left
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
⊢ ∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)

case right
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
⊢ ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n ↔ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

Tactic:
constructor

Goal state after:
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n → ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

case mpr
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ) → IsPrimitiveRoot ζ n
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case mpr
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : i.Coprime n
⊢ IsPrimitiveRoot (cexp (2 * ↑π * I * (↑i / ↑n))) n

Tactic:
exact isPrimitiveRoot_exp_of_coprime i n hn hi

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
⊢ ↑x ^ n = 1 ↔ ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

Tactic:
constructor

Goal state after:
case mp
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
⊢ ↑x ^ n = 1 → ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

case mpr
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
⊢ (∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x) → ↑x ^ n = 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h✝ h : IsPrimitiveRoot ζ k
⊢ Function.Bijective
    ⇑(((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
        ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)

Tactic:
constructor

Goal state after:
case left
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h✝ h : IsPrimitiveRoot ζ k
⊢ Function.Injective
    ⇑(((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
        ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)

case right
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h✝ h : IsPrimitiveRoot ζ k
⊢ Function.Surjective
    ⇑(((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
        ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)