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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w y : W
⊢ (fderiv ℝ (fun w ↦ ↑(𝐞 (-(L v) w))) w) y = -2 * ↑π * I * ↑((L v) y) * ↑(𝐞 (-(L v) w))

Tactic:
simp only [(hasFDerivAt_fourierChar_neg_bilinear_right L v w).fderiv, neg_mul, neg_smul,
    neg_apply, smul_apply, ContinuousLinearMap.comp_apply, ofRealCLM_apply, smul_eq_mul, neg_inj]

Goal state after:
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w y : W
⊢ 2 * ↑π * I * ↑(𝐞 (-(L v) w)) * ↑((L v) y) = 2 * ↑π * I * ↑((L v) y) * ↑(𝐞 (-(L v) w))
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : 𝓢(E, F)
inst✝ : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -↑k ≤ s
⊢ (fun x ↦ ‖x‖ ^ (-↑k)) =O[cocompact E] fun x ↦ ‖x‖ ^ s

Tactic:
suffices (fun x : ℝ ↦ x ^ (-k : ℤ)) =O[atTop] fun x : ℝ ↦ x ^ s
    from this.comp_tendsto tendsto_norm_cocompact_atTop

Goal state after:
E : Type u_5
F : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : 𝓢(E, F)
inst✝ : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -↑k ≤ s
⊢ (fun x ↦ x ^ (-↑k)) =O[atTop] fun x ↦ x ^ s
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 F
f : 𝓢(E, F)
a b : E
⊢ (compSubConstCLM 𝕜 b) ((compSubConstCLM 𝕜 a) f) = (compSubConstCLM 𝕜 (a + b)) f

Tactic:
ext x
  simp only [compSubConstCLM_apply]
  congr 1
  exact (sub_add_eq_sub_sub_swap x a b).symm

Goal state after:
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: case h'iφ
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
⊢ ∀ᶠ (i : ℝ) in atTop, AEStronglyMeasurable (fun x ↦ i ^ finrank ℝ F * φ (i • x)) μ

Tactic:
filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)
    exact (I.comp_smul hc.ne').aestronglyMeasurable.const_mul _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s : ℝ
⊢ IntegrableAtFilter (fun x ↦ x ^ s) atTop volume ↔ s < -1

Tactic:
refine ⟨fun ⟨t, ht, hint⟩ ↦ ?_, fun h ↦
    ⟨Set.Ioi 1, Ioi_mem_atTop 1, (integrableOn_Ioi_rpow_iff zero_lt_one).mpr h⟩⟩
  obtain ⟨a, ha⟩ := mem_atTop_sets.mp ht
  refine (integrableOn_Ioi_rpow_iff (zero_lt_one.trans_le (le_max_right a 1))).mp ?_
  exact hint.mono_set <| fun x hx ↦ ha _ <| (le_max_left a 1).trans hx.le

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: c : ℝ
hc : 1 < c
⊢ ∫ (t : ℝ) in Ioi c, t⁻¹ / log t ^ 2 = (log c)⁻¹

Tactic:
by
  convert! integral_Ioi_of_hasDerivAt_of_tendsto' (m := 0) (f := fun t ↦ -(log t)⁻¹) ?_
    (integrableOn_inv_div_log_sq_Ioi hc) ?_ using 1
  · simp
  · intro t _
    convert! (hasDerivAt_inv_log (by grind : t ≠ 0) (by grind) (by grind)).neg using 1
    field
  convert! tendsto_log_atTop.inv_tendsto_atTop.neg using 1
  simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.snd ℝ ℝ ℝ).ker
h : LinearMap.snd ℝ ℝ ℝ = 0
⊢ (LinearMap.snd ℝ ℝ ℝ) (0, 1) = 0 (0, 1)

Tactic:
rw [h]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:

Tactic:
_ = ∫⁻ p in polarCoord.symm '' polarCoord.target, f p := by
      rw [← setLIntegral_univ, setLIntegral_congr polarCoord_source_ae_eq_univ.symm,
        polarCoord.symm_image_target_eq_source]
    _ = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (polarCoord.symm p) := by
      rw [lintegral_image_eq_lintegral_abs_det_fderiv_mul volume _
        (fun p _ ↦ (hasFDerivAt_polarCoord_symm p).hasFDerivWithinAt)]
      · simp_rw [det_fderivPolarCoordSymm]; rfl
      exacts [polarCoord.symm.injOn, measurableSet_Ioi.prod measurableSet_Ioo]
    _ = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (polarCoord.symm p) := by
      refine setLIntegral_congr_fun polarCoord.open_target.measurableSet (fun x hx ↦ ?_)
      rw [abs_of_pos hx.1]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
⊢ HasFiniteIntegral (fun a ↦ rexp (c ^ 2 * (b.im ^ 2 / b.re + b.re)) * rexp (-(b.re * (a - b.im * c / b.re) ^ 2)))
    volume

Tactic:
suffices Integrable fun x : ℝ => exp (-(b.re * x ^ 2)) by
    exact (Integrable.comp_sub_right this (b.im * c / b.re)).hasFiniteIntegral.const_mul _

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Integrable (fun x ↦ rexp (-(b.re * x ^ 2))) volume
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℂ E
V : Type u_3
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace ℝ V
inst✝⁸ : FiniteDimensional ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℂ G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L⋆[ℂ] F →L[ℂ] G
⊢ ∫ (ξ : V), (M ((𝓕 f) ξ)) ((𝓕 g) ξ) = ∫ (x : V), (M (f x)) (g x)

Tactic:
by
  simpa using integral_sesq_fourier_eq f (𝓕 g) M

Goal state after:
Module: Mathlib.Analysis.RCLike.Inner

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
c : 𝕜
w : ι → ℝ
f g : (i : ι) → E i
⊢ c * ⟪f, g⟫_[𝕜, w] = ⟪star c • f, g⟫_[𝕜, w]

Tactic:
wInner_smul_left,

Goal state after:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
c : 𝕜
w : ι → ℝ
f g : (i : ι) → E i
⊢ c * ⟪f, g⟫_[𝕜, w] = star (star c) • ⟪f, g⟫_[𝕜, w]
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n : ℕ+
k l : ℕ
h : m.Coprime n
⊢ (↑m ^ k).Coprime (↑n ^ l)

Tactic:
by
  rw [← coprime_coe] at *; apply Nat.Coprime.pow; apply h

Goal state after:
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}
⊢ MeasurableSet A

Tactic:
suffices A = Metric.closedBall (0 : V) (R + 1) by
      rw [this]
      exact Metric.isClosed_closedBall.measurableSet

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}
⊢ A = Metric.closedBall 0 (R + 1)
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[cocompact ℝ] fun x ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ y + x ∈ Icc (x - r) (x + r)

Tactic:
· exact ⟨by linarith [(hr hy).1], by linarith [(hr hy).2]⟩

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

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

Tactic:
← q.num_div_den

Goal state after:
case e'_4
q : ℚ
h : Odd q.num
⊢ 2 * q.den = (↑q.num / ↑q.den / 2).den
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ := ringChar R
n : ℕ
inst✝ : NeZero (p * n)
hζ : IsPrimitiveRoot ζ (p * n)
h : p ≠ 0 ∧ n ≠ 0
this : NeZero p
hp : Fact (Nat.Prime p)
⊢ (frobenius R p) (ζ ^ n) = (frobenius R p) 1

Tactic:
frobenius_def,

Goal state after:
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ := ringChar R
n : ℕ
inst✝ : NeZero (p * n)
hζ : IsPrimitiveRoot ζ (p * n)
h : p ≠ 0 ∧ n ≠ 0
this : NeZero p
hp : Fact (Nat.Prime p)
⊢ (ζ ^ n) ^ p = (frobenius R p) 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
ξ : Rˣ
hξ : ↑ξ ^ k = 1
⊢ ∃ i < k, ζ ^ i = ξ

Tactic:
exact h.eq_pow_of_mem_rootsOfUnity <| (mem_rootsOfUnity' k ξ).mpr hξ

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

Goal state before:
pp: case neg
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
prod : map (Int.castRingHom (ZMod p)) P * map (Int.castRingHom (ZMod p)) Q ∣ X ^ n - 1
R : (ZMod p)[X]
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
⊢ False

Tactic:
rw [hR, ← mul_assoc, ← Polynomial.map_mul, ← sq, Polynomial.map_pow] at prod

Goal state after:
case neg
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
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ cyclotomic n ℚ = minpoly ℚ μ

Tactic:
rw [← map_cyclotomic_int, cyclotomic_eq_minpoly h hpos]
  exact (minpoly.isIntegrallyClosed_eq_field_fractions' _ (IsPrimitiveRoot.isIntegral h hpos)).symm

Goal state after:
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: 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
⊢ Q.degree < (minpoly R B.gen).degree

Tactic:
let : Nontrivial R := Nontrivial.of_polynomial_ne hQ

Goal state after:
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
this : Nontrivial R := Nontrivial.of_polynomial_ne hQ
⊢ Q.degree < (minpoly R B.gen).degree
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + (k + 1)
h : Irreducible (cyclotomic (p ^ (m + (k + 1))) R)
⊢ Irreducible (cyclotomic (p ^ m) R)

Tactic:
have : m + k ≠ 0 := (add_pos_of_pos_of_nonneg hm k.zero_le).ne'

Goal state after:
case inr.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + (k + 1)
h : Irreducible (cyclotomic (p ^ (m + (k + 1))) R)
this : m + k ≠ 0
⊢ Irreducible (cyclotomic (p ^ m) R)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + (k + 1)
h : Irreducible ((expand R p) (cyclotomic (p ^ (m + k)) R))
this : m + k ≠ 0
⊢ Irreducible (cyclotomic (p ^ m) R)

Tactic:
exact hk (by lia) (of_irreducible_expand hp.ne_zero h)

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

Goal state before:
pp: case hb.ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
hi : 0 ≠ 2 ∧ 0 ≠ 1 ∧ 0 ∣ n ∧ 0 < n
⊢ False

Tactic:
zero_dvd_iff

Goal state after:
case hb.ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
hi : 0 ≠ 2 ∧ 0 ≠ 1 ∧ n = 0 ∧ 0 < n
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.Basic

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

Tactic:
refine
    ⟨fun H ↦ of_union_of_dvd A B h, fun H => (iff_adjoin_eq_top _ A _).2
      ⟨fun s hs ↦ ?_, ?_⟩⟩
  · exact H.exists_isPrimitiveRoot (subset_union_left hs)
  · rw [_root_.eq_top_iff, ← ((iff_adjoin_eq_top _ A B).1 H).2]
    refine adjoin_mono fun x hx => ?_
    simp only [union_singleton, mem_insert_iff, mem_ofPred_eq] at hx ⊢
    obtain ⟨m, rfl | hm, hxpow⟩ := hx
    · obtain ⟨y, ⟨hy, hy', ⟨z, rfl⟩⟩⟩ := h
      exact ⟨_, ⟨hy, hy', by simp only [pow_mul, hxpow, one_pow]⟩⟩
    · exact ⟨m, ⟨hm, hxpow⟩⟩

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
⊢ ∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0

Tactic:
have : Fact (ringChar F).Prime := ⟨CharP.char_is_prime F _⟩
  have htr := (traceForm_nondegenerate (ZMod (ringChar F)) F).1 a
  simp_rw [Algebra.traceForm_apply] at htr
  by_contra! hf
  exact ha (htr hf)

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case pos
n : ℕ
x : ℤ
hn : n = 0
h : IsUnit x
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
rcases Int.isUnit_eq_one_or h with h | h

Goal state after:
case pos.inl
n : ℕ
x : ℤ
hn : n = 0
h✝ : IsUnit x
h : x = 1
⊢ ↑x * (↑x)⁻¹ = 1

case pos.inr
n : ℕ
x : ℤ
hn : n = 0
h✝ : IsUnit x
h : x = -1
⊢ ↑x * (↑x)⁻¹ = 1
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : X ^ p ^ 1 = X ^ Fintype.card (ZMod p)
⊢ IsSplittingField (ZMod p) (ZMod p) (X ^ p ^ 1 - X)

Tactic:
rw [h]

Goal state after:
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : X ^ p ^ 1 = X ^ Fintype.card (ZMod p)
⊢ IsSplittingField (ZMod p) (ZMod p) (X ^ Fintype.card (ZMod p) - X)
Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

Goal state before:
pp: 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, IsPrimitiveRoot m n

Tactic:
obtain ⟨m, hm⟩ := hm.prim
    use (e hm.toRootsOfUnity).val.val
    rw [IsPrimitiveRoot.coe_units_iff, IsPrimitiveRoot.coe_submonoidClass_iff]
    refine .map_of_injective ?_ e.injective
    rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, ← IsPrimitiveRoot.coe_units_iff]

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

Goal state before:
pp: n : ℤ
⊢ χ₄ ↑n = χ₄ ↑(n % 4)

Tactic:
← ZMod.intCast_mod n 4,

Goal state after:
n : ℤ
⊢ χ₄ ↑(n % ↑4) = χ₄ ↑(n % 4)
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter 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)
h : χ.primitiveCharacter ↑p = 1
hdvd : χ.conductor ∣ n / p ^ n.factorization p
⊢ ((changeLevel hdvd) χ.primitiveCharacter) ↑↑p = 1

Tactic:
changeLevel_eq_cast_of_dvd' χ.primitiveCharacter hdvd (Nat.isCoprime_iff_coprime.mpr hcop),

Goal state after:
case refine_2.refine_1
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter 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)
h : χ.primitiveCharacter ↑p = 1
hdvd : χ.conductor ∣ n / p ^ n.factorization p
⊢ χ.primitiveCharacter ↑↑p = 1
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, 1 a * ψ a + 1 = ∑ a ∈ {0}ᶜ, 1 a * ψ a + 1

