mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∑ x ∈ ?m.163, ?m.165 x = ∑ y, χ x * φ (y - x) * ψ y

pp: case hi
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a ∈ univ, a + x ∈ ?m.163

pp: case i_inj
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a₁ ∈ univ, ∀ a₂ ∈ univ, a₁ + x = a₂ + x → a₁ = a₂

pp: case i_surj
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ b ∈ ?m.163, ∃ a, ∃ (_ : a ∈ univ), a + x = b

pp: case h
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a ∈ univ, χ x * φ a * ψ (x + a) = ?m.165 (a + x)

pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ Finset R

pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ R → R'

Tactic:
]

Goal state after:
case hi
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a ∈ univ, a + x ∈ univ

case i_inj
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a₁ ∈ univ, ∀ a₂ ∈ univ, a₁ + x = a₂ + x → a₁ = a₂

case i_surj
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ b ∈ univ, ∃ a, ∃ (_ : a ∈ univ), a + x = b

case h
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a ∈ univ, χ x * φ a * ψ (x + a) = χ x * φ (a + x - x) * ψ (a + x)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: K : Type w
L : Type z
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
n₁ n₂ : ℕ
F₁ F₂ : IntermediateField K L
h₁ : IsCyclotomicExtension {n₁} K ↥F₁
h₂ : IsCyclotomicExtension {n₂} K ↥F₂
inst✝¹ : NeZero n₁
inst✝ : NeZero n₂
this✝ : FiniteDimensional K ↥F₁
this : IsCyclotomicExtension {n₁.lcm n₂} K ↥(F₁ ⊔ F₂).toSubalgebra
⊢ IsCyclotomicExtension {n₁.lcm n₂} K ↥(F₁ ⊔ F₂)

Tactic:
]

Goal state after:
K : Type w
L : Type z
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
n₁ n₂ : ℕ
F₁ F₂ : IntermediateField K L
h₁ : IsCyclotomicExtension {n₁} K ↥F₁
h₂ : IsCyclotomicExtension {n₂} K ↥F₂
inst✝¹ : NeZero n₁
inst✝ : NeZero n₂
this✝ : FiniteDimensional K ↥F₁
this : IsCyclotomicExtension {n₁.lcm n₂} K ↥(F₁ ⊔ F₂).toSubalgebra
⊢ IsCyclotomicExtension {n₁.lcm n₂} K ↥(F₁ ⊔ F₂)
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = -1
⊢ ψ (-x) = -ψ x

Tactic:
]

Goal state after:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = -1
⊢ ψ (-x) = -ψ x
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = -1
⊢ ψ (-1) * ψ x = -ψ x

Tactic:
]

Goal state after:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = -1
⊢ ψ (-1) * ψ x = -ψ x
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = 1
⊢ ψ (-x) = ψ x

Tactic:
]

Goal state after:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = 1
⊢ ψ (-x) = ψ x
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = 1
⊢ ψ (-1) * ψ x = ψ x

Tactic:
]

Goal state after:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = 1
⊢ ψ (-1) * ψ x = ψ x
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
m : ℕ
χ : DirichletCharacter S m
hχ : χ.Even
x✝ : ZMod m
⊢ χ x✝ = χ x✝

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
m : ℕ
χ : DirichletCharacter S m
hχ : χ.Odd
x✝ : ZMod m
⊢ -χ x✝ = -χ x✝

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x b : R
x✝ : b ∈ univ
⊢ b = b

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x a : R
x✝ : a ∈ univ
⊢ χ x * φ a * ψ (a + x) = χ x * φ a * ψ (a + x)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
sum_eq : ∀ (x : R), ∑ y, χ x * φ y * ψ (x + y) = ∑ y, χ x * φ (y - x) * ψ y
⊢ ∑ y, ∑ x, χ x * φ (y - x) * ψ y = ∑ t, ∑ x, χ x * φ (t - x) * ψ t

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : Field R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
⊢ χ ↑(-1) * gaussSum χ (ψ.mulShift ↑(-1)) = gaussSum χ ψ

Tactic:
]

Goal state after:
R : Type u
inst✝² : Field R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
⊢ χ ↑(-1) * gaussSum χ (ψ.mulShift ↑(-1)) = gaussSum χ ψ
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case inr
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b ≠ 0
x : R
⊢ χ x * ψ (b * x - b) = χ x * ψ (b * x - b)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ y, ∑ x, χ y * ψ (x * (y - 1)) = ↑(Fintype.card R)

Tactic:
]

Goal state after:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ y, ∑ x, χ y * ψ (x * (y - 1)) = ↑(Fintype.card R)
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ (if 1 ∈ Finset.univ then χ 1 * ↑(Fintype.card R) else 0) = ↑(Fintype.card R)

Tactic:
]

