mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (mFourierCoeff ⇑f)
⊢ HasSum (fun i ↦ mFourierCoeff (⇑f) i • mFourier i) f

Tactic:
by
  have sum_L2 := hasSum_mFourier_series_L2 (ContinuousMap.toLp 2 volume ℂ f)
  simp only [mFourierCoeff_toLp] at sum_L2
  refine ContinuousMap.hasSum_of_hasSum_Lp (.of_norm ?_) sum_L2
  simpa only [norm_smul, mFourier_norm, mul_one] using h.norm

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

Goal state before:
pp: G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
⊢ card (AddChar G R) ≤ card G

Tactic:
simpa only [Module.finrank_fintype_fun_eq_card] using
    (AddChar.linearIndependent G R).fintype_card_le_finrank

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommGroup A
B : Subgroup A
hB : B.FG
n : ℕ
hn : n ≠ 0
this : (map (powMonoidHom n) B).subgroupOf B = (powMonoidHom n).range
⊢ ((map (powMonoidHom n) B).subgroupOf B).FiniteIndex

Tactic:
rw [this]

Goal state after:
A : Type u_1
inst✝ : CommGroup A
B : Subgroup A
hB : B.FG
n : ℕ
hn : n ≠ 0
this : (map (powMonoidHom n) B).subgroupOf B = (powMonoidHom n).range
⊢ (powMonoidHom n).range.FiniteIndex
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
⊢ Function.HasTemperateGrowth ⇑g'

Tactic:
by apply hg₁

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ ∑ ψ, ψ a = 0 ↔ a ≠ 0

Tactic:
by
  classical
  cases nonempty_fintype α
  rw [sum_apply_eq_ite, Ne.ite_eq_right_iff]
  exact Nat.cast_ne_zero.2 Fintype.card_ne_zero

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

Goal state before:
pp: n : ℕ+
hn : n ≠ 1
⊢ ∃ p, p.Prime ∧ p ∣ n

Tactic:
by
  obtain ⟨p, hp⟩ := Nat.exists_prime_and_dvd (mt coe_eq_one_iff.mp hn)
  exists (⟨p, Nat.Prime.pos hp.left⟩ : ℕ+); rw [dvd_iff]; apply hp

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case coprime
a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : a.Coprime b
ha' : (μ * ↑ζ) a = 1 a
hb' : (μ * ↑ζ) b = 1 b
⊢ (μ * ↑ζ) (a * b) = 1 (a * b)

Tactic:
IsMultiplicative.map_mul_of_coprime _ hab,

Goal state after:
case coprime
a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : a.Coprime b
ha' : (μ * ↑ζ) a = 1 a
hb' : (μ * ↑ζ) b = 1 b
⊢ (μ * ↑ζ) a * (μ * ↑ζ) b = 1 (a * b)

a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : a.Coprime b
ha' : (μ * ↑ζ) a = 1 a
hb' : (μ * ↑ζ) b = 1 b
⊢ (μ * ↑ζ).IsMultiplicative
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}
this : A = Metric.closedBall 0 (R + 1)
⊢ MeasurableSet A

Tactic:
rw [this]

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}
this : A = Metric.closedBall 0 (R + 1)
⊢ MeasurableSet (Metric.closedBall 0 (R + 1))
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
ζ : M
⊢ IsPrimitiveRoot ζ 1 → ζ = 1

pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
ζ : M
⊢ ζ = 1 → IsPrimitiveRoot ζ 1

Tactic:
· intro h; rw [← pow_one ζ, h.pow_eq_one]

Goal state after:
case mpr
M : Type u_1
inst✝ : CommMonoid M
ζ : M
⊢ ζ = 1 → IsPrimitiveRoot ζ 1
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
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm
this : (fun w ↦ ∫ (v : V), 𝐞 (-w v) • f v) = (fun w ↦ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) ∘ ⇑A
⊢ Tendsto (fun x ↦ ∫ (v : V), 𝐞 (-x v) • f v ∂volume) (cocompact (StrongDual ℝ V)) (𝓝 0)

Tactic:
rw [this]

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
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm
this : (fun w ↦ ∫ (v : V), 𝐞 (-w v) • f v) = (fun w ↦ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) ∘ ⇑A
⊢ Tendsto ((fun w ↦ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) ∘ ⇑A) (cocompact (StrongDual ℝ V)) (𝓝 0)
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 _ i
    rw [pow_zero, ← pow_zero B.gen, ← Fin.val_mk B.dim_pos, ← B.basis_eq_pow,
      B.basis.repr_self_apply]
    split_ifs
    · exact isIntegral_one
    · exact isIntegral_zero

Goal state after:
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
x✝ : 0 < 1
⊢ cyclotomic (m * p) R = cyclotomic m R ^ (p - 1)

Tactic:
cyclotomic_mul_prime_eq_pow_of_not_dvd R hm

Goal state after:
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
x✝ : 0 < 1
⊢ cyclotomic m R ^ (p - 1) = cyclotomic m R ^ (p - 1)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
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
this : {b | n ≠ 0 ∧ b ^ n = 1} = ↑(nthRoots n 1).toFinset
⊢ {b | n ≠ 0 ∧ b ^ n = 1}.Finite

Tactic:
rw [this]

Goal state after:
case refine_1
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
this : {b | n ≠ 0 ∧ b ^ n = 1} = ↑(nthRoots n 1).toFinset
⊢ (↑(nthRoots n 1).toFinset).Finite
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ (q - 1) ^ φ n < (eval (↑q) (cyclotomic n ℤ)).natAbs

Tactic:
rw [← @Nat.cast_lt ℝ, Nat.cast_pow, Nat.cast_sub hq'.le, Nat.cast_one, Nat.cast_natAbs]

Goal state after:
case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ (↑q - 1) ^ φ n < ↑|eval (↑q) (cyclotomic n ℤ)|
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
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝ : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
b : B
hb : b ∈ {ζ}
⊢ ⟨b, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

pp: case refine_2
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝ : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
a : A
⊢ ⟨(algebraMap A B) a, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

pp: case refine_3
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝² : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
b₁ b₂ : B
x✝¹ : b₁ ∈ A[ζ]
x✝ : b₂ ∈ A[ζ]
hb₁ : ⟨b₁, x✝¹⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
hb₂ : ⟨b₂, x✝⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
⊢ ⟨b₁ + b₂, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

pp: case refine_4
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝² : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
b₁ b₂ : B
x✝¹ : b₁ ∈ A[ζ]
x✝ : b₂ ∈ A[ζ]
hb₁ : ⟨b₁, x✝¹⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
hb₂ : ⟨b₂, x✝⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
⊢ ⟨b₁ * b₂, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
· rw [Set.mem_singleton_iff] at hb
        refine subset_adjoin ?_
        simp only [mem_singleton_iff, exists_eq_left, mem_ofPred_eq, hb]
        rw [← Subalgebra.coe_eq_one, Subalgebra.coe_pow, Subtype.coe_mk]
        exact ⟨NeZero.ne n, ((IsPrimitiveRoot.iff_def ζ n).1 h).1⟩

Goal state after:
case refine_2
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝ : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
a : A
⊢ ⟨(algebraMap A B) a, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

case refine_3
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝² : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
b₁ b₂ : B
x✝¹ : b₁ ∈ A[ζ]
x✝ : b₂ ∈ A[ζ]
hb₁ : ⟨b₁, x✝¹⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
hb₂ : ⟨b₂, x✝⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
⊢ ⟨b₁ + b₂, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

case refine_4
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝² : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
b₁ b₂ : B
x✝¹ : b₁ ∈ A[ζ]
x✝ : b₂ ∈ A[ζ]
hb₁ : ⟨b₁, x✝¹⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
hb₂ : ⟨b₂, x✝⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
⊢ ⟨b₁ * b₂, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case pos.inl
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
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h✝ : p ∣ ps.prod id * n
h : p ∣ ps.prod id
⊢ False

pp: case pos.inr
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
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h✝ : p ∣ ps.prod id * n
h : p ∣ n
⊢ False

Tactic:
· have ⟨q, hq, hq'⟩ := (pp.prime.dvd_finsetProd_iff id).mp h
      rw [Finset.mem_filter, Nat.mem_primeFactors,
        ← (Nat.prime_dvd_prime_iff_eq pp hq.1.1).mp hq'] at hq
      exact hq.2 hpx

Goal state after:
case pos.inr
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
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h✝ : p ∣ ps.prod id * n
h : p ∣ n
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
⊢ IsCyclotomicExtension S K ↥(IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})

Tactic:
have key : ∀ b ∈ {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}, IsAlgebraic K b := by
    rintro b ⟨n, hn, h1, h2⟩
    exact ⟨X ^ n - 1, (monic_X_pow_sub_C (1 : K) h1).ne_zero, by simp [h2]⟩

Goal state after:
S : Set ℕ
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
key : ∀ b ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}, IsAlgebraic K b
⊢ IsCyclotomicExtension S K ↥(IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case inl
a : ZMod 0
⊢ ∃ d, d ∣ 0 ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
change ℤ at a
    rcases eq_or_ne a 0 with rfl | ha
    · refine ⟨0, dvd_zero _, 1, isUnit_one, by rw [Nat.cast_zero, mul_zero]⟩
    refine ⟨a.natAbs, dvd_zero _, Int.sign a, ?_, (Int.sign_mul_natAbs a).symm⟩
    rcases lt_or_gt_of_ne ha with h | h
    · simp only [Int.sign_eq_neg_one_of_neg h, IsUnit.neg_iff, isUnit_one]
    · simp only [Int.sign_eq_one_of_pos h, isUnit_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'
this✝ : CharP K p
this : CharP K' p
n : ℕ+
hKK' : p ^ ↑n = Fintype.card K'
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'

Tactic:
hK'

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'
this✝ : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hKK' : p ^ ↑n = p ^ ↑n'
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ ↑n'
⊢ K ≃ₐ[ZMod p] K'
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2 + 2 * (n / 4))

Tactic:
pow_add,

Goal state after:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2) * (-1) ^ (2 * (n / 4))
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
⊢ χ⁻¹ = χ

Tactic:
by
  ext x
  rw [inv_apply_eq_inv]
  rcases hχ x with (h₀ | h₁ | h₂)
  · rw [h₀, Ring.inverse_zero]
  · rw [h₁, Ring.inverse_one]
  · -- Porting note (#11573): was `by norm_cast`
    have : (-1 : R') = (-1 : R'ˣ) := by norm_cast; simp
    rw [h₂, this, Ring.inverse_unit (-1 : R'ˣ), inv_neg, inv_one]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
⊢ χ * χ = χ⁻¹ * χ

Tactic:
hχ.inv

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
⊢ χ * χ = χ * χ
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
h : IsCyclotomicExtension S A ↥C
this : Subalgebra.map C.val (adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
x✝ : B
⊢ ∀ x ∈ S, ¬x = 0 → x✝ ^ x = 1 → x✝ ∈ C

Tactic:
exact fun n hn₁ hn₂ hx ↦ h.mem_of_pow_eq_one S C hn₁ hn₂ hx

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
⊢ χ ^ (2 * n + 1) = χ

Tactic:
pow_add,

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
⊢ χ ^ (2 * n) * χ ^ 1 = χ
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
this : adjoin A {b | n ≠ 0 ∧ b ^ n = 1} = A[ζ]
⊢ C = adjoin A {x | n ≠ 0 ∧ x ^ n = 1} ↔ C = A[ζ]

Tactic:
rw [this]

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

Goal state before:
pp: A : Type u
B : Type v
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝¹ : NeZero n₁
inst✝ : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₁ : IsPrimitiveRoot ((algebraMap (↥C₁) B) ζ₁) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂) n₂
hζ :
  IsPrimitiveRoot
    ((algebraMap (↥C₁) B) ζ₁ ^ (n₁ / n₁.factorizationLCMLeft n₂) *
      (algebraMap (↥C₂) B) ζ₂ ^ (n₂ / n₁.factorizationLCMRight n₂))
    (n₁.lcm n₂)
⊢ IsCyclotomicExtension {n₁.lcm n₂} A ↥A[(algebraMap (↥C₁) B) ζ₁, (algebraMap (↥C₂) B) ζ₂]

Tactic:
hζ₁.adjoin_pair_eq A hζ₂ (NeZero.ne _) (NeZero.ne _) hζ

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝³ : Field R
inst✝² : Fintype R
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
⊢ ∑ a ∈ {0}ᶜ, ψ a + ψ 0 = 0

Tactic:
rw [← AddChar.sum_eq_zero_of_ne_one hψ, ← Finset.sum_compl_add_sum (s := {0})]

Goal state after:
R : Type u_1
R' : Type u_2
inst✝³ : Field R
inst✝² : Fintype R
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
⊢ ∑ a ∈ {0}ᶜ, ψ a + ψ 0 = ∑ i ∈ {0}ᶜ, ψ i + ∑ i ∈ {0}, ψ i
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

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

Tactic:
Odd

Goal state after:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = -1
⊢ ψ (-x) = -ψ x
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:

Tactic:
T μ p f (insert i s)
      = ∫⋯∫⁻_insert i s,
            f ^ (1 - (s.card : ℝ) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) ^ p ∂μ := by
          -- unfold `T` and reformulate the exponents
          simp_rw [T, card_insert_of_notMem hi]
          congr!
          push_cast
          ring
    _ = ∫⋯∫⁻_s, (fun x ↦ ∫⁻ (t : A i),
            (f (update x i t) ^ (1 - (s.card : ℝ) * p)
            * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (update x i t) ^ p) ∂(μ i)) ∂μ := by
          -- pull out the integral over `xᵢ`
          rw [lmarginal_insert' _ _ hi]
          · simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
          · change Measurable (fun x ↦ _)
            simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
            refine (hf.pow_const _).mul <| Finset.measurable_fun_prod _ ?_
            exact fun _ _ ↦ hf.lmarginal μ |>.pow_const _
    _ ≤ T μ p (∫⋯∫⁻_{i}, f ∂μ) s := lmarginal_mono (s := s) (fun x ↦ ?_)

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
⊢ ∫⁻ (t : A i), f (update x i t) ^ (1 - ↑(#s) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (update x i t) ^ p ∂μ i ≤
    ((∫⋯∫⁻_{i}, f ∂μ) ^ (1 - (↑(#s) - 1) * p) * ∏ i_1 ∈ s, (∫⋯∫⁻_{i_1}, ∫⋯∫⁻_{i}, f ∂μ ∂μ) ^ p) x
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case hi
ι : 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
t : A i
⊢ i ∈ {i}

Tactic:
exact Iff.mpr Finset.mem_singleton rfl

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

Goal state before:
pp: case hxy.e'_6.a
ι : 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
j : ι
hj : j ∈ s
⊢ (∫⋯∫⁻_{i, j}, f ∂μ) x = (∫⋯∫⁻_{j} ∪ {i}, f ∂μ) x

Tactic:
congr
                  rw [Finset.union_comm]
                  rfl

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y : 𝕜
⊢ (adjoint counit) (x * y) =
    (↑(lidIsometry 𝕜 E).symm.symm.toLinearEquiv ∘ₗ adjoint (LinearMap.lTensor 𝕜 counit)) (x ⊗ₜ[𝕜] y)

Tactic:
simp only [LinearIsometryEquiv.symm_symm, toLinearEquiv_lidIsometry, adjoint_lTensor,
          coe_comp, LinearEquiv.coe_coe, Function.comp_apply, lTensor_tmul, lid_tmul]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y : 𝕜
⊢ (adjoint counit) (x * y) = x • (adjoint counit) y
Module: Mathlib.Analysis.InnerProductSpace.Semisimple

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
this : q ⊔ qᗮ = ⊤
⊢ q ⊔ qᗮ ⊓ p = p

Tactic:
rw [← sup_inf_assoc_of_le _ hq₂, this, top_inf_eq p]

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)
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
p : ℝ
ι : Type := Fin (finrank ℝ E)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
⊢ ℝ≥0

Tactic:
exact (c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) * (c ^ p)⁻¹

Goal state after: