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

Goal state before:
pp: case e'_4
q : ℚ
h : Odd q.num
⊢ 2 * q.den = (q / 2).den

Tactic:
nth_rw 2 [← q.num_div_den]

Goal state after:
case e'_4
q : ℚ
h : Odd q.num
⊢ 2 * q.den = (↑q.num / ↑q.den / 2).den
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 - C 1).roots.card = n

Tactic:
← nthRoots

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
⊢ (nthRoots n 1).card = n
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case mp
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * ↑π * I / ↑n) ^ i = ↑x
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

Tactic:
← H,

Goal state after:
case mp
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * ↑π * I / ↑n) ^ i = ↑x
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (2 * ↑π * I / ↑n) ^ i
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case mpr
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
i : ℕ
left✝ : i < n
H : cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x
⊢ ↑x ^ n = 1

Tactic:
← H,

Goal state after:
case mpr
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
i : ℕ
left✝ : i < n
H : cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) ^ n = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case h
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)

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

Goal state after:
case h.inl
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
ihk : ∀ m < 0, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
h : IsPrimitiveRoot ζ 0
⊢ cyclotomic' 0 K ∈ lifts (Int.castRingHom K)

case h.inr
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: 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
⊢ Additive.ofMul ⟨(fun x ↦ ζ ^ x) 0, ⋯⟩ = 0

Tactic:
simp only [zpow_zero]; rfl

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

Goal state before:
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:
rintro ⟨ξ, i, rfl⟩

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
i : ℤ
⊢ ∃ a,
    (((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
          ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
        a =
      ⟨(fun x ↦ ζ ^ x) i, ⋯⟩
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case neg
n : ℕ
hzero : ¬n = 0
⊢ map (Int.castRingHom ℂ) ⋯.choose = cyclotomic' n ℂ ∧ ⋯.choose.degree = (cyclotomic' n ℂ).degree ∧ ⋯.choose.Monic

Tactic:
exact (int_coeff_of_cyclotomic' (Complex.isPrimitiveRoot_exp n hzero)).choose_spec

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (cyclotomic n ℤ).degree = ↑n.totient

pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (Int.castRingHom R) (cyclotomic n ℤ).leadingCoeff ≠ 0

Tactic:
· rcases n with - | k
    · simp only [cyclotomic, degree_one, dif_pos, Nat.totient_zero, CharP.cast_eq_zero]
    rw [← degree_cyclotomic' (Complex.isPrimitiveRoot_exp k.succ (Nat.succ_ne_zero k))]
    exact (int_cyclotomic_spec k.succ).2.1

Goal state after:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (Int.castRingHom R) (cyclotomic n ℤ).leadingCoeff ≠ 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
hpos : 0 < n
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ 0 < (cyclotomic n R).degree

Tactic:
degree_cyclotomic n R,

Goal state after:
n : ℕ
R : Type u_1
hpos : 0 < n
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ 0 < ↑n.totient
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case refine_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : (p * a).Coprime n✝
hprime : Nat.Prime p
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))

Tactic:
have hdiv := (Nat.Prime.coprime_iff_not_dvd hprime).1 (Nat.Coprime.coprime_mul_right hcop)

Goal state after:
case refine_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
h : IsPrimitiveRoot μ n✝
hcop : (p * a).Coprime n✝
hprime : Nat.Prime p
hdiv : ¬p ∣ n✝
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))
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
P : ℤ[X] := minpoly ℤ μ
P_K : K[X] := map (Int.castRingHom K) P
⊢ n.totient ≤ (minpoly ℤ μ).natDegree

Tactic:
calc
    n.totient = (primitiveRoots n K).card := h.card_primitiveRoots.symm
    _ ≤ P_K.roots.toFinset.card := Finset.card_le_card (is_roots_of_minpoly h)
    _ ≤ Multiset.card P_K.roots := Multiset.toFinset_card_le _
    _ ≤ P_K.natDegree := card_roots' _
    _ ≤ P.natDegree := natDegree_map_le

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : (cyclotomic i R).IsRoot ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
⊢ 1 = 1 + eval ζ (∏ i ∈ n.divisors, cyclotomic i R)

Tactic:
convert! (add_zero (M := R) _).symm

Goal state after:
case e'_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : (cyclotomic i R).IsRoot ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
⊢ eval ζ (∏ i ∈ n.divisors, cyclotomic i R) = 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
hcongr : ∀ j ∈ n.properDivisors.erase 1, (cyclotomic j R).coeff 0 = 1
⊢ ∏ x ∈ n.properDivisors.erase 1, 1 = 1

Tactic:
simp only [Finset.prod_const_one]

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

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

Tactic:
rw [norm_eq_neg_one_pow (K := K) hζ, IsCyclotomicExtension.finrank _ hirr]

Goal state after:
case pos
K : Type u
L : Type v
inst✝⁵ : CommRing L
ζ : L
inst✝⁴ : Field K
inst✝³ : Algebra K L
inst✝² : IsDomain L
inst✝¹ : NeZero 2
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
hirr : Irreducible (cyclotomic 2 K)
⊢ (-1) ^ φ 2 = -1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
s : ℕ
hs : s ∈ S
⊢ s ≠ 0 → ∃ r, IsPrimitiveRoot r s