Goal state after:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ (if 1 ∈ Finset.univ then χ 1 * ↑(Fintype.card R) else 0) = ↑(Fintype.card R)
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
h : χ ^ (orderOf χ - 1) = χ⁻¹
⊢ χ (-1) * ↑(Fintype.card R) = χ (-1) * ↑(Fintype.card R)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ gaussSum χ ψ * gaussSum χ ψ = gaussSum χ ψ * (gaussSum χ ψ⁻¹ * χ (-1))

Tactic:
]

Goal state after:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ gaussSum χ ψ * gaussSum χ ψ = gaussSum χ ψ * (gaussSum χ ψ⁻¹ * χ (-1))
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝ : E
p : ℝ
hp : 1 < p
hx : x✝ = 0
h2p : 0 < p - 1
x : E
⊢ ‖x‖ ^ p = ‖x‖ ^ (1 + (p - 1))

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝ : E
p : ℝ
hp : 1 < p
hx : x✝ = 0
h2p : 0 < p - 1
x : E
⊢ ‖x‖ ^ p = ‖x‖ ^ (1 + (p - 1))
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case e_a
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ χ ↑(-1) * gaussSum χ (ψ.mulShift ↑(-1)) = χ (-1) * gaussSum χ (ψ.mulShift (-1))

Tactic:
]

Goal state after:
case e_a
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ χ ↑(-1) * gaussSum χ (ψ.mulShift ↑(-1)) = χ (-1) * gaussSum χ (ψ.mulShift (-1))
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
χ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ x, (frobenius R' p) (χ x * ψ x) = ∑ a, (χ ^ p) a * (ψ ^ p) a

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
χ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ x, (frobenius R' p) (χ x * ψ x) = ∑ a, (χ ^ p) a * (ψ ^ p) a
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ ψ ^ p = χ ↑p * gaussSum χ ψ

Tactic:
_root_.gaussSum_frob,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum (χ ^ p) (ψ ^ p) = χ ↑p * gaussSum χ ψ
Module: Mathlib.Order.Grade

Goal state before:
pp: case succ
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : Preorder 𝕆
inst✝³ : Preorder ℙ
inst✝² : Preorder α
inst✝¹ : Preorder β
n✝ : ℕ
inst✝ : GradeMinOrder (Fin (n✝ + 1)) α
a : Fin (n✝ + 1)
h : IsMin a
⊢ IsMin ↑0

Tactic:
]

Goal state after:
case succ
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : Preorder 𝕆
inst✝³ : Preorder ℙ
inst✝² : Preorder α
inst✝¹ : Preorder β
n✝ : ℕ
inst✝ : GradeMinOrder (Fin (n✝ + 1)) α
a : Fin (n✝ + 1)
h : IsMin a
⊢ IsMin ↑0
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖‖f x‖ ^ (p - 2)‖ * ‖(innerSL ℝ) (f x) ∘SL fderiv ℝ f x‖ ≤ p * ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖

Tactic:
]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖‖f x‖ ^ (p - 2)‖ * ‖(innerSL ℝ) (f x) ∘SL fderiv ℝ f x‖ ≤ p * ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ (ψ.mulShift ↑hp.unit) = 1 ↑hp.unit * gaussSum χ (ψ.mulShift ↑hp.unit)

Tactic:
one_apply_coe,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ (ψ.mulShift ↑hp.unit) = 1 * gaussSum χ (ψ.mulShift ↑hp.unit)
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ (ψ.mulShift ↑hp.unit) = gaussSum χ (ψ.mulShift ↑hp.unit)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ ψ = gaussSum χ ψ

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = χ (↑p ^ n) * gaussSum χ ψ
⊢ χ (↑p ^ n) * χ ↑p * gaussSum χ ψ = χ (↑p ^ n) * χ ↑p * gaussSum χ ψ

Tactic:
]

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

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
k j : ZMod N
⊢ stdAddChar (-(j * k)) • Φ (-j) = stdAddChar (-(j * k)) • Φ (-j)

Tactic:
]

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

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ ∑ y, ∑ x, stdAddChar (-((j + y) * x)) • Φ y = ↑N • Φ (-j)

Tactic:
]

Goal state after:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ ∑ y, ∑ x, stdAddChar (-((j + y) * x)) • Φ y = ↑N • Φ (-j)
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: case hbc
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖f x‖ ^ (p - 2 + 1) * ‖fderiv ℝ f x‖ = ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖

Tactic:
]

Goal state after:
case hbc
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖f x‖ ^ (p - 2 + 1) * ‖fderiv ℝ f x‖ = ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : χ (-1) = 0 ∨ ↑(Fintype.card R) = 0
hf : gaussSum χ ψ = 0
⊢ False

Tactic:
]

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : χ (-1) = 0 ∨ ↑(Fintype.card R) = 0
hf : gaussSum χ ψ = 0
⊢ False
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)
this : gaussSum χ ψ ≠ 0
⊢ (gaussSum χ ψ ^ 2) ^ (p ^ n / 2) = χ (↑p ^ n)

Tactic:
]

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)
this : gaussSum χ ψ ≠ 0
⊢ (gaussSum χ ψ ^ 2) ^ (p ^ n / 2) = χ (↑p ^ n)
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖‖x‖ ^ (p - 2)‖ * ‖(innerSL ℝ) x‖ = p * ‖x‖ ^ (p - 1)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖‖x‖ ^ (p - 2)‖ * ‖(innerSL ℝ) x‖ = p * ‖x‖ ^ (p - 1)
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j✝ : ZMod N
h1 : ∀ (t : ZMod N), ∑ i, stdAddChar (t * i) = if t = 0 then ↑N else 0
x j : ZMod N
⊢ x = -j ↔ x = -j

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)
this : gaussSum χ ψ ≠ 0
⊢ gaussSum χ ψ ^ p ^ n = gaussSum χ ψ ^ p ^ n

Tactic:
]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ p * ‖x‖ ^ (p - 2 + 1) = p * ‖x‖ ^ (p - 1)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ p * ‖x‖ ^ (p - 2 + 1) = p * ‖x‖ ^ (p - 1)
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
⊢ s.card ⋖ s.card + 1

Tactic:
]

Goal state after:
α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
⊢ s.card ⋖ s.card + 1
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s✝ t : Multiset α
a : α
s : Multiset α
hs : IsMin s
⊢ IsMin ⊥.card

Tactic:
]

Goal state after:
α : Type u_1
s✝ t : Multiset α
a : α
s : Multiset α
hs : IsMin s
⊢ IsMin ⊥.card
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ (Differentiable ℝ fun x ↦ ‖x‖ ^ p) ∧
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv ℝ fun x ↦ ‖x‖ ^ p)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ (Differentiable ℝ fun x ↦ ‖x‖ ^ p) ∧
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv ℝ fun x ↦ ‖x‖ ^ p)
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto (fun x ↦ ‖fderiv ℝ (fun x ↦ ‖x‖ ^ p) x‖) (𝓝 0) (𝓝 0)

Tactic:
]

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto (fun x ↦ ‖fderiv ℝ (fun x ↦ ‖x‖ ^ p) x‖) (𝓝 0) (𝓝 0)
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (∃ a ∉ t, insert a t = s) ↔ t ⊆ s ∧ #(s \ t) = 1

Tactic:
]

Goal state after:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (∃ a ∉ t, insert a t = s) ↔ t ⊆ s ∧ #(s \ t) = 1
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ ↑n'
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
hchar : ringChar F' = ringChar FF'
⊢ ((algebraMap F' FF') (χ (-1)) * ↑(Fintype.card F)) ^ (ringChar FF' ^ ↑n' / 2) =
    (algebraMap F' FF') (χ (↑(ringChar FF') ^ ↑n'))

Tactic:
]

Goal state after:
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ ↑n'
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
hchar : ringChar F' = ringChar FF'
⊢ ((algebraMap F' FF') (χ (-1)) * ↑(Fintype.card F)) ^ (ringChar FF' ^ ↑n' / 2) =
    (algebraMap F' FF') (χ (↑(ringChar FF') ^ ↑n'))
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
a : α
ha : s \ t = {a}
⊢ s = s

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s✝ t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin ⊥.val

Tactic:
]

Goal state after:
α : Type u_1
s✝ t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin ⊥.val
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s✝ t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin #⊥

Tactic:
]

Goal state after:
α : Type u_1
s✝ t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin #⊥
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: case e_f
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
k j : ZMod N
⊢ ↑(toCircle (-(k * j))) * χ j = ↑(toCircle (-(k * j))) * χ j

Tactic:
]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
k : ZMod N
⊢ χ⁻¹ (-k) * gaussSum χ stdAddChar = χ⁻¹ (-k) * gaussSum χ stdAddChar

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁✝ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ ↑n'
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁✝
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
hch₁ : IsUnit ↑(ringChar FF')
hchar : ringChar F' = ringChar FF'
this✝ : Fact (Nat.Prime (ringChar F'))
this : Fact (Nat.Prime (ringChar FF'))
⊢ ((χ.ringHomComp (algebraMap F' FF')) (-1) * ↑(Fintype.card F)) ^ (ringChar FF' ^ ↑n' / 2) =
    (χ.ringHomComp (algebraMap F' FF')) (↑(ringChar FF') ^ ↑n')

Tactic:
]

Goal state after:
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁✝ : ringChar F' ≠ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ ↑n'
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁✝
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
hch₁ : IsUnit ↑(ringChar FF')
hchar : ringChar F' = ringChar FF'
this✝ : Fact (Nat.Prime (ringChar F'))
this : Fact (Nat.Prime (ringChar FF'))
⊢ ((χ.ringHomComp (algebraMap F' FF')) (-1) * ↑(Fintype.card F)) ^ (ringChar FF' ^ ↑n' / 2) =
    (χ.ringHomComp (algebraMap F' FF')) (↑(ringChar FF') ^ ↑n')