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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
n k : ℕ
inst✝¹ : NeZero ↑n
inst✝ : IsSepClosed F
⊢ ∃ m, IsPrimitiveRoot m n

Tactic:
by
    have : NeZero n := .of_neZero_natCast F
    have := isCyclotomicExtension {n} F fun _ h _ ↦ Set.mem_singleton_iff.mp h ▸ ‹NeZero (n : F)›
    exact IsCyclotomicExtension.exists_isPrimitiveRoot (S := {n}) F _ rfl (NeZero.ne _)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ ↑(toCircle ↑j) = cexp (2 * ↑π * I * ↑j / ↑N)

Tactic:
rw [toCircle, AddChar.compAddMonoidHom_apply, toCircle_addChar, AddChar.coe_mk,
    AddCircle.toCircle, toAddCircle_intCast, Function.Periodic.lift_coe, Circle.coe_exp]

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ cexp (↑(2 * π / 1 * (↑j / ↑N)) * I) = cexp (2 * ↑π * I * ↑j / ↑N)
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ toUnits (toCircle x) ∈ rootsOfUnity n Circle

Tactic:
by ext; simp [← AddChar.map_nsmul_eq_pow]

Goal state after:
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
⊢ y *
        ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 *
          (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2) +
      z *
        ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 *
          (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) (a.1 * ↑b.2 + b.1 * ↑a.2, ⟨↑a.2 * ↑b.2, ⋯⟩).1

Tactic:
← mul_assoc,

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
⊢ y * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 *
        (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2 +
      z *
        ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 *
          (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.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.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:
← mul_assoc,

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 +
      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
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∣ n
⊢ χ.FactorsThrough d ↔ (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker

Tactic:
by
  refine ⟨fun ⟨_, ⟨χ₀, hχ₀⟩⟩ x hx ↦ ?_, fun h ↦ ?_⟩
  · rw [MonoidHom.mem_ker, hχ₀, changeLevel_toUnitHom, MonoidHom.comp_apply, hx, map_one]
  · let E := MonoidHom.liftOfSurjective _ (ZMod.unitsMap_surjective hd) ⟨_, h⟩
    have hE : E.comp (ZMod.unitsMap hd) = χ.toUnitHom := MonoidHom.liftOfRightInverse_comp ..
    refine ⟨hd, MulChar.ofUnitHom E, equivToUnitHom.injective (?_ : toUnitHom _ = toUnitHom _)⟩
    simp_rw [changeLevel_toUnitHom, toUnitHom_eq, ofUnitHom_eq, Equiv.apply_symm_apply, hE,
      toUnitHom_eq]

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

Goal state before:
pp: case refine_4
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
⊢ y *
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 *
        (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.1) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) (a.1 * b.1, ⟨↑a.2 * ↑b.2, ⋯⟩).1

Tactic:
← mul_assoc,

Goal state after:
case refine_4
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
⊢ y * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 *
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.1 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) (a.1 * b.1, ⟨↑a.2 * ↑b.2, ⋯⟩).1
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
inst✝ : IsDomain B
C : Subalgebra A B
h : IsCyclotomicExtension S A ↥C
m : ℕ
ζ : B
h₁ : m ∈ S
h₂ : m ≠ 0
hζ : ζ ^ m = 1
η : ↥C
hη : IsPrimitiveRoot ((algebraMap (↥C) B) η) m
⊢ ζ ∈ C

Tactic:
have : NeZero m := ⟨h₂⟩

Goal state after:
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
h : IsCyclotomicExtension S A ↥C
m : ℕ
ζ : B
h₁ : m ∈ S
h₂ : m ≠ 0
hζ : ζ ^ m = 1
η : ↥C
hη : IsPrimitiveRoot ((algebraMap (↥C) B) η) m
this : NeZero m
⊢ ζ ∈ C
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : χ ↑x = -1
⊢ (χ ↑x)⁻¹ʳ = χ ↑x

Tactic:
· -- Porting note (#11573): was `by norm_cast`
    have : (-1 : R') = (-1 : R'ˣ) := by norm_cast; simp
    rw [h₂, this, Ring.inverse_unit (-1 : R'ˣ), inv_neg, inv_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ⁻¹.conductor = χ.conductor

Tactic:
rw [← zpow_neg_one]
  refine dvd_antisymm (conductor_zpow_dvd ..) ?_
  nth_rewrite 1 [← inv_inv χ, ← zpow_neg_one, ← zpow_neg_one]
  exact conductor_zpow_dvd ..

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
hn : NeZero n
h : χ.conductor.lcm ψ.conductor ∣ n
⊢ χ * ψ = (changeLevel h) (χ.primitiveCharacter.mul ψ.primitiveCharacter)

Tactic:
mul,

Goal state after:
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
hn : NeZero n
h : χ.conductor.lcm ψ.conductor ∣ n
⊢ χ * ψ = (changeLevel h) ((changeLevel ⋯) χ.primitiveCharacter * (changeLevel ⋯) ψ.primitiveCharacter)
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝¹ : NeZero n
inst✝ : Nontrivial R
p : ℕ
hp : Fact (Nat.Prime p)
this : NeZero (n / p ^ n.factorization p)
⊢ χ ∈ subgroupOfPrimitiveMapToOne R n p ↔ χ.primitiveCharacter ↑p = 1

Tactic:
have hcop := Nat.coprime_ordCompl hp.out (NeZero.ne n)

Goal state after:
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝¹ : NeZero n
inst✝ : Nontrivial R
p : ℕ
hp : Fact (Nat.Prime p)
this : NeZero (n / p ^ n.factorization p)
hcop : p.Coprime (n / p ^ n.factorization p)
⊢ χ ∈ subgroupOfPrimitiveMapToOne R n p ↔ χ.primitiveCharacter ↑p = 1
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'
a : Rˣ
⊢ ∑ i, χ ↑a * (χ i * ψ (↑a * i)) = ∑ a, χ a * ψ a

Tactic:
← mul_assoc,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ ∑ x, χ ↑a * χ x * ψ (↑a * x) = ∑ a, χ 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
x : R
⊢ χ x * ψ (b * (x - 1)) = χ (b * (b⁻¹ * x)) * ψ (b * x - b)

Tactic:
← mul_assoc,

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 * b⁻¹ * x) * ψ (b * x - b)
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 ↑p) = χ ↑p * (χ ↑hp.unit * gaussSum χ (ψ.mulShift ↑hp.unit))

Tactic:
← mul_assoc,

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 * χ ↑hp.unit * gaussSum χ (ψ.mulShift ↑hp.unit)
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 * (χ ↑p * gaussSum χ ψ) = χ (↑p ^ (n + 1)) * gaussSum χ ψ

Tactic:
← mul_assoc,

Goal state after:
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 * χ ↑p * gaussSum χ ψ = χ (↑p ^ (n + 1)) * gaussSum χ ψ
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) * (‖f x‖ * ‖fderiv ℝ f x‖) = ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖

Tactic:
← mul_assoc,

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) * ‖f x‖ * ‖fderiv ℝ f x‖ = ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖
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)
hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * ↑(Fintype.card (ZMod 8))
h : ↑8 ^ (Fintype.card F / 2) = χ ↑(Fintype.card F)
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))

Tactic:
convert_to (8 : F) ^ (Fintype.card F / 2) = _

Goal state after:
case e'_2
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)
hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * ↑(Fintype.card (ZMod 8))
h : ↑8 ^ (Fintype.card F / 2) = χ ↑(Fintype.card F)
⊢ 2 ^ (Fintype.card F / 2) = 8 ^ (Fintype.card F / 2)

case convert_2
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)
hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * ↑(Fintype.card (ZMod 8))
h : ↑8 ^ (Fintype.card F / 2) = χ ↑(Fintype.card F)
⊢ 8 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x : E
⊢ ↑(lidIsometry 𝕜 E).symm.symm.toLinearEquiv (One.one ⊗ₜ[𝕜] x) = x

Tactic:
exact one_smul _ _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x : E
⊢ ↑((commIsometry 𝕜 E 𝕜).trans (lidIsometry 𝕜 E)).symm.symm.toLinearEquiv (x ⊗ₜ[𝕜] One.one) = x

Tactic:
exact one_smul _ _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ r • x = { toFun := ⇑(adjoint counit), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x

Tactic:
dsimp
    simp_rw [← rTensor_tmul, ← adjoint_rTensor, ← comp_apply, ← adjoint_comp,
      rTensor_counit_comp_comul, ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry,
      ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm]
    simp

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

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ innerProductForm.flip = innerProductForm

Tactic:
apply linearMap_ext
  ext
  simp only [LinearMap.compAlternatingMap_apply, LinearMap.flip_apply,
    innerProductForm_ιMulti_ιMulti]
  rw [← Matrix.det_transpose]
  congr 1
  ext
  exact real_inner_comm _ _

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
inst✝ : FiniteDimensional 𝕜 E
ι : Type u_5
T : ι → E →ₗ[𝕜] E
hT : ∀ (i : ι), (T i).IsSymmetric
h : Pairwise (Commute on T)
x✝ : ι
⊢ ⨆ μ, maxGenEigenspace (T x✝) μ = ⊤

Tactic:
rw [← orthogonal_eq_bot_iff,
      congr(⨆ μ, $(maxGenEigenspace_eq_eigenspace (isFinitelySemisimple <| hT _) μ)),
      (hT _).orthogonalComplement_iSup_eigenspaces_eq_bot]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : Fin (Module.finrank 𝕜 E) → E := fun i ↦ ↑√(⋯.eigenvalues ⋯ i) • (⋯.eigenvectorBasis ⋯) i
x✝ : E
⊢ T x✝ =
    ∑ x, (↑√(⋯.eigenvalues ⋯ x) * (↑√(⋯.eigenvalues ⋯ x) * ⟪(⋯.eigenvectorBasis ⋯) x, x✝⟫)) • (⋯.eigenvectorBasis ⋯) x

Tactic:
← mul_assoc,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : Fin (Module.finrank 𝕜 E) → E := fun i ↦ ↑√(⋯.eigenvalues ⋯ i) • (⋯.eigenvectorBasis ⋯) i
x✝ : E
⊢ T x✝ =
    ∑ x, (↑√(⋯.eigenvalues ⋯ x) * ↑√(⋯.eigenvalues ⋯ x) * ⟪(⋯.eigenvectorBasis ⋯) x, x✝⟫) • (⋯.eigenvectorBasis ⋯) x
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p
v : (ι → ℝ) → F := u ∘ ⇑e.symm
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  ↑c * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (⇑e.symm) volume ≤
    ↑c * (↑(‖↑e.symm‖₊ ^ p) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂Measure.map (⇑e.symm) volume) ^ p)
⊢ ↑c * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (⇑e.symm) volume ≤
    ↑C * (↑c * ∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂Measure.map (⇑e.symm) volume) ^ p

Tactic:
← mul_assoc,

Goal state after:
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p
v : (ι → ℝ) → F := u ∘ ⇑e.symm
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  ↑c * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (⇑e.symm) volume ≤
    ↑c * ↑(‖↑e.symm‖₊ ^ p) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂Measure.map (⇑e.symm) volume) ^ p
⊢ ↑c * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (⇑e.symm) volume ≤
    ↑C * (↑c * ∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂Measure.map (⇑e.symm) volume) ^ p