pp: case refine_2
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
⊢ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} = ⊤

Tactic:
· exact H.exists_isPrimitiveRoot (subset_union_left hs)

Goal state after:
case refine_2
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
⊢ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} = ⊤
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
ζ : B
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
x : B
hx : map (algebraMap A B) (cyclotomic n A) ≠ 0 ∧ (aeval x) (cyclotomic n A) = 0
⊢ eval x (cyclotomic n B) = 0

Tactic:
← map_cyclotomic n (algebraMap A B),

Goal state after:
case refine_1
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
ζ : B
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
x : B
hx : map (algebraMap A B) (cyclotomic n A) ≠ 0 ∧ (aeval x) (cyclotomic n A) = 0
⊢ eval x (map (algebraMap A B) (cyclotomic n A)) = 0
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
b : Module.Basis (↥(IsNoetherian.finsetBasisIndex (ZMod p) (GaloisField p n))) (ZMod p) (GaloisField p n) :=
  IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
this : Fintype (GaloisField p n)
⊢ p ^ Module.finrank (ZMod p) (GaloisField p n) = p ^ n

Tactic:
finrank p h

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
b : Module.Basis (↥(IsNoetherian.finsetBasisIndex (ZMod p) (GaloisField p n))) (ZMod p) (GaloisField p n) :=
  IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
this : Fintype (GaloisField p n)
⊢ p ^ n = p ^ n
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
hψ : ψ.IsPrimitive
a : ZMod n
h : ψ a = 1
⊢ ¬ψ.mulShift a ≠ 1

Tactic:
rw [zmod_char_ne_one_iff n (mulShift ψ a), mulShift_apply, mul_one, h, Classical.not_not]

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

Goal state before:
pp: case inr
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hq : ringChar F' = 0
⊢ ¬ringChar F' ∣ p

Tactic:
rw [hq]
      exact fun hf => Nat.Prime.ne_zero hp.1 (zero_dvd_iff.mp hf)

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

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
this : DecidableEq L := Classical.decEq L
⊢ adjoin K ((cyclotomic n K).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
obtain ⟨ζ : L, hζ⟩ :=
        IsCyclotomicExtension.exists_isPrimitiveRoot K L (mem_singleton n) (NeZero.ne _)

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
this : DecidableEq L := Classical.decEq L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ adjoin K ((cyclotomic n K).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R' : Type u_2
inst✝² : CommMonoidWithZero R'
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
χ : MulChar R R'
⊢ χ ↑(ringChar R) = 0

Tactic:
by rw [ringChar.Nat.cast_ringChar, χ.map_zero]

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

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

Tactic:
by
  by_cases ha : IsUnit a
  · 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]
  · revert ha
    nontriviality R
    intro ha
    -- `nontriviality R` by itself doesn't do it
    rw [map_nonunit _ ha, Ring.inverse_non_unit a ha, MulChar.map_zero χ]

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'
χ₁ χ₂ : MulChar R R'
a : Rˣ
⊢ (equivToUnitHom (χ₁ * χ₂)) a = (equivToUnitHom χ₁) a * (equivToUnitHom χ₂) a

Tactic:
apply_fun ((↑) : R'ˣ → R') using Units.val_injective
  push_cast
  simp_rw [coe_equivToUnitHom, coeToFun_mul, Pi.mul_apply]

Goal state after:
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
⊢ χ ↑u * gaussSum χ e = gaussSum χ e

Tactic:
suffices e.mulShift u = e by conv_lhs => rw [← this, gaussSum_mulShift]
  rw [(by ring : u.val = (u - 1) + 1), ← mulShift_mul, mulShift_one, mul_eq_right]
  rsuffices ⟨a, ha⟩ : (d : ℤ) ∣ (u.val.val - 1 : ℤ)
  · have : u.val - 1 = ↑(u.val.val - 1 : ℤ) := by simp only [ZMod.natCast_val, Int.cast_sub,
      ZMod.intCast_cast, ZMod.cast_id', id_eq, Int.cast_one]
    rw [this, ha]
    ext1 y
    simpa only [Int.cast_mul, Int.cast_natCast, mulShift_apply, mul_assoc, one_apply]
      using DFunLike.ext_iff.mp he (a * y)
  rw [← Units.val_inj, Units.val_one, ZMod.unitsMap_def, Units.coe_map] at hu
  have : ZMod.castHom hd (ZMod d) u.val = ((u.val.val : ℤ) : ZMod d) := by simp
  rwa [MonoidHom.coe_coe, this, ← Int.cast_one, eq_comm,
    ZMod.intCast_eq_intCast_iff_dvd_sub] at hu

Goal state after:
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
a : α
⊢ ∅ ⋖ {a}

Tactic:
exact insert_empty_eq (β := Finset α) a ▸ covBy_insert <| notMem_empty a

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 + ↑(χ₈ 6) * τ ^ ↑6 +
      ↑(χ₈ 7) * τ ^ ↑7 =
    2 * (τ - τ ^ 3)

Tactic:
show χ₈ 6 = 0 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 +
      ↑(χ₈ 7) * τ ^ ↑7 =
    2 * (τ - τ ^ 3)
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
⊢ T ≠ 0 ↔ ∃ x, 0 < ⟪T x, x⟫

Tactic:
simp [← hT.isSymmetric.inner_map_self_eq_zero, lt_iff_le_and_ne', hT.inner_nonneg_left]

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
⊢ (innerProductForm ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm s))))
      ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm t))) =
    0

Tactic:
· rw [innerProductForm_ιMulti_ιMulti]
    obtain ⟨x, hxt, hxs⟩ := (Set.powersetCard.exists_mem_notMem_iff_ne t s).mp (.symm h)
    simp only [Set.mem_range, not_exists,
      ← Set.powersetCard.mem_range_ofFinEmbEquiv_symm_iff_mem] at hxs hxt
    obtain ⟨i, rfl⟩ := hxt
    exact det_eq_zero_of_row_eq_zero i (fun j ↦ hv.inner_eq_zero (hxs j))

Goal state after:
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
y : ι → ℝ
⊢ fderiv ℝ v y = fderiv ℝ u (e.symm y) ∘SL fderiv ℝ (⇑e.symm) y

Tactic:
apply fderiv_comp _ (hu.differentiable one_ne_zero _)

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 := ⋯
ι : Type := ⋯
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ⋯
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := ⋯
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 := ⋯
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
y : ι → ℝ
⊢ DifferentiableAt ℝ (⇑e.symm) y
Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic

Goal state before:
pp: case hg_ker.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ (↑f - 1).rangeᗮ
⊢ RCLike.re ⟪↑f x, ↑1 x⟫ = ‖↑1 x‖ ^ 2

Tactic:
have : ∀ y, ⟪f y, x⟫ = ⟪y, x⟫ := by
        simpa [Submodule.mem_orthogonal, inner_sub_left, sub_eq_zero] using hx

Goal state after:
case hg_ker.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ (↑f - 1).rangeᗮ
this : ∀ (y : E), ⟪f y, x⟫ = ⟪y, x⟫
⊢ RCLike.re ⟪↑f x, ↑1 x⟫ = ‖↑1 x‖ ^ 2
Module: Mathlib.Analysis.InnerProductSpace.SingularValues

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
⊢ T.singularValues = 0 ↔ T = 0

Tactic:
constructor <;> intro h
  · rw [← range_eq_bot, ← Submodule.finrank_eq_zero, ← Nat.le_zero,
      ← singularValues_eq_zero_iff_le_finrank_range, h, Finsupp.zero_apply]
  · exact h ▸ singularValues_zero

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
n : ℕ
⊢ μ (s ∩ t ∪ s \ t) = μ s

Tactic:
inter_union_sdiff

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
n : ℕ
⊢ μ s = μ s
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹⁴ : RCLike 𝕜
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace 𝕜 E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : InnerProductSpace 𝕜 F
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : InnerProductSpace 𝕜 G
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : InnerProductSpace 𝕜 H
inst✝⁵ : CompleteSpace E
inst✝⁴ : CompleteSpace G
inst✝³ : CompleteSpace (E ⊗[𝕜] G)
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace (F ⊗[𝕜] H)
f : E →L[𝕜] F
g : G →L[𝕜] H
⊢ ContinuousLinearMap.adjoint (mapL f g) = mapL (ContinuousLinearMap.adjoint f) (ContinuousLinearMap.adjoint g)

Tactic:
apply ContinuousLinearMap.coe_inj.mp <| ext' ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹⁴ : RCLike 𝕜
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace 𝕜 E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : InnerProductSpace 𝕜 F
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : InnerProductSpace 𝕜 G
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : InnerProductSpace 𝕜 H
inst✝⁵ : CompleteSpace E
inst✝⁴ : CompleteSpace G
inst✝³ : CompleteSpace (E ⊗[𝕜] G)
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace (F ⊗[𝕜] H)
f : E →L[𝕜] F
g : G →L[𝕜] H
⊢ ∀ (x : F) (y : H),
    ↑(ContinuousLinearMap.adjoint (mapL f g)) (x ⊗ₜ[𝕜] y) =
      ↑(mapL (ContinuousLinearMap.adjoint f) (ContinuousLinearMap.adjoint g)) (x ⊗ₜ[𝕜] y)
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.areaForm x) y = o.volumeForm ![x, y]

Tactic:
simp [areaForm]

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

Goal state before:
pp: case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ ((o.kahler x) a * (o.kahler a) y).im = (↑(‖a‖ ^ 2) * (o.kahler x) y).im

Tactic:
simp only [o.kahler_apply_apply, Complex.add_im, Complex.add_re, Complex.I_im, Complex.I_re,
        Complex.mul_im, Complex.mul_re, Complex.ofReal_im, Complex.ofReal_re, Complex.real_smul]
      rw [real_inner_comm a x, o.areaForm_swap x a]
      linear_combination o.inner_mul_areaForm_sub a x y

Goal state after: