mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
a : ℕ
x✝ : a > 0
x : ℕ × ℕ
_hx : x ∈ a.divisorsAntidiagonal
⊢ μ x.1 • g x.2 = ↑(μ x.1) * g x.2

Tactic:
zsmul_eq_mul

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
a : ℕ
x✝ : a > 0
x : ℕ × ℕ
_hx : x ∈ a.divisorsAntidiagonal
⊢ ↑(μ x.1) * g x.2 = ↑(μ x.1) * g x.2
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : ℕ → R := fun n ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ i ∈ n.divisorsAntidiagonal, μ i.1 • G i.2 = f n

Tactic:
apply sum_eq_iff_sum_smul_moebius_eq.mp _ n hn

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : ℕ → R := ⋯
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∀ n > 0, ∑ i ∈ n.divisors, f i = G n
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
a : ℕ
x✝¹ : a > 0
x✝ : a ∈ s
x : ℕ × ℕ
_hx : x ∈ a.divisorsAntidiagonal
⊢ μ x.1 • g x.2 = ↑(μ x.1) * g x.2

Tactic:
zsmul_eq_mul

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
a : ℕ
x✝¹ : a > 0
x✝ : a ∈ s
x : ℕ × ℕ
_hx : x ∈ a.divisorsAntidiagonal
⊢ ↑(μ x.1) * g x.2 = ↑(μ x.1) * g x.2
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ ‖f v - f (v + i w)‖ = 0

Tactic:
rw [hR_bd v _, hR_bd (v + i w) _, sub_zero, norm_zero]

Goal state after:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ R ≤ ‖v + i w‖

E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ R ≤ ‖v‖
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 (eval μ (X ^ p)) (map (algebraMap ℤ K) (minpoly ℤ (μ ^ p))) = 0

Tactic:
eval_X_pow,

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 (μ ^ p) (map (algebraMap ℤ K) (minpoly ℤ (μ ^ p))) = 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
⊢ (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1

Tactic:
by
  have h0d : 0 < d := Nat.pos_of_dvd_of_pos hdvd (by positivity)
  rw [← prod_cyclotomic_eq_X_pow_sub_one h0d,
    ← prod_cyclotomic_eq_X_pow_sub_one (by positivity), mul_comm,
    Finset.prod_sdiff (by gcongr)]

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

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

Tactic:
eval_X_pow,

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ 0 + (∏ i ∈ n.properDivisors, cyclotomic i R) * P = X ^ n - 1

Tactic:
by rwa [zero_add, mul_comm]

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
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this : ↑n = ∏ j ∈ n.divisors.erase 1, eval 1 (cyclotomic j ℤ)
⊢ False

Tactic:
←
    Finset.prod_sdiff <| @range_pow_padicValNat_subset_divisors' p _ _,

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
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)) *
      ∏ x ∈ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case neg
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : ¬∃ s ∈ S, s ≠ 0
⊢ IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension (∅ ∪ {1} \ {0}) A B

Tactic:
empty_union,

Goal state after:
case neg
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : ¬∃ s ∈ S, s ≠ 0
⊢ IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension ({1} \ {0}) A B
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case neg
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : ¬∃ s ∈ S, s ≠ 0
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B

Tactic:
· rw [eq_self_sdiff_zero S, eq_self_sdiff_zero (S ∪ {1}), union_sdiff_distrib,
      show S \ {0} = ∅ by aesop, empty_union, show {1} \ {0} = {1} by simp]
    refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩
    · refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs _ ↦ ⟨1, by simp [mem_singleton_iff.1 hs]⟩, ?_⟩
      simpa [adjoin_singleton_one] using subsingleton_iff_bot_eq_top.mpr inferInstance
    · refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs ↦ (notMem_empty s hs).elim, ?_⟩
      simp [singleton_one]

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

Goal state before:
pp: case refine_2
n✝ : ℕ
inst✝⁴ : NeZero n✝
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n✝} A B
b : B
x✝ : b ∈ {b | ∃ n ∈ {n✝}, n ≠ 0 ∧ b ^ n = 1}
n : ℕ
hb : n = n✝ ∧ n ≠ 0 ∧ b ^ n = 1
⊢ IsIntegral A b

Tactic:
exact ⟨X ^ n - 1,
      ⟨monic_X_pow_sub_C _ (hb.1 ▸ NeZero.ne _), by simpa [sub_eq_zero] using hb.2.2⟩⟩

Goal state after:
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 : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
refine hζ.norm_pow_sub_one_of_prime_pow_ne_two hirr hs fun h => ?_

Goal state after:
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
h : p ^ (k - s + 1) = 2
⊢ False
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ ↑(d * a₀) = ↑((↑u).val * d)

Tactic:
natCast_eq_natCast_iff,

Goal state after:
case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ d * a₀ ≡ (↑u).val * d [MOD N]
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case a
S : Set ℕ
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension S K L
M : Type u_1
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤
⊢ ⇑i '' {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} ⊆ ↑(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})

Tactic:
rintro _ ⟨y, ⟨n, hn, h1, h2⟩, rfl⟩

Goal state after:
case a
S : Set ℕ
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension S K L
M : Type u_1
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤
y : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : y ^ n = 1
⊢ i y ∈ ↑(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case a
S : Set ℕ
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension S K L
M : Type u_1
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsSepClosed M
this✝ : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
this : NeZero n
y : L
hy : IsPrimitiveRoot y n
m : ℕ
h2 : (i.toRingHom y ^ m) ^ n = 1
⊢ i.toRingHom y ^ m ∈ ↑(IntermediateField.adjoin K (⇑i '' {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))

Tactic:
exact pow_mem (IntermediateField.subset_adjoin K (i '' {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
      ⟨y, ⟨n, hn, h1, hy.pow_eq_one⟩, rfl⟩) m

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

Goal state before:
pp: case right
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
f : AlgebraicClosure K →ₐ[K] AlgebraicClosure K
x : AlgebraicClosure K
hx : x ∈ Subalgebra.map f (IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}).toSubalgebra
⊢ x ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
Subalgebra.mem_map

Goal state after:
case right
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
f : AlgebraicClosure K →ₐ[K] AlgebraicClosure K
x : AlgebraicClosure K
hx : ∃ x_1 ∈ (IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}).toSubalgebra, f x_1 = x
⊢ x ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

Goal state before:
pp: case h
n : ℕ
inst✝² : NeZero n
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
hm✝ : HasEnoughRootsOfUnity M n
e : ↥(rootsOfUnity n M) ≃* ↥(rootsOfUnity n N)
m : M
hm : IsPrimitiveRoot m n
⊢ IsPrimitiveRoot (↑↑(e hm.toRootsOfUnity)) n

Tactic:
IsPrimitiveRoot.coe_units_iff,

Goal state after:
case h
n : ℕ
inst✝² : NeZero n
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
hm✝ : HasEnoughRootsOfUnity M n
e : ↥(rootsOfUnity n M) ≃* ↥(rootsOfUnity n N)
m : M
hm : IsPrimitiveRoot m n
⊢ IsPrimitiveRoot (↑(e hm.toRootsOfUnity)) n
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u_1
inst✝² : AddGroup R
inst✝¹ : Fintype R
R' : Type u_2
inst✝ : CommRing R'
ψ : AddChar R R'
hψ : ψ = 1
⊢ ∑ a, ψ a = ↑(Fintype.card R)

Tactic:
simp [hψ]

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'
inst✝ : Nontrivial R'
χ : MulChar R R'
a : R
⊢ χ a ≠ 0 → IsUnit a

Tactic:
simpa using (map_nonunit χ).mt

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∈ χ.conductorSet
⊢ χ.conductor ∣ d

Tactic:
have : NeZero d := ⟨by
    contrapose hd
    exact hd ▸ zero_ne_mem_conductorSet χ⟩
  suffices d.gcd χ.conductor ∈ χ.conductorSet by
    have : χ.conductor ≤ d.gcd χ.conductor := Nat.sInf_le this
    contrapose! this
    refine Nat.lt_of_le_of_ne ?_ (Nat.gcd_eq_right_iff_dvd.not.mpr this)
    exact Nat.gcd_le_right _ <| Nat.pos_of_ne_zero <| conductor_ne_zero χ
  obtain ⟨hd, χ₀, hχ₀⟩ := hd
  suffices (changeLevel (d.dvd_mul_right χ.conductor)) χ₀ =
      (changeLevel (χ.conductor.dvd_mul_left d)) χ.primitiveCharacter by
    obtain ⟨_, χ₁, hχ₁⟩ := factorsThrough_gcd χ₀ χ.primitiveCharacter this
    refine ⟨Nat.dvd_trans (d.gcd_dvd_left χ.conductor) hd, χ₁, ?_⟩
    rw [changeLevel_trans _ (d.gcd_dvd_left χ.conductor), ← hχ₁, hχ₀]
  have : NeZero (d * χ.conductor * n) :=
    ⟨Nat.mul_ne_zero (Nat.mul_ne_zero (NeZero.ne d) χ.conductor_ne_zero) (NeZero.ne n)⟩
  apply changeLevel_injective <| Nat.dvd_mul_right (d * χ.conductor) n
  rw [← changeLevel_trans, ← changeLevel_trans,
    changeLevel_trans _ hd (n.dvd_mul_left (d * χ.conductor)), ← hχ₀,
    changeLevel_trans χ.primitiveCharacter χ.conductor_dvd_level, changeLevel_primitiveCharacter]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
inst✝¹ : NeZero n
inst✝ : Nontrivial R
p : ℕ
hp : Fact (Nat.Prime p)
this : NeZero (n / p ^ n.factorization p)
hcop : p.Coprime (n / p ^ n.factorization p)
ψ : DirichletCharacter R (n / p ^ n.factorization p)
hψ : ψ ↑p = 1
⊢ ((changeLevel ⋯) ψ).primitiveCharacter ↑p = 1

Tactic:
rw [← Int.cast_natCast] at hψ ⊢

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
inst✝¹ : NeZero n
inst✝ : Nontrivial R
p : ℕ
hp : Fact (Nat.Prime p)
this : NeZero (n / p ^ n.factorization p)
hcop : p.Coprime (n / p ^ n.factorization p)
ψ : DirichletCharacter R (n / p ^ n.factorization p)
hψ : ψ ↑↑p = 1
⊢ ((changeLevel ⋯) ψ).primitiveCharacter ↑↑p = 1
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = -1
⊢ ψ (-1) * ψ x = -ψ x

Tactic:
simp [hψ]

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

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = 1
⊢ ψ (-1) * ψ x = ψ x

Tactic:
simp [hψ]

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:
by rw [sub_add_cancel]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case e_a
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ χ ↑(-1) * gaussSum χ (ψ.mulShift ↑(-1)) = χ (-1) * gaussSum χ ψ⁻¹

Tactic:
inv_mulShift

Goal state after:
case e_a
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ χ ↑(-1) * gaussSum χ (ψ.mulShift ↑(-1)) = χ (-1) * gaussSum χ (ψ.mulShift (-1))
Module: Mathlib.Order.Grade

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
s : Flag α
a b : ↥s
⊢ ↑a ⋖ ↑b ↔ a ⋖ b

Tactic:
by simp [covBy_iff_wcovBy_and_not_le]

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
hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3)
⊢ gaussSum χ ψ₈char ^ 2 = 8

Tactic:
hg₁

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
hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3)
⊢ (2 * (τ - τ ^ 3)) ^ 2 = 8
Module: Mathlib.Analysis.InnerProductSpace.Affine

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b : P
v : V
⊢ ⟪-(b -ᵥ a), v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0