Tactic:
by
    simp [← ({0} : Finset R).sum_compl_add_sum]

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

Goal state before:
pp: S : Type u_2
inst✝¹ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst✝ : NoZeroDivisors S
this : ψ (-1) ^ 2 = 1
⊢ ψ.Even ∨ ψ.Odd

Tactic:
convert! sq_eq_one_iff.mp this

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝ : E
p : ℝ
hp : 1 < p
hx : x✝ = 0
h2p : 0 < p - 1
x : E
⊢ ‖x‖ ^ p = ‖x‖ * ‖x‖ ^ (p - 1)

Tactic:
rw [← rpow_one_add' (norm_nonneg x) (by positivity)]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝ : E
p : ℝ
hp : 1 < p
hx : x✝ = 0
h2p : 0 < p - 1
x : E
⊢ ‖x‖ ^ p = ‖x‖ ^ (1 + (p - 1))
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasStrictFDerivAt (fun x ↦ ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x ↔
    HasStrictFDerivAt (fun x ↦ (‖x‖ ^ 2) ^ (p / 2)) ((p / 2 * (‖x‖ ^ 2) ^ (p / 2 - 1)) • 2 • (innerSL ℝ) x) x

Tactic:
← Real.rpow_natCast_mul (norm_nonneg _),

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasStrictFDerivAt (fun x ↦ ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x ↔
    HasStrictFDerivAt (fun x ↦ ‖x‖ ^ (↑2 * (p / 2))) ((p / 2 * ‖x‖ ^ (↑2 * (p / 2 - 1))) • 2 • (innerSL ℝ) x) x
Module: Mathlib.Order.Grade

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

Tactic:
refine and_congr_right' ⟨fun h c hac ↦ h hac, fun h c hac hcb ↦
    @h ⟨c, mem_iff_forall_le_or_ge.2 fun d hd ↦ ?_⟩ hac hcb⟩
  classical
  obtain hda | had := le_or_gt (⟨d, hd⟩ : s) a
  · exact .inr ((Subtype.coe_le_coe.2 hda).trans hac.le)
  obtain hbd | hdb := le_or_gt b ⟨d, hd⟩
  · exact .inl (hcb.le.trans hbd)
  · cases h had hdb

Goal state after:
Module: Mathlib.Order.Grade

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
s : Flag α
a : ↥s
h : IsMax a
b : α
hab : ↑a ≤ b
⊢ b ≤ ↑a

Tactic:
refine @h ⟨b, mem_iff_forall_le_or_ge.2 fun c hc ↦ ?_⟩ hab
    classical
    exact .inr <| hab.trans' <| h.isTop ⟨c, hc⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ #(Ico s t) = 2 ^ (#t - #s) - 1

Tactic:
card_Ico_eq_card_Icc_sub_one,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ #(Icc s t) - 1 = 2 ^ (#t - #s) - 1
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder β
f : Finset α → β
⊢ StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s < f (cons a s ha)

Tactic:
by
  classical simp [strictMono_iff_forall_covBy, covBy_iff_exists_cons]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
h₁ : (fun a ↦ ↑(χ₈ a) * τ ^ ↑a) = fun a ↦ χ a * ψ₈char a
⊢ ↑0 * τ ^ ↑0 + ↑1 * τ ^ ↑1 + ↑0 * τ ^ ↑2 + ↑(-1) * τ ^ ↑3 + ↑0 * τ ^ ↑4 + ↑(χ₈ 5) * τ ^ ↑5 + ↑(χ₈ 6) * τ ^ ↑6 +
      ↑(χ₈ 7) * τ ^ ↑7 =
    2 * (τ - τ ^ 3)

Tactic:
show χ₈ 5 = -1 from rfl,

Goal state after:
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
h₁ : (fun a ↦ ↑(χ₈ a) * τ ^ ↑a) = fun a ↦ χ a * ψ₈char a
⊢ ↑0 * τ ^ ↑0 + ↑1 * τ ^ ↑1 + ↑0 * τ ^ ↑2 + ↑(-1) * τ ^ ↑3 + ↑0 * τ ^ ↑4 + ↑(-1) * τ ^ ↑5 + ↑(χ₈ 6) * τ ^ ↑6 +
      ↑(χ₈ 7) * τ ^ ↑7 =
    2 * (τ - τ ^ 3)
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsIdempotentElem T
⊢ T.IsPositive ↔ T.IsSymmetric

Tactic:
by
  refine ⟨fun h => h.isSymmetric, fun h => ⟨h, fun x => ?_⟩⟩
  rw [← hT.eq, Module.End.mul_apply, h]
  exact inner_self_nonneg

Goal state after: