mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case left
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
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
⊢ cyclotomic' k K * B = X ^ k - 1

Tactic:
← prod_cyclotomic'_eq_X_pow_sub_one hpos h,

Goal state after:
case left
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
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
⊢ cyclotomic' k K * B = ∏ i ∈ k.divisors, cyclotomic' i K
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ∈ rootsOfUnity n ℂ
⊢ ↑(ζ ^ n) = 1

Tactic:
_root_.mem_rootsOfUnity

Goal state after:
ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ^ n = 1
⊢ ↑(ζ ^ n) = 1
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 : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
⊢ map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) ((expand ℤ p) Q)

Tactic:
← ZMod.expand_card,

Goal state after:
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
Q : ℤ[X] := minpoly ℤ (μ ^ p)
⊢ (expand (ZMod p) p) (map (Int.castRingHom (ZMod p)) Q) = map (Int.castRingHom (ZMod p)) ((expand ℤ p) Q)
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case neg
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
⊢ IsIntegral R ((B.basis.repr ((algebraMap S A) ((algebraMap R S) (Q.coeff ↑⟨j, hj⟩)) * B.basis ⟨j, hj⟩)) i)

Tactic:
←
    Algebra.smul_def,

Goal state after:
case neg
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
⊢ IsIntegral R ((B.basis.repr ((algebraMap R S) (Q.coeff ↑⟨j, hj⟩) • B.basis ⟨j, hj⟩)) i)
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case refine_1
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝ : Nontrivial A
⊢ (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) → ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ 0)) i)

Tactic:
intro _

Goal state after:
case refine_1
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝¹ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
⊢ ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ 0)) i)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_1.refine_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ (map (algebraMap ℚ ℂ) (minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)))).IsRoot
    (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n) ^ p)

Tactic:
←
        cyclotomic_eq_minpoly_rat hprim hnpos,

Goal state after:
case inr.refine_1.refine_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ (map (algebraMap ℚ ℂ) (cyclotomic n ℚ)).IsRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n) ^ p)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p

Tactic:
← ZMod.expand_card,

Goal state after:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) = (expand (ZMod p) p) (cyclotomic n (ZMod p))
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: 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)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
⊢ IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))

Tactic:
rw [sub_add_cancel]

Goal state after:
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)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
⊢ IsPrimitiveRoot (ζ ^ p ^ s) (p ^ (k + 1 - s))
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ (unitsMap hm).comp (unitsMap hd) = unitsMap ⋯

Tactic:
simp only [unitsMap_def]

Goal state after:
n m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ (Units.map ↑(castHom hm (ZMod n))).comp (Units.map ↑(castHom hd (ZMod m))) = Units.map ↑(castHom ⋯ (ZMod n))
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case h
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
⊢ Nat.Prime p → p ∣ x + ps.prod id * n → ¬p ∣ m

Tactic:
pp

Goal state after:
case h
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
⊢ p ∣ x + ps.prod id * n → ¬p ∣ m
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ (X ^ n - 1).Splits

Tactic:
obtain ⟨z, hz⟩ := ((isCyclotomicExtension_iff _ _ _).1 H).1 hS (NeZero.ne _)

Goal state after:
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
z : L
hz : IsPrimitiveRoot z n
⊢ (X ^ n - 1).Splits
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n : ℤ
m : ℕ
⊢ IsUnit ↑n ↔ IsCoprime (↑m) n

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ⟨unitOfIsCoprime n (isCoprime_comm.mp h), by simp⟩⟩
  obtain rfl | hm := eq_or_ne m 0
  · rw [Nat.cast_zero, isCoprime_zero_left]
    exact_mod_cast h
  · have : NeZero m := ⟨hm⟩
    obtain ⟨u, hu⟩ := h
    have h_coprime := val_coe_unit_coprime u
    rw [hu, Nat.coprime_iff_gcd_eq_one, ← Int.gcd_natCast_natCast,
      val_intCast, Int.gcd_emod] at h_coprime
    rwa [isCoprime_comm, Int.isCoprime_iff_gcd_eq_one]

Goal state after:
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'
this✝ : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
⊢ K ≃ₐ[ZMod p] K'

Tactic:
choose n' a' hK' using FiniteField.card K' 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
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ ↑n'
⊢ 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✝¹ : IsDomain A
inst✝ : IsFractionRing A K
⊢ Function.Injective ⇑(algebraMap A (CyclotomicField n K))

