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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
f : S ≃ₐ[R] S
⊢ μ ^ (↑((autToPow R hμ) f)).val = f μ

Tactic:
rw [IsPrimitiveRoot.coe_autToPow_apply]

Goal state after:
R : Type u_4
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
f : S ≃ₐ[R] S
⊢ μ ^ (↑⋯.choose).val = f μ
Module: Mathlib.FieldTheory.Galois.Abelian

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Field M
inst✝³ : Algebra K M
inst✝² : Algebra L M
inst✝¹ : IsScalarTower K L M
inst✝ : IsAbelianGalois K M
this : IsGalois K L
x y : Gal(M/K)
⊢ (AlgEquiv.restrictNormalHom L) x * (AlgEquiv.restrictNormalHom L) y =
    (AlgEquiv.restrictNormalHom L) y * (AlgEquiv.restrictNormalHom L) x

Tactic:
← map_mul,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Field M
inst✝³ : Algebra K M
inst✝² : Algebra L M
inst✝¹ : IsScalarTower K L M
inst✝ : IsAbelianGalois K M
this : IsGalois K L
x y : Gal(M/K)
⊢ (AlgEquiv.restrictNormalHom L) (x * y) = (AlgEquiv.restrictNormalHom L) y * (AlgEquiv.restrictNormalHom L) x
Module: Mathlib.FieldTheory.Galois.Abelian

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Field M
inst✝³ : Algebra K M
inst✝² : Algebra L M
inst✝¹ : IsScalarTower K L M
inst✝ : IsAbelianGalois K M
this : IsGalois K L
x y : Gal(M/K)
⊢ (AlgEquiv.restrictNormalHom L) (x * y) = (AlgEquiv.restrictNormalHom L) y * (AlgEquiv.restrictNormalHom L) x

Tactic:
← map_mul,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Field M
inst✝³ : Algebra K M
inst✝² : Algebra L M
inst✝¹ : IsScalarTower K L M
inst✝ : IsAbelianGalois K M
this : IsGalois K L
x y : Gal(M/K)
⊢ (AlgEquiv.restrictNormalHom L) (x * y) = (AlgEquiv.restrictNormalHom L) (y * x)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case h.inr.inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : 0 = ∑ i ∈ range n, x ^ i
⊢ 0 < eval x (cyclotomic n R)

pp: case h.inr.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : ∑ i ∈ range n, x ^ i < 0
⊢ 0 < eval x (cyclotomic n R)

Tactic:
· rw [eq_comm, geom_sum_eq_zero_iff_neg_one hn'.ne'] at h
    exact h.1.symm ▸ cyclotomic_neg_one_pos hn

Goal state after:
case h.inr.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : ∑ i ∈ range n, x ^ i < 0
⊢ 0 < eval x (cyclotomic n R)
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_self_sdiff_zero,

Goal state after:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ IsCyclotomicExtension ({0} \ {0}) A B → ⊥ = ⊤
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ ∀ x ∈ ⊤, x ∈ (X ^ p ^ n - X).rootSet (GaloisField p n)

Tactic:
rw [← SplittingField.adjoin_rootSet]

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ ∀ x ∈ Algebra.adjoin (ZMod p) ((X ^ p ^ n - X).rootSet (X ^ p ^ n - X).SplittingField),
    x ∈ (X ^ p ^ n - X).rootSet (GaloisField p n)
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ ∃ r < n, x = ζ ^ r ∨ x = -ζ ^ r

Tactic:
obtain ⟨r, hr⟩ := hζ.exists_neg_pow_of_isOfFinOrder hno hx

Goal state after:
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
r : ℕ
hr : x = (-ζ) ^ r
⊢ ∃ r < n, x = ζ ^ r ∨ x = -ζ ^ r
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 : Units.mk0 (q - 1).toNNReal ⋯ ^ φ n < Units.mk0 ‖eval (↑q) (cyclotomic n ℂ)‖₊ ⋯
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)

Tactic:
simp only [← Units.val_lt_val, Units.val_pow_eq_pow_val, Units.val_mk0, ← NNReal.coe_lt_coe,
      hq'.le, coe_nnnorm, NNReal.coe_pow, Real.coe_toNNReal', sub_nonneg, sup_of_le_left] at this

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 ℂ)‖
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case pos
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : n = 0
⊢ IsCyclotomicExtension (S ∪ {0}) A B

Tactic:
eq_self_sdiff_zero,

Goal state after:
case pos
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : n = 0
⊢ IsCyclotomicExtension ((S ∪ {0}) \ {0}) A B
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case mem
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
x✝ x : B
n : ℕ
hn1 : n ∈ S
hn2 : n ≠ 0
hx : x ^ n = 1
⊢ ⟨x, ⋯⟩ ∈ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}

Tactic:
exact subset_adjoin ⟨n, hn1, hn2, Subtype.val_injective hx⟩

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

Goal state before:
pp: S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
⊢ ∀ (x : ↥(adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})), x ∈ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}

Tactic:
by
    rintro ⟨x, hx⟩
    induction hx using adjoin_induction with
    | mem x hx =>
      obtain ⟨n, hn1, hn2, hx⟩ := hx
      exact subset_adjoin ⟨n, hn1, hn2, Subtype.val_injective hx⟩
    | algebraMap x => exact Subalgebra.algebraMap_mem _ x
    | add x y hx hy ihx ihy => exact Subalgebra.add_mem _ ihx ihy
    | mul x y hx hy ihx ihy => exact Subalgebra.mul_mem _ ihx ihy

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

Goal state before:
pp: case pos
S✝ : Set ℕ
n : ℕ
S : Set ℕ
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
hn : n = 0
this : insert n S \ {0} = S \ {0}
⊢ Module.Finite A B

Tactic:
eq_self_sdiff_zero,

Goal state after:
case pos
S✝ : Set ℕ
n : ℕ
S : Set ℕ
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S \ {0}) A B
hn : n = 0
this : insert n S \ {0} = S \ {0}
⊢ Module.Finite A B
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
m : ℤ
h : IsCoprime m ↑n
⊢ ↑(↑m)⁻¹.val * ↑m = 1

Tactic:
by
  rw [mul_comm, coe_int_mul_val_inv h]

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

Goal state before:
pp: case inl
n : ℤ
h : IsUnit ↑n
⊢ IsCoprime (↑0) n

Tactic:
rw [Nat.cast_zero, isCoprime_zero_left]
    exact_mod_cast h

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : Finite G
inst✝² : IsCyclic G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Nat.card G)
hord : Nat.card ↥(rootsOfUnity (Nat.card G) M) = Nat.card G
⊢ Nonempty ((G →* Mˣ) ≃* G)

Tactic:
let e := (IsCyclic.monoidHom_mulEquiv_rootsOfUnity G Mˣ).some

Goal state after:
G : Type u_1
M : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : Finite G
inst✝² : IsCyclic G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Nat.card G)
hord : Nat.card ↥(rootsOfUnity (Nat.card G) M) = Nat.card G
e : (G →* Mˣ) ≃* ↥(rootsOfUnity (Nat.card G) Mˣ) := ⋯.some
⊢ Nonempty ((G →* Mˣ) ≃* G)
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this✝ : Finite F
this : Fintype F
⊢ Nonempty (K →ₐ[F] L)

Tactic:
have := Module.finite_of_finrank_pos (Nat.pos_of_dvd_of_pos h Module.finrank_pos)

Goal state after:
F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this✝¹ : Finite F
this✝ : Fintype F
this : Module.Finite F K
⊢ Nonempty (K →ₐ[F] L)
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✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this✝¹ : NeZero ↑n
k : K
this✝ : ∀ (z : K), ∃ x, z * (algebraMap A K) ↑x.2 = (algebraMap A K) x.1
z : A
w : ↥(nonZeroDivisors A)
hw : k * (algebraMap A K) ↑(z, w).2 = (algebraMap A K) (z, w).1
this : IsScalarTower A K (CyclotomicField n K) := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ (algebraMap K (CyclotomicField n K)) k * (algebraMap K (CyclotomicField n K)) ((algebraMap A K) ↑w) =
    (algebraMap A (CyclotomicField n K)) z

Tactic:
← map_mul,

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✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this✝¹ : NeZero ↑n
k : K
this✝ : ∀ (z : K), ∃ x, z * (algebraMap A K) ↑x.2 = (algebraMap A K) x.1
z : A
w : ↥(nonZeroDivisors A)
hw : k * (algebraMap A K) ↑(z, w).2 = (algebraMap A K) (z, w).1
this : IsScalarTower A K (CyclotomicField n K) := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ (algebraMap K (CyclotomicField n K)) (k * (algebraMap A K) ↑w) = (algebraMap A (CyclotomicField n K)) z
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_3
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✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
y z : CyclotomicField n K
a : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
ha :
  y * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.1
b : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
hb :
  z * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.1
⊢ (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.1 *
        (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2 +
      z * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2 *
        (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) (a.1 * ↑b.2 + b.1 * ↑a.2, ⟨↑a.2 * ↑b.2, ⋯⟩).1

Tactic:
hb

Goal state after:
case refine_3
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✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
y z : CyclotomicField n K
a : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
ha :
  y * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.1
b : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
hb :
  z * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.1
⊢ (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.1 *
        (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2 +
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.1 *
        (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) (a.1 * ↑b.2 + b.1 * ↑a.2, ⟨↑a.2 * ↑b.2, ⋯⟩).1
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : Fintype M
inst✝¹ : DecidableEq M
R : Type u_2
inst✝ : CommMonoidWithZero R
inst_cyc : IsCyclic Mˣ
χ : MulChar M R
⊢ (fun ζ ↦ ofRootOfUnity ⋯ ⋯) ((fun χ ↦ ⟨χ.toUnitHom (Classical.choose ⋯), ⋯⟩) χ) = χ

Tactic:
simp only [toUnitHom_eq, eq_iff <| Classical.choose_spec inst_cyc.exists_generator,
      ofRootOfUnity_spec, coe_equivToUnitHom]

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
h : IsUnit (χ a)
⊢ 1 = χ a * χ a⁻¹ʳ

Tactic:
← map_mul,

Goal state after:
case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (χ a)
⊢ 1 = χ (a * a⁻¹ʳ)
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
⊢ ∑ a, χ (a * b⁻¹) * ψ (a - b) = ∑ c, χ c * ψ (b * (c - 1))

Tactic:
refine (Fintype.sum_bijective _ (mulLeft_bijective₀ b hb) _ _ fun x ↦ ?_).symm

Goal state after:
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 - 1)) = χ (b * x * b⁻¹) * ψ (b * x - b)
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
x y : R
| χ y * χ x⁻¹ * (ψ y * ψ (-x))

Tactic:
← map_mul,

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
x y : R
| χ (y * x⁻¹) * (ψ y * ψ (-x))
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‖ ^ p) = fun x ↦ ‖x‖ * ‖x‖ ^ (p - 1)

Tactic:
by
          ext x
          rw [← rpow_one_add' (norm_nonneg x) (by positivity)]
          ring_nf

Goal state after:
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 ↑⊥

Tactic:
bot_eq_zero

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.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:
simp only [← MulChar.ringHomComp_apply]

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'
⊢ ((χ.ringHomComp (algebraMap F' FF')) (-1) * ↑(Fintype.card F)) ^ (ringChar FF' ^ ↑n' / 2) =
    (χ.ringHomComp (algebraMap F' FF')) (↑(ringChar FF') ^ ↑n')
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Function.Even (𝓕 Φ) ↔ Function.Even Φ

Tactic:
have h {f : ZMod N → ℂ} (hf : f.Even) : (𝓕 f).Even := by
    simp only [Function.Even, ← congr_fun (dft_comp_neg f), funext hf, implies_true]
  refine ⟨fun hΦ x ↦ ?_, h⟩
  simpa only [neg_neg, smul_right_inj (NeZero.ne (N : ℂ)), dft_dft] using h hΦ (-x)

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
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
h₁ : (fun a ↦ ↑(χ₈ a) * τ ^ ↑a) = fun a ↦ χ a * ψ₈char a
⊢ ↑0 * τ ^ ↑0 + ↑1 * τ ^ ↑1 + ↑0 * τ ^ ↑2 + ↑(-1) * τ ^ 3 + ↑0 * τ ^ ↑4 + ↑(-1) * τ ^ 5 + ↑0 * τ ^ ↑6 + ↑1 * τ ^ ↑7 =
    2 * (τ - τ ^ 3)

Tactic:
show ((7 : Fin 8) : ℕ) = 7 from rfl

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
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
h₁ : (fun a ↦ ↑(χ₈ a) * τ ^ ↑a) = fun a ↦ χ a * ψ₈char a
⊢ ↑0 * τ ^ ↑0 + ↑1 * τ ^ ↑1 + ↑0 * τ ^ ↑2 + ↑(-1) * τ ^ 3 + ↑0 * τ ^ ↑4 + ↑(-1) * τ ^ 5 + ↑0 * τ ^ ↑6 + ↑1 * τ ^ 7 =
    2 * (τ - τ ^ 3)
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
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
h₁ : (fun a ↦ ↑(χ₈ a) * τ ^ ↑a) = fun a ↦ χ a * ψ₈char a
hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3)
⊢ (2 * (τ - τ ^ 3)) ^ 2 = 8

Tactic:
linear_combination (4 * τ ^ 2 - 8) * τ_spec

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

Goal state before:
pp: case neg
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
ι : Type u_2
inst✝ : LinearOrder ι
v : ι → E
hv : Orthonormal ℝ v
s t : ↑(Set.powersetCard ι n)
h : ¬s = t
x : ι
hxs : ∀ (x_1 : Fin n), ¬(Set.powersetCard.ofFinEmbEquiv.symm s) x_1 = x
hxt : ∃ y, (Set.powersetCard.ofFinEmbEquiv.symm t) y = x
⊢ (of fun i j ↦
        ⟪(v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm s)) j, (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm t)) i⟫).det =
    0

Tactic:
obtain ⟨i, rfl⟩ := hxt

Goal state after:
case neg
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
ι : Type u_2
inst✝ : LinearOrder ι
v : ι → E
hv : Orthonormal ℝ v
s t : ↑(Set.powersetCard ι n)
h : ¬s = t
i : Fin n
hxs : ∀ (x : Fin n), ¬(Set.powersetCard.ofFinEmbEquiv.symm s) x = (Set.powersetCard.ofFinEmbEquiv.symm t) i
⊢ (of fun i j ↦
        ⟪(v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm s)) j, (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm t)) i⟫).det =
    0