mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
⊢ (cyclotomic n R).coeff 0 = 1

Tactic:
have hprod : (∏ i ∈ Nat.properDivisors n, (Polynomial.cyclotomic i R).coeff 0) = -1 := by
    rw [← Finset.insert_erase (Nat.one_mem_properDivisors_iff_one_lt.2
      (lt_of_lt_of_le one_lt_two hn)), Finset.prod_insert (Finset.notMem_erase 1 _),
      cyclotomic_one R]
    have hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j := by
      intro j hj
      apply Nat.succ_le_of_lt
      exact (Ne.le_iff_lt (Finset.mem_erase.1 hj).1.symm).mp
        (Nat.succ_le_of_lt (Nat.pos_of_mem_properDivisors (Finset.mem_erase.1 hj).2))
    have hcongr : ∀ j ∈ n.properDivisors.erase 1, (cyclotomic j R).coeff 0 = 1 := by
      intro j hj
      exact hi j (Nat.mem_properDivisors.1 (Finset.mem_erase.1 hj).2).2 (hleq j hj)
    have hrw : (∏ x ∈ n.properDivisors.erase 1, (cyclotomic x R).coeff 0) = 1 := by
      rw [Finset.prod_congr (refl (n.properDivisors.erase 1)) hcongr]
      simp only [Finset.prod_const_one]
    simp only [hrw, mul_one, zero_sub, coeff_one_zero, coeff_X_zero, coeff_sub]

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
⊢ (cyclotomic n R).coeff 0 = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this✝ : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
x✝ : cyclotomic p ℚ ∣ P
c : ℚ[X]
hP' : ↑(p - 1) + c.degree ≤ ↑(p - 1)
hc : P = cyclotomic p ℚ * c
this : c.degree ≤ 0
⊢ ∀ (i j : Fin p), α i = α j

Tactic:
obtain ⟨c, rfl⟩ := natDegree_eq_zero.mp (natDegree_eq_zero_iff_degree_le_zero.mpr this)

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this✝ : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
x✝ : cyclotomic p ℚ ∣ P
c : ℚ
hP' : ↑(p - 1) + (C c).degree ≤ ↑(p - 1)
hc : P = cyclotomic p ℚ * C c
this : (C c).degree ≤ 0
⊢ ∀ (i j : Fin p), α i = α j
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ (algebraMap R K) (x ^ n) - (algebraMap R K) (y ^ n) = (algebraMap R K) (∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y))

Tactic:
map_pow,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ (algebraMap R K) x ^ n - (algebraMap R K) (y ^ n) = (algebraMap R K) (∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ (algebraMap R K) x ^ n - (algebraMap R K) (y ^ n) = (algebraMap R K) (∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y))

Tactic:
map_pow,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ (algebraMap R K) x ^ n - (algebraMap R K) y ^ n = (algebraMap R K) (∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y))
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ IsCyclotomicExtension {0} A B ↔ ⊤ = ⊥

Tactic:
eq_comm

Goal state after:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ IsCyclotomicExtension {0} A B ↔ ⊥ = ⊤
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
L : Type v
inst✝⁴ : CommRing L
ζ : L
hζ : IsPrimitiveRoot ζ n
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Algebra K L
hodd : Odd n
hz : (Algebra.norm K) (ζ ^ n) = 1
⊢ (Algebra.norm K) ζ = 1

Tactic:
map_pow,

Goal state after:
n : ℕ
L : Type v
inst✝⁴ : CommRing L
ζ : L
hζ : IsPrimitiveRoot ζ n
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Algebra K L
hodd : Odd n
hz : (Algebra.norm K) ζ ^ n = 1
⊢ (Algebra.norm K) ζ = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : (q - 1) ^ φ n < ‖eval (↑q) (cyclotomic n ℂ)‖
⊢ eval q (cyclotomic n ℝ) = ‖eval (↑q) (cyclotomic n ℂ)‖

Tactic:
eq_comm

Goal state after:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : (q - 1) ^ φ n < ‖eval (↑q) (cyclotomic n ℂ)‖
⊢ ‖eval (↑q) (cyclotomic n ℂ)‖ = eval q (cyclotomic n ℝ)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ¬0 = (-ζ).arg

Tactic:
eq_comm

Goal state after:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ¬(-ζ).arg = 0
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
⊢ IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))

Tactic:
sub_add_cancel

Goal state after:
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
⊢ IsPrimitiveRoot (ζ ^ p ^ s) (p ^ (k + 1 - s))
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h✝ : IsCyclotomicExtension {n} A B
x : B
h : x ∈ {b | n ≠ 0 ∧ b ^ n = 1}
⊢ x ∈ ↑(nthRoots n 1).toFinset

Tactic:
by simpa [n.pos_of_neZero] using h.2

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case e'_3
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : ‖eval (↑q) (cyclotomic n ℂ)‖ < max (q + 1) 0 ^ φ n
⊢ eval q (cyclotomic n ℝ) = ‖eval (↑q) (cyclotomic n ℂ)‖

Tactic:
eq_comm

Goal state after:
case e'_3
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : ‖eval (↑q) (cyclotomic n ℂ)‖ < max (q + 1) 0 ^ φ n
⊢ ‖eval (↑q) (cyclotomic n ℂ)‖ = eval q (cyclotomic n ℝ)
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case refine_2.e_a
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this✝¹ : IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this✝ : FiniteDimensional K L
this : IsGalois K L
H : (Algebra.norm K) η₁ = ↑(p ^ (k - s + 1)).minFac
⊢ (p ^ (k - s + 1)).minFac = p

Tactic:
rw [Nat.pow_minFac, hpri.1.minFac_eq]

Goal state after:
case refine_2.e_a
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this✝¹ : IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this✝ : FiniteDimensional K L
this : IsGalois K L
H : (Algebra.norm K) η₁ = ↑(p ^ (k - s + 1)).minFac
⊢ k - s + 1 ≠ 0
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case pos
n m : ℕ
hm : NeZero m
h✝ : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h : p ∣ x + ps.prod id * n - x
⊢ False

Tactic:
add_comm,

Goal state after:
case pos
n m : ℕ
hm : NeZero m
h✝ : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h : p ∣ ps.prod id * n + x - x
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ (map (algebraMap K L) (X ^ n - 1)).Splits

Tactic:
rw [Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
    Polynomial.map_X]
  obtain ⟨z, hz⟩ := ((isCyclotomicExtension_iff _ _ _).1 H).1 hS (NeZero.ne _)
  exact X_pow_sub_one_splits hz

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

Goal state before:
pp: S : Set ℕ
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
key : ∀ b ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}, IsAlgebraic K b
⊢ IsCyclotomicExtension S K ↥(IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}).toSubalgebra

Tactic:
congr(IsCyclotomicExtension S K $(IntermediateField.adjoin_toSubalgebra_of_isAlgebraic key))