Tactic:
inner_neg_left,

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b : P
v : V
⊢ -⟪b -ᵥ a, v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0
Module: Mathlib.Analysis.InnerProductSpace.Affine

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ ⟪a -ᵥ c, b -ᵥ c⟫ = dist b c ^ 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0

Tactic:
rw [real_inner_comm, inner_vsub_vsub_right_eq_dist_sq_left_iff, real_inner_comm]

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

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p : P
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
⊢ dist p b ^ 2 = dist p a ^ 2 + dist a b ^ 2

Tactic:
simpa using dist_sq_lineMap_of_inner_eq_zero 1 h_inner

Goal state after:
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 ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
⊢ (∫⋯∫⁻_{i}, f ∂μ) x ^ p * ((∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p) =
    (∫⋯∫⁻_{i}, f ∂μ) x ^ (p + (1 - k * p)) * ∏ j ∈ s, (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p

Tactic:
rw [ENNReal.rpow_add_of_nonneg]

Goal state after:
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
⊢ (∫⋯∫⁻_{i}, f ∂μ) x ^ p * ((∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p) =
    (∫⋯∫⁻_{i}, f ∂μ) x ^ p * (∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p

case hy
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
⊢ 0 ≤ p

case hz
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
⊢ 0 ≤ 1 - k * p
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
T : E →ₗ[𝕜] E
f : E ≃ₗᵢ[𝕜] F
⊢ (↑f.toLinearEquiv ∘ₗ T ∘ₗ ↑f.symm.toLinearEquiv).IsPositive ↔ T.IsPositive

Tactic:
simp_rw [IsPositive, isSymmetric_linearIsometryEquiv_conj_iff, and_congr_right_iff,
    LinearIsometryEquiv.toLinearEquiv_symm, coe_comp, LinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.coe_symm_toLinearEquiv,
    Function.comp_apply, LinearIsometryEquiv.inner_map_eq_flip]

Goal state after:
𝕜 : 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
T : E →ₗ[𝕜] E
f : E ≃ₗᵢ[𝕜] F
⊢ T.IsSymmetric → ((∀ (x : F), 0 ≤ re ⟪T (f.symm x), f.symm x⟫) ↔ ∀ (x : E), 0 ≤ re ⟪T x, x⟫)