Tactic:
IsScalarTower.algebraMap_eq A K (CyclotomicField n 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✝¹ : IsDomain A
inst✝ : IsFractionRing A K
⊢ Function.Injective ⇑((algebraMap K (CyclotomicField n K)).comp (algebraMap A K))
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ χ₄ ↑n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1

Tactic:
have help : ∀ m : ℤ, 0 ≤ m → m < 4 → χ₄ m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1 := by
    decide
  rw [← Int.emod_emod_of_dvd n (by lia : (2 : ℤ) ∣ 4), ← ZMod.intCast_mod n 4]
  exact help (n % 4) (Int.emod_nonneg n (by lia)) (Int.emod_lt_abs n (by lia))

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
⊢ Function.Injective ⇑(changeLevel hm)

Tactic:
intro _

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
a₁✝ : DirichletCharacter R n
⊢ ∀ ⦃a₂ : DirichletCharacter R n⦄, (changeLevel hm) a₁✝ = (changeLevel hm) a₂ → a₁✝ = a₂
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
f : R' →+* R''
hf : Function.Injective ⇑f
χ : MulChar R R'
⊢ χ.ringHomComp f = 1 ↔ χ = 1

Tactic:
conv_lhs => rw [← (show (1 : MulChar R R').ringHomComp f = 1 by simp)]

Goal state after:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
f : R' →+* R''
hf : Function.Injective ⇑f
χ : MulChar R R'
⊢ χ.ringHomComp f = ringHomComp 1 f ↔ χ = 1
Module: Mathlib.NumberTheory.MulChar.Basic

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

Tactic:
rw [h₀, Ring.inverse_zero]

Goal state after:
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:
have : (-1 : R') = (-1 : R'ˣ) := by norm_cast; simp

Goal state after:
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
this : -1 = ↑(-1)
⊢ (χ ↑x)⁻¹ʳ = χ ↑x
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
this✝ : NeZero d
hd : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel hd) χ₀
this : (changeLevel ⋯) χ₀ = (changeLevel ⋯) χ.primitiveCharacter
w✝ : d.gcd χ.conductor ∣ d
χ₁ : DirichletCharacter R (d.gcd χ.conductor)
hχ₁ : χ₀ = (changeLevel w✝) χ₁
⊢ χ = (changeLevel ⋯) χ₁

Tactic:
rw [changeLevel_trans _ (d.gcd_dvd_left χ.conductor), ← hχ₁, hχ₀]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
⊢ ∑ a, χ a = 0

Tactic:
by
  rcases ne_one_iff.mp hχ with ⟨b, hb⟩
  refine eq_zero_of_mul_eq_self_left hb ?_
  simpa only [Finset.mul_sum, ← map_mul] using b.mulLeft_bijective.sum_comp _

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
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
⊢ (ZMod.unitsMap hd).ker ≤ (MulChar.toUnitHom χ).ker

Tactic:
intro _

Goal state after:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
h_ne : gaussSum χ e ≠ 0
x✝ : (ZMod N)ˣ
⊢ x✝ ∈ (ZMod.unitsMap hd).ker → x✝ ∈ (MulChar.toUnitHom χ).ker
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, χ a * ψ a) * ∑ a, φ a * ψ a = ∑ t, ∑ x, χ x * φ (t - x) * ψ t

Tactic:
sum_mul_sum

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
⊢ ∑ i, ∑ j, χ i * ψ i * (φ j * ψ j) = ∑ t, ∑ x, χ x * φ (t - x) * ψ t
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)
⊢ χ ∈ subgroupOfPrimitiveMapToOne R n p ↔ χ.primitiveCharacter ↑p = 1

Tactic:
by
  have : NeZero (n / p ^ n.factorization p) := ⟨(Nat.ordCompl_pos p (NeZero.ne n)).ne'⟩
  have hcop := Nat.coprime_ordCompl hp.out (NeZero.ne n)
  simp only [subgroupOfPrimitiveMapToOne, Subgroup.mem_map, mem_annihilator_iff,
    Set.mem_singleton_iff, forall_eq, ZMod.coe_unitOfCoprime]
  refine ⟨?_, fun h ↦ ?_⟩
  · rintro ⟨ψ, hψ, rfl⟩
    rw [← Int.cast_natCast] at hψ ⊢
    rw [primitiveCharacter_changeLevel_apply, primitiveCharacter_apply_of_isCoprime, hψ]
    exact Nat.isCoprime_iff_coprime.mpr hcop
  · have hdvd : χ.conductor ∣ n / p ^ n.factorization p := by
      apply Nat.dvd_ordCompl_of_dvd_not_dvd χ.conductor_dvd_level
      simp [← hp.out.coprime_iff_not_dvd, ← Nat.isCoprime_iff_coprime,
        ← apply_ne_zero_iff (χ := χ.primitiveCharacter), h]
    refine ⟨changeLevel hdvd χ.primitiveCharacter, ?_, ?_⟩
    · rw [show (p : ZMod (n / p ^ n.factorization p))
          = ((p : ℤ) : ZMod (n / p ^ n.factorization p)) from (Int.cast_natCast p).symm,
        changeLevel_eq_cast_of_dvd' χ.primitiveCharacter hdvd (Nat.isCoprime_iff_coprime.mpr hcop),
        Int.cast_natCast]
      exact h
    · rw [← changeLevel_trans, changeLevel_primitiveCharacter]

Goal state after:
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'
x b : R
x✝ : b ∈ univ
⊢ b - x + x = b

Tactic:
rw [sub_add_cancel]

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

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j✝ : ZMod N
h1 : ∀ (t : ZMod N), ∑ i, stdAddChar (t * i) = if t = 0 then ↑N else 0
x j : ZMod N
⊢ -x + -j = 0 ↔ x = -j

Tactic:
add_eq_zero_iff_neg_eq,

Goal state after:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j✝ : ZMod N
h1 : ∀ (t : ZMod N), ∑ i, stdAddChar (t * i) = if t = 0 then ↑N else 0
x j : ZMod N
⊢ - -x = -j ↔ x = -j
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s ⩿ insert a s

Tactic:
by simp [← coe_wcovBy_coe]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s.erase a ⩿ s

Tactic:
by simp [← coe_wcovBy_coe]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⋖ t
⊢ ∃ a ∈ t, t.erase a = s

Tactic:
by
  simpa only [← coe_inj, coe_erase] using! h.finset_coe.exists_set_sdiff_singleton

Goal state after:
Module: Mathlib.Analysis.Hofer

Goal state before:
pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
this : Nonempty X
F : ℕ → X → X
hF : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → d x' (F k x') ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun n ↦ Nat.recOn n x F
hu :
  ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / 2 ^ x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
v : ℕ → ℝ := fun n ↦ (ϕ ∘ u) (n + 1)
hv₀ : 0 < v 0
⊢ Tendsto v atTop atTop

Tactic:
apply tendsto_atTop_of_geom_le hv₀ one_lt_two

Goal state after:
X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
this : Nonempty X
F : ℕ → X → X
hF : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → d x' (F k x') ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := ⋯
hu :
  ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key : ∀ (n : ℕ), d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
key₁ : ∀ (x : ℕ), d (u x) (u (x + 1)) ≤ ε / 2 ^ x
key₂ : ∀ (x : ℕ), 2 * ϕ (u x) < ϕ (u (x + 1))
cauchy_u : CauchySeq u
y : X
limy : Tendsto u atTop (𝓝 y)
v : ℕ → ℝ := ⋯
hv₀ : 0 < v 0
⊢ ∀ (n : ℕ), 2 * v n ≤ v (n + 1)
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case e'_4
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ Disjoint {i} (insert i s)ᶜ

Tactic:
rw [Finset.disjoint_singleton_left, notMem_compl]

Goal state after:
case e'_4
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ i ∈ insert i s
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : (↑#ι).HolderConjugate p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : 1 < ↑#ι
h1 : 0 < ↑#ι - 1
h2 : 0 ≤ 1 / (↑#ι - 1)
h3 : (↑#ι - 1) * (1 / (↑#ι - 1)) ≤ 1
h4 : p = 1 + 1 / (↑#ι - 1)
⊢ ∫⁻ (x : (i : ι) → A i), ∏ i, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ (1 / (↑#ι - 1)) ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ p

Tactic:
h4

Goal state after:
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : (↑#ι).HolderConjugate p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : 1 < ↑#ι
h1 : 0 < ↑#ι - 1
h2 : 0 ≤ 1 / (↑#ι - 1)
h3 : (↑#ι - 1) * (1 / (↑#ι - 1)) ≤ 1
h4 : p = 1 + 1 / (↑#ι - 1)
⊢ ∫⁻ (x : (i : ι) → A i), ∏ i, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ (1 / (↑#ι - 1)) ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + 1 / (↑#ι - 1))
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
⊢ ‖u x‖ₑ ^ p = ‖u x‖ₑ ^ (1 / (↑#ι - 1) * ↑#ι)

Tactic:
hp.conjugate_eq

Goal state after:
ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
⊢ ‖u x‖ₑ ^ (↑#ι / (↑#ι - 1)) = ‖u x‖ₑ ^ (1 / (↑#ι - 1) * ↑#ι)
Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hA : A.IsSymmetric
hB : B.IsSymmetric
hAB : Commute A B
⊢ ⨆ i, ⨆ j, eigenspace A (i, j).2 ⊓ eigenspace B (i, j).1 = ⊤

Tactic:
iSup_comm

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hA : A.IsSymmetric
hB : B.IsSymmetric
hAB : Commute A B
⊢ ⨆ j, ⨆ i, eigenspace A (i, j).2 ⊓ eigenspace B (i, j).1 = ⊤
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
g : Submodule 𝕜 (E × F)
x : F × E
⊢ x ∈ g.adjoint ↔ ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0

Tactic:
simp only [Submodule.adjoint, mem_map, mem_orthogonal, LinearEquiv.coe_coe,
    LinearEquiv.trans_apply, LinearEquiv.skewSwap_symm_apply, coe_symm_linearEquiv, Prod.exists,
    prod_inner_apply, ofLp_fst, ofLp_snd, forall_exists_index, and_imp, coe_linearEquiv]

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
g : Submodule 𝕜 (E × F)
x : F × E
⊢ (∃ y,
      (∀ (u : WithLp 2 (F × E)) (x : E) (x_1 : F),
          (x, x_1) ∈ g → toLp 2 (x_1, -x) = u → ⟪u.fst, y.fst⟫ + ⟪u.snd, y.snd⟫ = 0) ∧
        y.ofLp = x) ↔
    ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0