Goal state after:
S : Set ℕ
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
key : ∀ b ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}, IsAlgebraic K b
⊢ IsCyclotomicExtension S K ↥(adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
n : ℕ
inst✝⁷ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
ζ : (cyclotomic n K).SplittingField
hζ : IsPrimitiveRoot ζ n
⊢ adjoin K {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1} =
    adjoin K ((cyclotomic n K).rootSet (cyclotomic n K).SplittingField)

Tactic:
eq_comm

Goal state after:
case refine_2
n : ℕ
inst✝⁷ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
ζ : (cyclotomic n K).SplittingField
hζ : IsPrimitiveRoot ζ n
⊢ adjoin K ((cyclotomic n K).rootSet (cyclotomic n K).SplittingField) =
    adjoin K {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((2 * (2 * (n / 4)) + n % 4) / 2)

Tactic:
add_comm,

Goal state after:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((n % 4 + 2 * (2 * (n / 4))) / 2)
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : Odd n
hχ : χ ^ n = 1
⊢ χ ((-1) ^ n) = 1

Tactic:
map_pow,

Goal state after:
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : Odd n
hχ : χ ^ n = 1
⊢ χ (-1) ^ n = 1
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝³ : Field R
inst✝² : Fintype R
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
⊢ ∑ a, 1 a * ψ a + 1 = 0

Tactic:
calc ∑ a, (1 : MulChar R R') a * ψ a + 1
  _ = ∑ a ∈ {0}ᶜ, (1 : MulChar R R') a * ψ a + 1 := by
    simp [← ({0} : Finset R).sum_compl_add_sum]
  _ = ∑ a ∈ {0}ᶜ, ψ a + ψ 0 := by
    congr! <;> aesop (add simp MulChar.one_apply)
  _ = 0 := by
    rw [← AddChar.sum_eq_zero_of_ne_one hψ, ← Finset.sum_compl_add_sum (s := {0})]
    simp

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 - x + x = b

Tactic:
sub_add_cancel

Goal state after:
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
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
⊢ (fun x ↦ ‖x‖ * ‖x‖ ^ (p - 1)) =o[𝓝 0] fun x ↦ ‖x‖ * 1

Tactic:
by
        refine (isBigO_refl _ _).mul_isLittleO <| (isLittleO_const_iff <| by simp).mpr ?_
        convert! continuousAt_id.norm.rpow_const (.inr h2p.le) |>.tendsto
        simp [h2p.ne']

Goal state after:
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:
abs_eq_self.mpr <| zero_le_one.trans hp.le,

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.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
⊢ -j + -x = 0 ↔ x = -j

Tactic:
add_comm,

Goal state after:
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 = 0 ↔ x = -j
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:
abs_eq_self.mpr <| zero_le_one.trans hp.le,

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.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ (∃ a, a ::ₘ s = t) → s ⋖ t

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
α : Type u_1
s : Multiset α
a : α
⊢ s ⋖ a ::ₘ s
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' := ⋯
FF' : Type u_2 := ⋯
hchar : ringChar F' = ringChar FF'
⊢ (algebraMap F' FF') ((χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2)) =
    (algebraMap F' FF') (χ ↑(Fintype.card F'))

Tactic:
map_pow,

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)) ^ (Fintype.card F' / 2) = (algebraMap F' FF') (χ ↑(Fintype.card F'))
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
x✝ : Set α
hx✝ : x✝ ∈ Set.range SetLike.coe
s : Finset α
t : Set α
ht : t ∈ Set.Icc x✝ ↑s
⊢ t ∈ Set.range SetLike.coe

Tactic:
exact ⟨_, (s.finite_toSet.subset ht.2).coe_toFinset⟩

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
⊢ ¬ringChar FF ∣ 8

Tactic:
rw [Ne, ← Nat.prime_dvd_prime_iff_eq FFp Nat.prime_two] at hFF

Goal state after:
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ¬ringChar FF ∣ 2
⊢ ¬ringChar FF ∣ 8
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))

Tactic:
let τ : FF := ψ₈char 1

Goal state after:
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
hT' : T ≠ 0
α : 𝕜
h : (α • T).IsPositive
⊢ ?m.48

Tactic:
simpa only [hT.1 _] using hT.ne_zero_iff.mp hT'

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

Goal state before:
pp: V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ ∀ (v : V), C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖

Tactic:
intro v

Goal state after:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
v : V
⊢ C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ True ∧ ∀ (x_1 : E), 0 ≤ (starRingEnd 𝕜) ⟪x, x_1⟫ * ⟪x, x_1⟫

Tactic:
RCLike.conj_mul,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ True ∧ ∀ (x_1 : E), 0 ≤ ↑‖⟪x, x_1⟫‖ ^ 2
Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram

Goal state before:
pp: V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
⊢ ∀ (x : V), x ∈ (↑(continuousLinearMapOfBilin B)).rangeᗮᗮ

Tactic:
intro v

Goal state after:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
v : V
⊢ v ∈ (↑(continuousLinearMapOfBilin B)).rangeᗮᗮ
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_4
inst✝ : Finite n
M : Matrix n n 𝕜
this : Fintype n
⊢ (∃ m u, ∑ x, vecMulVec (u x).ofLp (star (u x).ofLp) = M) ↔ ∃ m v, M = ∑ i, vecMulVec (v i) (star (v i))

Tactic:
eq_comm

Goal state after:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_4
inst✝ : Finite n
M : Matrix n n 𝕜
this : Fintype n
⊢ (∃ m u, M = ∑ x, vecMulVec (u x).ofLp (star (u x).ofLp)) ↔ ∃ m v, M = ∑ i, vecMulVec (v i) (star (v i))
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
x : F × E
h : ∀ (a : E) (a_1 : a ∈ T.domain), ⟪↑T ⟨a, ⋯⟩, x.1⟫ = ⟪a, x.2⟫
⊢ ∀ (x_1 : ↥T.domain), ⟪x.2, ↑x_1⟫ = ⟪x.1, ↑T x_1⟫

Tactic:
rintro ⟨a, ha⟩

Goal state after:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
x : F × E
h : ∀ (a : E) (a_1 : a ∈ T.domain), ⟪↑T ⟨a, ⋯⟩, x.1⟫ = ⟪a, x.2⟫
a : E
ha : a ∈ T.domain
⊢ ⟪x.2, ↑⟨a, ha⟩⟫ = ⟪x.1, ↑T ⟨a, ha⟩⟫