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

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

Tactic:
replace hunit := degree_eq_zero_of_isUnit hunit
    rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom (ZMod p)) _] at hunit
    · exact (minpoly.degree_pos (isIntegral h hpos)).ne' hunit
    simp only [Pmonic, eq_intCast, Monic.leadingCoeff, Int.cast_one, Ne, not_false_iff,
      one_ne_zero]

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

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

Tactic:
rcases hξ with ⟨i, hin, hi, H⟩

Goal state after:
case neg.refine_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
i : ℕ
hin : i < k
hi : i.Coprime k
H : ζ ^ i = ξ
⊢ ∃ a, (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ
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 S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
x y : S ≃ₐ[R] S
hxy' : ∃ m, ↑(x * y) ↑↑μ' = ↑↑μ' ^ m
hx' : ∃ m, ↑x ↑↑μ' = ↑↑μ' ^ m
hy' : ∃ m, ↑y ↑↑μ' = ↑↑μ' ^ m
hxy : (↑↑μ' ^ hx'.choose) ^ hy'.choose = ↑↑μ' ^ hxy'.choose
⊢ ↑hxy'.choose = ↑hx'.choose * ↑hy'.choose

Tactic:
← pow_mul

Goal state after:
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 S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
x y : S ≃ₐ[R] S
hxy' : ∃ m, ↑(x * y) ↑↑μ' = ↑↑μ' ^ m
hx' : ∃ m, ↑x ↑↑μ' = ↑↑μ' ^ m
hy' : ∃ m, ↑y ↑↑μ' = ↑↑μ' ^ m
hxy : ↑↑μ' ^ (hx'.choose * hy'.choose) = ↑↑μ' ^ hxy'.choose
⊢ ↑hxy'.choose = ↑hx'.choose * ↑hy'.choose
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 S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
⊢ ∀ (x y : S ≃ₐ[R] S), ↑⋯.choose = ↑⋯.choose * ↑⋯.choose

Tactic:
intro x y
        generalize_proofs hxy' hx' hy'
        have hxy := hxy'.choose_spec
        replace hxy : x (((μ' : Sˣ) : S) ^ hy'.choose) = ((μ' : Sˣ) : S) ^ hxy'.choose :=
          hy'.choose_spec ▸ hxy
        rw [map_pow] at hxy
        replace hxy : (((μ' : Sˣ) : S) ^ hx'.choose) ^ hy'.choose = ((μ' : Sˣ) : S) ^ hxy'.choose :=
          hx'.choose_spec ▸ hxy
        rw [← pow_mul] at hxy
        replace hxy : μ' ^ (hx'.choose * hy'.choose) = μ' ^ hxy'.choose :=
          rootsOfUnity.coe_injective (by simpa only [rootsOfUnity.coe_pow] using! hxy)
        convert ho ▸ (ZMod.natCast_eq_natCast_iff ..).mpr (pow_eq_pow_iff_modEq.mp hxy).symm
        exact (Nat.cast_mul ..).symm

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
hnm : cyclotomic n R = cyclotomic m R
hzero : n ≠ 0
⊢ n = m

Tactic:
have := NeZero.mk hzero
    rw [← map_cyclotomic_int _ R, ← map_cyclotomic_int _ R] at hnm
    replace hnm := map_injective (Int.castRingHom R) Int.cast_injective hnm
    replace hnm := congr_arg (map (Int.castRingHom ℂ)) hnm
    rw [map_cyclotomic_int, map_cyclotomic_int] at hnm
    have hprim := Complex.isPrimitiveRoot_exp _ hzero
    have hroot := isRoot_cyclotomic_iff (R := ℂ).2 hprim
    rw [hnm] at hroot
    have hmzero : NeZero m := ⟨fun h => by simp [h] at hroot⟩
    rw [isRoot_cyclotomic_iff (R := ℂ)] at hroot
    replace hprim := hprim.eq_orderOf
    rwa [← IsPrimitiveRoot.eq_orderOf hroot] at hprim

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : (∑ i ∈ range p, (X ^ p ^ n_n) ^ i) * ∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R = X ^ p ^ (n_n + 1) - 1
⊢ (X ^ p ^ (n_n + 1)) ^ p = X ^ p ^ (n_n + 1 + 1)

Tactic:
← pow_mul

Goal state after:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : (∑ i ∈ range p, (X ^ p ^ n_n) ^ i) * ∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R = X ^ p ^ (n_n + 1) - 1
⊢ X ^ (p ^ (n_n + 1) * p) = X ^ p ^ (n_n + 1 + 1)
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case mk
p n : ℕ
inst✝¹² : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C✝ : Type w
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsCyclotomicExtension {n} A B
inst✝⁷ : Field K
inst✝⁶ : CommRing L
inst✝⁵ : IsDomain L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst✝² : CommRing C
inst✝¹ : IsDomain C
inst✝ : Algebra K C
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
hn : NeZero ↑n
val✝ : C
property✝ : (aeval val✝) (minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen) = 0
⊢ eval (↑⟨val✝, property✝⟩) (cyclotomic n C) = 0

Tactic:
← map_cyclotomic _ (algebraMap K C),

Goal state after:
case mk
p n : ℕ
inst✝¹² : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C✝ : Type w
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsCyclotomicExtension {n} A B
inst✝⁷ : Field K
inst✝⁶ : CommRing L
inst✝⁵ : IsDomain L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst✝² : CommRing C
inst✝¹ : IsDomain C
inst✝ : Algebra K C
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
hn : NeZero ↑n
val✝ : C
property✝ : (aeval val✝) (minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen) = 0
⊢ eval (↑⟨val✝, property✝⟩) (Polynomial.map (algebraMap K C) (cyclotomic n K)) = 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ a.succ * m
⊢ (cyclotomic m R ^ (p ^ a.succ - p ^ (a.succ - 1))) ^ p = cyclotomic m R ^ (p * p ^ (a + 1) - p ^ (a + 2 - 1))

pp: R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ a.succ * m
⊢ ¬p ∣ m

Tactic:
← pow_mul

Goal state after:
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ a.succ * m
⊢ cyclotomic m R ^ ((p ^ a.succ - p ^ (a.succ - 1)) * p) = cyclotomic m R ^ (p * p ^ (a + 1) - p ^ (a + 2 - 1))

R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ a.succ * m
⊢ ¬p ∣ m
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

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

Tactic:
rw [pow_zero, one_mul, isRoot_cyclotomic_iff]

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

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

Tactic:
ht,

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

Goal state before:
pp: 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 (S ∪ {n}) A B
hn : ¬n = 0
this✝¹ : IsCyclotomicExtension S A ↥(adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
this✝ : Module.Finite A ↥(adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
x✝ : IsCyclotomicExtension {n} (↥(adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B := union_right S {n} A B
this : NeZero n
⊢ Module.Finite (↥(adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})) B

Tactic:
exact finite_of_singleton n _ _

Goal state after:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case succ.refine_2
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ (aeval 0) (X ^ (n✝ + 1) ^ n - X) = 0

Tactic:
rw [← coeff_zero_eq_aeval_zero']
    simp only [coeff_X_pow, coeff_X_zero, sub_zero, _root_.map_eq_zero, ite_eq_right_iff,
      one_ne_zero, coeff_sub]
    intro hn
    exact Nat.not_lt_zero 1 (eq_zero_of_pow_eq_zero hn.symm ▸ hp)

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

Goal state before:
pp: case refine_2
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
i : ℕ
left✝ : i < n
hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1
⊢ cyclotomic n B ≠ 0 ∧ eval ζ (cyclotomic n B) = 0

Tactic:
← IsRoot

Goal state after:
case refine_2
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
i : ℕ
left✝ : i < n
hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1
⊢ cyclotomic n B ≠ 0 ∧ (cyclotomic n B).IsRoot ζ
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
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : cyclotomic n B ≠ 0 ∧ eval x (cyclotomic n B) = 0
⊢ (cyclotomic n B).IsRoot x

Tactic:
← IsRoot

Goal state after:
case refine_1
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : cyclotomic n B ≠ 0 ∧ (cyclotomic n B).IsRoot x
⊢ (cyclotomic n B).IsRoot x
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: m : ℕ
n : ℤ
h : IsUnit ↑n
⊢ IsUnit (↑n)⁻¹

Tactic:
isUnit_iff_exists

Goal state after:
m : ℕ
n : ℤ
h : IsUnit ↑n
⊢ ∃ b, (↑n)⁻¹ * b = 1 ∧ b * (↑n)⁻¹ = 1
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
K' : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field K'
inst✝³ : Fintype K
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
⊢ K ≃ₐ[ZMod p] K'

Tactic:
have : CharP K p := by rw [← Algebra.charP_iff (ZMod p) K p]; exact ZMod.charP p

Goal state after:
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
K' : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field K'
inst✝³ : Fintype K
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this : CharP K p
⊢ K ≃ₐ[ZMod p] K'
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: 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
⊢ ∃ x_1,
    x * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x_1.2 =
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x_1.1

Tactic:
have : NeZero (n : K) := NeZero.nat_of_injective (IsFractionRing.injective A K)

Goal state after:
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
⊢ ∃ x_1,
    x * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x_1.2 =
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x_1.1
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
z : ℕ
hz₁ : ↑z = ↑x
hz₂ : ↑z = 1
hz₀ : z.gcd (n * m) = 1
this✝ : ((changeLevel ⋯) χ) ↑z = χ ↑z
this : ((changeLevel ⋯) ψ) ↑(ZMod.unitOfCoprime z hz₀) = ψ (↑(ZMod.unitOfCoprime z hz₀)).cast
⊢ ((changeLevel ⋯) ψ) ↑z = 1

Tactic:
simp only [ZMod.coe_unitOfCoprime, dvd_mul_left, ZMod.cast_natCast] at this

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
z : ℕ
hz₁ : ↑z = ↑x
hz₂ : ↑z = 1
hz₀ : z.gcd (n * m) = 1
this✝ : ((changeLevel ⋯) χ) ↑z = χ ↑z
this : ((changeLevel ⋯) ψ) ↑z = ψ ↑z
⊢ ((changeLevel ⋯) ψ) ↑z = 1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case refine_1.inr.inr
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
H : χ ↑x = -1
⊢ χ ↑x ^ 2 = 1

Tactic:
· simp only [H, even_two, Even.neg_pow, one_pow]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
⊢ χ ^ (orderOf χ - 1 + 1) = 1

Tactic:
Nat.sub_one_add_one_eq_of_pos χ.orderOf_pos,

Goal state after:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
⊢ χ ^ orderOf χ = 1
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:

Tactic:
(fun x : E ↦ ‖x‖ ^ p - ‖(0 : E)‖ ^ p - 0)
        = (fun x : E ↦ ‖x‖ ^ p) := by simp [zero_lt_one.trans hp |>.ne']
      _ = (fun x : E ↦ ‖x‖ * ‖x‖ ^ (p - 1)) := by
          ext x
          rw [← rpow_one_add' (norm_nonneg x) (by positivity)]
          ring_nf
      _ =o[𝓝 0] (fun x : E ↦ ‖x‖ * 1) := by
        refine (isBigO_refl _ _).mul_isLittleO <| (isLittleO_const_iff <| by simp).mpr ?_
        convert! continuousAt_id.norm.rpow_const (.inr h2p.le) |>.tendsto
        simp [h2p.ne']
      _ =O[𝓝 0] (fun (x : E) ↦ x - 0) := by
        simp_rw [mul_one, isBigO_norm_left (f' := fun x ↦ x), sub_zero, isBigO_refl]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫‖
x : H
⊢ ‖x‖ * ↑c ≤ ‖f x‖

Tactic:
simp_rw [sq, mul_assoc] at h

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * ↑c) ≤ ‖⟪f x, x⟫‖
⊢ ‖x‖ * ↑c ≤ ‖f x‖
Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
𝕜 : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → α
g : α → E
n : ℕ
x y : α
⊢ dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) = dist (birkhoffSum f g n x) (birkhoffSum f g n y) / ↑n

Tactic:
by
  simp [birkhoffAverage, dist_smul₀, div_eq_inv_mul]

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case e'_3
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p' : ℝ≥0
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
n' : ℝ≥0 := (↑n).conjExponent
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hp : 1 ≤ 1
hp' : (↑p')⁻¹ = ↑1⁻¹ - (↑n)⁻¹
h2p : ↑1 < ↑n
hnp : 0 < ↑n - ↑1
⊢ ↑p' = ↑n'

pp: case e'_4.e'_5
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p' : ℝ≥0
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
n' : ℝ≥0 := (↑n).conjExponent
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hp : 1 ≤ 1
hp' : (↑p')⁻¹ = ↑1⁻¹ - (↑n)⁻¹
h2p : ↑1 < ↑n
hnp : 0 < ↑n - ↑1
⊢ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑1) = ↑(eLpNormLESNormFDerivOneConst μ ↑n')

Tactic:
· suffices (p' : ℝ) = n' by simpa using this
      rw [← inv_inj, hp']
      simp [field, n', NNReal.conjExponent, *]

Goal state after:
case e'_4.e'_5
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p' : ℝ≥0
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
n' : ℝ≥0 := (↑n).conjExponent
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hp : 1 ≤ 1
hp' : (↑p')⁻¹ = ↑1⁻¹ - (↑n)⁻¹
h2p : ↑1 < ↑n
hnp : 0 < ↑n - ↑1
⊢ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑1) = ↑(eLpNormLESNormFDerivOneConst μ ↑n')
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
i : ℕ
⊢ 0 ≤ if h : ∃ a, Fin.valEmbedding a = i then √(⋯.eigenvalues ⋯ h.choose) else 0

Tactic:
split_ifs <;> positivity

Goal state after:
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
n : ℕ
⊢ 0 < T.singularValues n ↔ n < finrank 𝕜 ↥T.range

Tactic:
by
  rw [singularValues_pos_iff_ne_zero, ← Finsupp.mem_support_iff, support_singularValues,
    Finset.mem_range]

Goal state after:
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
f : E →L[𝕜] F
g : G →L[𝕜] H
⊢ ‖ContinuousLinearMap.rTensor H f ∘SL ContinuousLinearMap.lTensor E g‖ ≤ ‖f‖ * ‖g‖

Tactic:
ContinuousLinearMap.opNorm_comp_le,

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
f : E →L[𝕜] F
g : G →L[𝕜] H
⊢ ‖ContinuousLinearMap.rTensor H f‖ * ‖ContinuousLinearMap.lTensor E g‖ ≤ ‖f‖ * ‖g‖
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝¹ : EMetricSpace X
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : ⨆ i, dimH (s i) < ↑d
this : ∀ (i : ι), μH[↑d] (s i) = 0
⊢ μH[↑d] (⋃ i, s i) ≠ ∞

Tactic:
measure_iUnion_null this

Goal state after:
X : Type u_2
inst✝¹ : EMetricSpace X
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : ⨆ i, dimH (s i) < ↑d
this : ∀ (i : ι), μH[↑d] (s i) = 0
⊢ 0 ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ∞
c : ℝ≥0
⊢ c ≠ 0 → μH[d₂] s ≤ ↑c * μH[d₁] s

Tactic:
hc

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ∞
c : ℝ≥0
hc : c ≠ 0
⊢ μH[d₂] s ≤ ↑c * μH[d₁] s
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
p : Submodule 𝕜 V
f : U →ₗ[𝕜] V
h : ∀ (c : U), f c ∈ p
⊢ (codRestrict p f h).normDet = f.normDet

Tactic:
by
  have : f = p.subtype ∘ₗ f.codRestrict p h := rfl
  conv_rhs => rw [this]
  rw [normDet_comp]
  have : (p.subtype.domRestrict (codRestrict p f h).range).normDet = 1 :=
    (p.subtypeₗᵢ.comp (codRestrict p f h).range.subtypeₗᵢ).normDet_eq_one
  simp [this]

Goal state after: