mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case e'_2
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
x : ι → ℝ × ℝ
hx : x ∈ Set.univ.pi fun x ↦ polarCoord.target
⊢ ((∏ i, (x i).1) • f fun i ↦ ↑polarCoord.symm (x i)) =
    |(fderivPiPolarCoordSymm x).det| • f fun i ↦ ↑polarCoord.symm (x i)

Tactic:
simp_rw [det_fderivPiPolarCoordSymm, Finset.abs_prod, abs_fst_of_mem_pi_polarCoord_target hx]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
hs : 0 < s
⊢ 0 < Gamma s

Tactic:
Gamma_eq_integral hs

Goal state after:
s : ℝ
hs : 0 < s
⊢ 0 < ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ I₁ T =
    I₂ T + I * ((∫ (x : ℝ) in 0..c, cexp (-b * (↑T + ↑x * I) ^ 2)) - ∫ (x : ℝ) in 0..c, cexp (-b * (↑T - ↑x * I) ^ 2))

Tactic:
(fun a b => by rw [sq]; ring_nf : ∀ a b : ℂ, (a - b * I) ^ 2 = (-a + b * I) ^ 2)

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ I₁ T =
    I₂ T + I * ((∫ (x : ℝ) in 0..c, cexp (-b * (↑T + ↑x * I) ^ 2)) - ∫ (x : ℝ) in 0..c, cexp (-b * (-↑T + ↑x * I) ^ 2))
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
n✝ : ℕ
a b : α
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite α
ψ : AddChar α Circle
⊢ (fun ψ ↦ { toFun := fun a ↦ ⟨ψ a, ⋯⟩, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ })
      ((fun ψ ↦ toMonoidHomEquiv.symm (coeHom.comp ψ.toMonoidHom)) ψ) =
    ψ

Tactic:
ext : 1; simp

Goal state after:
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
n✝ : ℕ
a b : α
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite α
ψ : AddChar α ℂ
⊢ (fun ψ ↦ toMonoidHomEquiv.symm (coeHom.comp ψ.toMonoidHom))
      ((fun ψ ↦ { toFun := fun a ↦ ⟨ψ a, ⋯⟩, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }) ψ) =
    ψ

Tactic:
ext : 1; simp

Goal state after:
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n k : ℕ+
h : k.Coprime m
⊢ (k * n).gcd m = m.gcd n

Tactic:
symm

Goal state after:
m n k : ℕ+
h : k.Coprime m
⊢ m.gcd n = (k * n).gcd m
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n k : ℕ+
h : k.Coprime m
⊢ n.gcd m = (k * n).gcd m

Tactic:
symm

Goal state after:
m n k : ℕ+
h : k.Coprime m
⊢ (k * n).gcd m = n.gcd m
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
x : ℕ × ℕ
hx : x ∈ (n + 1).divisorsAntidiagonal
⊢ (μ x.1 • if x.2 = 0 then 0 else g x.2) = μ x.1 • g x.2

Tactic:
rw [if_neg (pos_of_mem_divisors (snd_mem_divisors_of_mem_antidiagonal hx)).ne']

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[cocompact ℝ] fun x ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (0 - r) r
⊢ (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x ↦ |x| ^ (-b)

Tactic:
zero_sub

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[cocompact ℝ] fun x ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
⊢ (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x ↦ |x| ^ (-b)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (X ^ n - C 1).Monic
⊢ X ^ n - 1 = (Multiset.map (fun ζ ↦ X - C ζ) (X ^ n - C 1).roots).prod

Tactic:
symm

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (X ^ n - C 1).Monic
⊢ (Multiset.map (fun ζ ↦ X - C ζ) (X ^ n - C 1).roots).prod = X ^ n - 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
hζ : IsPrimitiveRoot ζ k
hk : 1 < k
⊢ (∑ i ∈ range k, X ^ i).IsRoot ζ

Tactic:
by
  simp [geom_sum_eq_zero hζ hk]

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

Goal state before:
pp: case left
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h✝ h : IsPrimitiveRoot ζ k
⊢ Function.Injective
    ⇑(((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
        ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)

pp: case right
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h✝ h : IsPrimitiveRoot ζ k
⊢ Function.Surjective
    ⇑(((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
        ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)

Tactic:
· rw [injective_iff_map_eq_zero]
        intro i hi
        rw [Subtype.ext_iff] at hi
        have := (h.zpow_eq_one_iff_dvd _).mp hi
        rw [← (CharP.intCast_eq_zero_iff (ZMod k) k _).mpr this, eq_comm]
        exact ZMod.intCast_rightInverse i

Goal state after:
case right
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h✝ h : IsPrimitiveRoot ζ k
⊢ Function.Surjective
    ⇑(((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
        ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed
⊢ eval₂ (algebraMap ℤ K) μ ((expand ℤ p) (minpoly ℤ (μ ^ p))) = 0

Tactic:
coe_expand,

Goal state after:
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed
⊢ eval₂ (algebraMap ℤ K) μ (eval₂ C (X ^ p) (minpoly ℤ (μ ^ p))) = 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ cyclotomic 1 R = X - 1

Tactic:
symm

Goal state after:
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = cyclotomic 1 R
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ nthRoots n a = Multiset.map (fun x ↦ ζ ^ x * α) (Multiset.range n)

Tactic:
symm

Goal state after:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ Multiset.map (fun x ↦ ζ ^ x * α) (Multiset.range n) = nthRoots n a
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ #(primitiveRoots k R) = φ k

Tactic:
symm

Goal state after:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ φ k = #(primitiveRoots k R)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: 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 : Even n ∧ x + 1 < 0
⊢ 2 ≠ 1

Tactic:
decide

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

Goal state before:
pp: case e'_4.e'_5
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
this : ¬SameRay ℝ (↑q) (-ζ)
⊢ q = ‖q‖

Tactic:
symm

Goal state after:
case e'_4.e'_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := ⋯
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q) (-ζ)
⊢ ‖q‖ = q
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
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this : Algebra B C := (↑f).toAlgebra
⊢ IsCyclotomicExtension S A C

Tactic:
have : IsCyclotomicExtension {1} B C := singleton_one_of_algebraMap_bijective f.surjective

Goal state after:
S : Set ℕ
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this✝ : Algebra B C := (↑f).toAlgebra
this : IsCyclotomicExtension {1} B C
⊢ IsCyclotomicExtension S A C
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
n : ℕ
hn1 : n ∈ S
hn2 : n ≠ 0
⊢ ∃ r, IsPrimitiveRoot r n

Tactic:
by
    obtain ⟨r, hr1, hr2⟩ := h n hn1 hn2
    exact ⟨⟨r, subset_adjoin ⟨n, hn1, hn2, hr1⟩⟩, Subtype.val_injective hr1,
      fun l hl ↦ hr2 l congr($hl.1)⟩

Goal state after:
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
hx : x ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
⊢ ⟨x, ⋯⟩ ∈ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}

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

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

Goal state before:
pp: case pos
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)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s + 1 = 1
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
simp only [add_eq_right] at hks

Goal state after:
case pos
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)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : Algebra (ZMod p) K
inst✝ : Finite K
⊢ (Polynomial.map (algebraMap (ZMod p) K) (X ^ Nat.card K - X)).Splits

Tactic:
have : Fintype K := Fintype.ofFinite K

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : Algebra (ZMod p) K
inst✝ : Finite K
this : Fintype K
⊢ (Polynomial.map (algebraMap (ZMod p) K) (X ^ Nat.card K - X)).Splits
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this : Finite K
⊢ IsSplittingField (ZMod p) K (X ^ p ^ n - X)

Tactic:
have : Fintype K := Fintype.ofFinite K

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this✝ : Finite K
this : Fintype K
⊢ IsSplittingField (ZMod p) K (X ^ p ^ n - X)
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (x y : ZMod 4),
    (match x * y with
      | 0 => 0
      | 2 => 0
      | 1 => 1
      | 3 => -1) =
      (match x with
        | 0 => 0
        | 2 => 0
        | 1 => 1
        | 3 => -1) *
        match y with
        | 0 => 0
        | 2 => 0
        | 1 => 1
        | 3 => -1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (a : ZMod 4),
    ¬IsUnit a →
      (match a with
        | 0 => 0
        | 2 => 0
        | 1 => 1
        | 3 => -1) =
        0

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (a : ZMod 4), χ₄ a = 0 ∨ χ₄ a = 1 ∨ χ₄ a = -1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
⊢ ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (x y : ZMod 8),
    (match x * y with
      | 0 => 0
      | 2 => 0
      | 4 => 0
      | 6 => 0
      | 1 => 1
      | 7 => 1
      | 3 => -1
      | 5 => -1) =
      (match x with
        | 0 => 0
        | 2 => 0
        | 4 => 0
        | 6 => 0
        | 1 => 1
        | 7 => 1
        | 3 => -1
        | 5 => -1) *
        match y with
        | 0 => 0
        | 2 => 0
        | 4 => 0
        | 6 => 0
        | 1 => 1
        | 7 => 1
        | 3 => -1
        | 5 => -1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (a : ZMod 8),
    ¬IsUnit a →
      (match a with
        | 0 => 0
        | 2 => 0
        | 4 => 0
        | 6 => 0
        | 1 => 1
        | 7 => 1
        | 3 => -1
        | 5 => -1) =
        0

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (a : ZMod 8), χ₈ a = 0 ∨ χ₈ a = 1 ∨ χ₈ a = -1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (x y : ZMod 8),
    (match x * y with
      | 0 => 0
      | 2 => 0
      | 4 => 0
      | 6 => 0
      | 1 => 1
      | 3 => 1
      | 5 => -1
      | 7 => -1) =
      (match x with
        | 0 => 0
        | 2 => 0
        | 4 => 0
        | 6 => 0
        | 1 => 1
        | 3 => 1
        | 5 => -1
        | 7 => -1) *
        match y with
        | 0 => 0
        | 2 => 0
        | 4 => 0
        | 6 => 0
        | 1 => 1
        | 3 => 1
        | 5 => -1
        | 7 => -1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (a : ZMod 8),
    ¬IsUnit a →
      (match a with
        | 0 => 0
        | 2 => 0
        | 4 => 0
        | 6 => 0
        | 1 => 1
        | 3 => 1
        | 5 => -1
        | 7 => -1) =
        0

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (a : ZMod 8), χ₈' a = 0 ∨ χ₈' a = 1 ∨ χ₈' a = -1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (a : ZMod 8), χ₈' a = χ₄ a.cast * χ₈ a

Tactic:
decide

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ ∀ (a b : MulChar R R'), a * b = b * a

Tactic:
intro χ₁ χ₂
    ext a
    simp only [mul_comm, Pi.mul_apply, MulChar.coeToFun_mul]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : (χ ^ n) ↑a = χ ↑a ^ n
⊢ (χ ^ (n + 1)) ↑a = χ ↑a ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ, mul_apply, ih]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : IsUnit a
⊢ 1 a = 1

Tactic:
exact one_apply_coe h.unit

Goal state after:
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
inst✝² : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝¹ : NeZero n₁
inst✝ : NeZero n₂
ζ₁ : ↥C₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
⊢ IsCyclotomicExtension {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)

Tactic:
replace hζ₁ := hζ₁.map_of_injective (FaithfulSMul.algebraMap_injective C₁ B)

Goal state after:
A : Type u
B : Type v
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝¹ : NeZero n₁
inst✝ : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
hζ₁ : IsPrimitiveRoot ((algebraMap (↥C₁) B) ζ₁) n₁
⊢ IsCyclotomicExtension {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case refine_1
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
⊢ (4 * 2) • 1 = 0

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case refine_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
⊢ ¬4 • 1 = 0

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case refine_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
⊢ ¬ψ₈.char 1 ^ 4 = 1

Tactic:
· rw [← map_nsmul_eq_pow ψ₈.char, ψ₈.prim.zmod_char_eq_one_iff]
      decide

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : F →L[𝕜] E
⊢ (adjoint S ∘SL T ∘SL S).IsPositive

Tactic:
convert! hT.conj_adjoint (S†)
  rw [adjoint_adjoint]

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

Goal state before:
pp: 𝕜 : 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
S : F →ₗ.[𝕜] E
a : 𝕜
x : F
hx : Continuous ⇑((innerₛₗ 𝕜) x ∘ₗ T.toFun)
⊢ Continuous ⇑(((starRingEnd 𝕜) a • (innerₛₗ 𝕜) x) ∘ₗ T.toFun)

Tactic:
exact hx.const_smul (conj a)

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

Goal state before:
pp: 𝕜 : 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
hx : x ∈ T.graph.adjoint
hx' : x.1 = 0
⊢ x.2 = 0

Tactic:
simp only [mem_adjoint_iff, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left, hx',
    inner_zero_right, zero_sub, neg_eq_zero, forall_exists_index, forall_apply_eq_imp_iff] at hx

Goal state after:
𝕜 : 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
hx' : x.1 = 0
hx : ∀ a ∈ T.domain, ⟪a, x.2⟫ = 0
⊢ x.2 = 0