mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Tactic:
constructor
  · intro hξ
    obtain ⟨i, hik, rfl⟩ := h.eq_pow_of_mem_rootsOfUnity hξ.pow_eq_one
    rw [h.pow_iff_coprime <| NeZero.pos k] at hξ
    exact ⟨i, hik, hξ, rfl⟩
  · rintro ⟨i, -, hi, rfl⟩; exact h.pow_of_coprime i hi

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

Goal state before:
pp: case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) (P ^ 2) * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
⊢ False

Tactic:
Polynomial.map_pow

Goal state after:
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
⊢ False
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg.refine_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
i : ℕ
hin : i < k
hi : i.Coprime k
H : ζ ^ i = ξ
⊢ ∃ a, (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ

Tactic:
exact ⟨i, ⟨hin, hi.symm⟩, H⟩

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

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
m : ℕ
hcop : m.Coprime n
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ m)

Tactic:
by
  revert n hcop
  refine UniqueFactorizationMonoid.induction_on_prime m ?_ ?_ ?_
  · intro h hn
    congr
    simpa [(Nat.coprime_zero_left _).mp hn] using h
  · intro u hunit _ _
    congr
    simp [Nat.isUnit_iff.mp hunit]
  · intro a p _ hprime hind h hcop
    rw [hind h (Nat.Coprime.coprime_mul_left hcop)]; clear hind
    replace hprime := hprime.nat_prime
    have hdiv := (Nat.Prime.coprime_iff_not_dvd hprime).1 (Nat.Coprime.coprime_mul_right hcop)
    have := Fact.mk hprime
    rw [minpoly_eq_pow (h.pow_of_coprime a (Nat.Coprime.coprime_mul_left hcop)) hdiv]
    congr 1
    ring

Goal state after:
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
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
heq : (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0
⊢ (cyclotomic n R).coeff 0 = 1

Tactic:
have hzero : (X ^ n - 1 : R[X]).coeff 0 = (-1 : R) := by
    rw [coeff_zero_eq_eval_zero _]
    simp only [zero_pow (by positivity : n ≠ 0), eval_X, eval_one, zero_sub, eval_pow, eval_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
heq : (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0
hzero : (X ^ n - 1).coeff 0 = -1
⊢ (cyclotomic n R).coeff 0 = 1
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
hx' : IsIntegral K ⟨x, ⋯⟩
⊢ Basis (Fin (minpoly K x).natDegree) K ↥K[x]

Tactic:
apply Basis.mk (v := fun i : Fin _ ↦ ⟨x, subset_adjoin (Set.mem_singleton x)⟩ ^ (i : ℕ))

Goal state after:
case hli
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
hx' : IsIntegral K ⟨x, ⋯⟩
⊢ LinearIndependent K fun i ↦ ⟨x, ⋯⟩ ^ ↑i

case hsp
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
hx' : IsIntegral K ⟨x, ⋯⟩
⊢ ⊤ ≤ Submodule.span K (Set.range fun i ↦ ⟨x, ⋯⟩ ^ ↑i)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this✝ : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1)
⊢ map (algebraMap (ZMod p) R) (cyclotomic n (ZMod p) ^ (p - 1)) =
    map (algebraMap (ZMod p) R) (cyclotomic n (ZMod p)) ^ (p - 1)

Tactic:
Polynomial.map_pow

Goal state after:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this✝ : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1)
⊢ map (algebraMap (ZMod p) R) (cyclotomic n (ZMod p)) ^ (p - 1) =
    map (algebraMap (ZMod p) R) (cyclotomic n (ZMod p)) ^ (p - 1)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this✝ : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p
⊢ map (algebraMap (ZMod p) R) (cyclotomic n (ZMod p) ^ p) = map (algebraMap (ZMod p) R) (cyclotomic n (ZMod p)) ^ p

Tactic:
Polynomial.map_pow

Goal state after:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this✝ : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p
⊢ map (algebraMap (ZMod p) R) (cyclotomic n (ZMod p)) ^ p = map (algebraMap (ZMod p) R) (cyclotomic n (ZMod p)) ^ p
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
⊢ (cyclotomic (p ^ k * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m

Tactic:
rcases k.eq_zero_or_pos with (rfl | hk)

Goal state after:
case inl
m p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
⊢ (cyclotomic (p ^ 0 * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m

case inr
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
⊢ (cyclotomic (p ^ k * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case inl
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : GCDMonoid.lcm l n = n * r
ineq : φ n * φ r ≤ φ (GCDMonoid.lcm l n)
rpos : 0 < r
key : r = 1
⊢ l ∣ 2 * n

Tactic:
key,

Goal state after:
case inl
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : GCDMonoid.lcm l n = n * 1
ineq : φ n * φ r ≤ φ (GCDMonoid.lcm l n)
rpos : 0 < r
key : r = 1
⊢ l ∣ 2 * n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ False

Tactic:
rw [← Finset.prod_sdiff (s₁ := {n})] at this

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ((∏ x ∈ (n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ)) *
        ∏ x ∈ {n}, eval 1 (cyclotomic x ℤ))
⊢ False

R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ {n} ⊆ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n))
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case inr
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : GCDMonoid.lcm l n = n * r
ineq : φ n * φ r ≤ φ (GCDMonoid.lcm l n)
rpos : 0 < r
key : r = 2
⊢ l ∣ 2 * n

Tactic:
key,

Goal state after:
case inr
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : GCDMonoid.lcm l n = n * 2
ineq : φ n * φ r ≤ φ (GCDMonoid.lcm l n)
rpos : 0 < r
key : r = 2
⊢ l ∣ 2 * n
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case pos
n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
h1 : n = 1
⊢ (Algebra.norm K) ζ = 1

pp: case neg
n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
h1 : ¬n = 1
⊢ (Algebra.norm K) ζ = 1

Tactic:
· rw [h1, one_right_iff] at hζ
    rw [hζ, show 1 = algebraMap K L 1 by simp, Algebra.norm_algebraMap, one_pow]

Goal state after:
case neg
n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
h1 : ¬n = 1
⊢ (Algebra.norm K) ζ = 1
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
⊢ (Algebra.norm K) ζ = 1

Tactic:
have hz := congr_arg (norm K) ((IsPrimitiveRoot.iff_def _ n).1 hζ).1
  rw [← (algebraMap K L).map_one, Algebra.norm_algebraMap, one_pow, map_pow, ← one_pow n] at hz
  exact StrictMono.injective hodd.strictMono_pow hz

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
⊢ ∃ k, (x + k * n).Coprime m

Tactic:
use ps.prod id

Goal state after:
case h
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := ⋯
⊢ (x + ps.prod id * n).Coprime m
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) (2 ^ (k + 1) / 2 ^ k)
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Tactic:
rw [Nat.pow_div (le_succ k) zero_lt_two, Nat.succ_sub (le_refl k), Nat.sub_self, pow_one] at this

Goal state after:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case inr
n : ℤ
m : ℕ
hm : m ≠ 0
this : NeZero m
u : (ZMod m)ˣ
hu : ↑u = ↑n
h_coprime : (↑n).val.Coprime m
⊢ IsCoprime (↑m) n

Tactic:
Nat.coprime_iff_gcd_eq_one,

Goal state after:
case inr
n : ℤ
m : ℕ
hm : m ≠ 0
this : NeZero m
u : (ZMod m)ˣ
hu : ↑u = ↑n
h_coprime : (↑n).val.gcd m = 1
⊢ IsCoprime (↑m) n
Module: Mathlib.Data.Int.Range

Goal state before:
pp: m n r : ℤ
h : m ≤ r ∧ r < n
⊢ m + ↑(r - m).toNat < n ∧ m + ↑(r - m).toNat = r

Tactic:
by simp [toNat_of_nonneg (sub_nonneg.2 h.1), h.2]

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

Goal state before:
pp: case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ χ⁻¹ a = χ a⁻¹ʳ

pp: case neg
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : ¬IsUnit a
⊢ χ⁻¹ a = χ a⁻¹ʳ

Tactic:
· rw [inv_apply_eq_inv]
    have h := IsUnit.map χ ha
    apply_fun (χ a * ·) using IsUnit.mul_right_injective h
    dsimp only
    rw [Ring.mul_inverse_cancel _ h, ← map_mul, Ring.mul_inverse_cancel _ ha, map_one]

Goal state after:
case neg
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : ¬IsUnit a
⊢ χ⁻¹ a = χ a⁻¹ʳ
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : DecidableEq F
ζ : R
hζ : IsPrimitiveRoot ζ (Fintype.card Fˣ)
⊢ Fintype.card Fˣ ∣ Fintype.card F - 1

Tactic:
rw [Fintype.card_units]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
⊢ χ ↑x ^ p = χ ↑x

Tactic:
rcases hχ x with (hx | hx | hx) <;> rw [hx]

Goal state after:
case inl
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = 0
⊢ 0 ^ p = 0

case inr.inl
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = 1
⊢ 1 ^ p = 1

case inr.inr
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = -1
⊢ (-1) ^ p = -1
Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
u : (ZMod N)ˣ
hu : (ZMod.unitsMap hd) u = 1
a : ℤ
ha : ↑(↑u).val - 1 = ↑d * a
this : ↑u - 1 = ↑(↑(↑u).val - 1)
⊢ e.mulShift (↑u - 1) = 1

Tactic:
rw [this, ha]

Goal state after:
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
u : (ZMod N)ˣ
hu : (ZMod.unitsMap hd) u = 1
a : ℤ
ha : ↑(↑u).val - 1 = ↑d * a
this : ↑u - 1 = ↑(↑(↑u).val - 1)
⊢ e.mulShift ↑(↑d * a) = 1
Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
u : (ZMod N)ˣ
hu : ↑(ZMod.castHom hd (ZMod d)) ↑u = 1
this : (ZMod.castHom hd (ZMod d)) ↑u = ↑↑(↑u).val
⊢ ↑d ∣ ↑(↑u).val - 1

Tactic:
MonoidHom.coe_coe,

Goal state after:
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
u : (ZMod N)ˣ
hu : (ZMod.castHom hd (ZMod d)) ↑u = 1
this : (ZMod.castHom hd (ZMod d)) ↑u = ↑↑(↑u).val
⊢ ↑d ∣ ↑(↑u).val - 1
Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
⊢ χ.FactorsThrough d

Tactic:
rw [DirichletCharacter.factorsThrough_iff_ker_unitsMap hd]

Goal state after:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
⊢ (ZMod.unitsMap hd).ker ≤ (MulChar.toUnitHom χ).ker
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 ∈ {0}ᶜ, ψ a + ψ 0 = 0

Tactic:
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✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
⊢ gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ = χ (-1) * ↑(Fintype.card R)

Tactic:
have h : χ ^ (orderOf χ - 1) = χ⁻¹ := by
    refine (inv_eq_of_mul_eq_one_right ?_).symm
    rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos χ.orderOf_pos, pow_orderOf_eq_one]

Goal state after:
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) = χ⁻¹
⊢ gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ = χ (-1) * ↑(Fintype.card R)
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) (ψ.mulShift ↑p) = χ ↑p * gaussSum χ ψ

Tactic:
hχ.pow_char p,

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 ↑p) = χ ↑p * gaussSum χ ψ
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) * ‖x‖) = p * ‖x‖ ^ (p - 1)

Tactic:
rw [← Real.rpow_add_one' (by positivity) (by linarith)]

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.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
f : Finset α → β
inst✝ : DecidableEq α
⊢ StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s < f (insert a s)

Tactic:
by
  simp [strictMono_iff_forall_lt_cons]

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

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ ⟪a -ᵥ b, a -ᵥ c⟫ = dist a c ^ 2 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0

Tactic:
by
  rw [real_inner_comm, inner_vsub_vsub_left_eq_dist_sq_left_iff, real_inner_comm]

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

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
t₁ t₂ : ℝ
h_inner : ⟪b -ᵥ a, c -ᵥ a⟫ = 0
⊢ dist ((AffineMap.lineMap a b) t₁) ((AffineMap.lineMap a c) t₂) ^ 2 = t₁ ^ 2 * dist a b ^ 2 + t₂ ^ 2 * dist a c ^ 2

Tactic:
have hvec : AffineMap.lineMap a b t₁ -ᵥ AffineMap.lineMap a c t₂ =
              t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a) := by
    rw [AffineMap.lineMap_apply, AffineMap.lineMap_apply, vadd_vsub_vadd_cancel_right]

Goal state after:
V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
t₁ t₂ : ℝ
h_inner : ⟪b -ᵥ a, c -ᵥ a⟫ = 0
hvec : (AffineMap.lineMap a b) t₁ -ᵥ (AffineMap.lineMap a c) t₂ = t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
⊢ dist ((AffineMap.lineMap a b) t₁) ((AffineMap.lineMap a c) t₂) ^ 2 = t₁ ^ 2 * dist a b ^ 2 + t₂ ^ 2 * dist a c ^ 2
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : (↑#ι).HolderConjugate p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
⊢ 1 < #ι

Tactic:
exact Fintype.one_lt_card

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hA : A.IsSymmetric
hB : B.IsSymmetric
hAB : Commute A B
⊢ ⨆ j, ⨆ i, eigenspace A (i, j).2 ⊓ eigenspace B (i, j).1 = ⊤

Tactic:
exact iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute hA hB hAB

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[ℝ] ℝ
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
v w : V
mem_w_orthogonal : w ∈ (↑(continuousLinearMapOfBilin B)).rangeᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ C * (‖w‖ * ‖w‖) = 0

Tactic:
←
      mul_assoc

Goal state after:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
v w : V
mem_w_orthogonal : w ∈ (↑(continuousLinearMapOfBilin B)).rangeᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ C * ‖w‖ * ‖w‖ = 0