mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: 𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
⊢ IsHilbertSum 𝕜 (fun b ↦ ↥(bif b then K else Kᗮ)) fun b ↦ (bif b then K else Kᗮ).subtypeₗᵢ

Tactic:
have : ∀ b, CompleteSpace (↥(cond b K Kᗮ)) := by
    intro b
    cases b <;> first | exact instOrthogonalCompleteSpace K | assumption

Goal state after:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ IsHilbertSum 𝕜 (fun b ↦ ↥(bif b then K else Kᗮ)) fun b ↦ (bif b then K else Kᗮ).subtypeₗᵢ
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
this : ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f
⊢ |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f

Tactic:
rwa [← Real.norm_eq_abs, ← norm_iteratedFDeriv_eq_norm_iteratedDeriv]

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

Goal state before:
pp: a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
⊢ HasDerivAt (fun t ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x

Tactic:
convert! (((hasDerivAt_id _).add_const _).rpow_const _).div_const _ using 1

Goal state after:
case e'_9
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
⊢ (x + m) ^ a = 1 * (a + 1) * (id x + m) ^ (a + 1 - 1) / (a + 1)

case convert_3
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
⊢ id x + m ≠ 0 ∨ 1 ≤ a + 1
Module: Mathlib.MeasureTheory.Integral.Asymptotics

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
f : α → E
g : α → F
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
μ : Measure α
hfm : AEStronglyMeasurable f μ
hf : f =O[⊤] g
hg : Integrable g μ
⊢ Integrable f μ

Tactic:
rewrite [

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
f : α → E
g : α → F
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
μ : Measure α
hfm : AEStronglyMeasurable f μ
hf : f =O[⊤] g
hg : Integrable g μ
⊢ Integrable f μ
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s : ℂ
t : ℝ
ht : 0 < t
hs : s.re ≤ 0
⊢ IntegrableOn (deriv fun x ↦ ‖↑x ^ s‖) (Ioi t) volume

Tactic:
by
  rw [integrableOn_congr_fun (fun x hx ↦ by
    rw [deriv_norm_ofReal_cpow _ (ht.trans hx)]) measurableSet_Ioi]
  obtain hs | hs := eq_or_lt_of_le hs
  · simp_rw [hs, zero_mul]
    exact integrableOn_zero
  · replace hs : s.re - 1 < -1 := by rwa [sub_lt_iff_lt_add, neg_add_cancel]
    exact (integrableOn_Ioi_rpow_of_lt hs ht).const_mul s.re

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

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ 𝓕 f w = ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v

Tactic:
simp_rw [fourier_real_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul,
    mul_assoc]

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

Goal state before:
pp: p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (fun x ↦ b * x ^ (p - 1)) atTop atTop

Tactic:
exact Tendsto.const_mul_atTop hb (tendsto_rpow_atTop (by linarith))

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

Goal state before:
pp: case inr
b : ℝ
hb : 0 < b
⊢ (∫ (x : ℝ), rexp (-b * x ^ 2)) ^ 2 = √(π / b) ^ 2

Tactic:
← ofReal_inj,

Goal state after:
case inr
b : ℝ
hb : 0 < b
⊢ ↑((∫ (x : ℝ), rexp (-b * x ^ 2)) ^ 2) = ↑(√(π / b) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
f : ℝ → ℂ := fun x ↦ cexp (-b * ↑x ^ 2)
full_integral : (∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)) + ∫ (x : ℝ) in Ioi 0, f x = (↑π / b) ^ (1 / 2)
h_eq : ∫ (x : ℝ) in Iic 0, f x = ∫ (x : ℝ) in Ioi 0, f x
⊢ ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2

Tactic:
← mul_two

Goal state after:
b : ℂ
hb : 0 < b.re
f : ℝ → ℂ := fun x ↦ cexp (-b * ↑x ^ 2)
full_integral : (∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2)) * 2 = (↑π / b) ^ (1 / 2)
h_eq : ∫ (x : ℝ) in Iic 0, f x = ∫ (x : ℝ) in Ioi 0, f x
⊢ ∫ (x : ℝ) in Ioi 0, cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) / 2
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-(r * t)) = (1 / r) ^ a * Gamma a

Tactic:
← ofReal_inj,

Goal state after:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ↑(∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-(r * t))) = ↑((1 / r) ^ a * Gamma a)
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: case e_f.e_a
E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ inner ℝ x (b i) ^ 2
i : Fin (Module.finrank ℝ E)
x : E
⊢ ((fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i))) ((fourierMultiplierCLM F fun x ↦ inner ℝ x (b i)) f)) x =
    ((fourierMultiplierCLM F fun x ↦ inner ℝ x (b i) ^ 2) f) x

Tactic:
· rw [fourierMultiplierCLM_ofReal ℂ (by fun_prop),
      fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]
    simp [sq, Pi.mul_def]

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : RCLike 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : FiniteDimensional ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : CompleteSpace E
⊢ ∀ (f : 𝓢(V, E)), 𝓕 (𝓕⁻ f) = f

Tactic:
by
    intro f
    ext x
    rw [fourier_coe, fourierInv_coe, f.continuous.fourier_fourierInv_eq f.integrable
      (𝓕 f).integrable]

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
⊢ (map (powMonoidHom n) B).IsFiniteRelIndex B

Tactic:
isFiniteRelIndex_iff_finiteIndex

Goal state after:
A : Type u_1
inst✝ : CommGroup A
B : Subgroup A
hB : B.FG
n : ℕ
hn : n ≠ 0
⊢ ((map (powMonoidHom n) B).subgroupOf B).FiniteIndex
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: n : ℕ
⊢ |μ n| = if Squarefree n then 1 else 0

Tactic:
split_ifs with h
  · exact abs_moebius_eq_one_of_squarefree h
  · simp only [moebius_eq_zero_of_not_squarefree h, abs_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + f p) = (ArithmeticFunction.prodPrimeFactors fun p ↦ (↑ζ + f) p) n

Tactic:
simp_rw [prodPrimeFactors_apply hn.ne_zero, add_apply, natCoe_apply]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + f p) = ∏ p ∈ n.primeFactors, (↑(ζ p) + f p)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
h' : k.gcd l < k
⊢ ζ ^ k.gcd l = 1

Tactic:
simp [h1, hl]

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

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
⊢ ζ ^ ↑k = 1

Tactic:
exact_mod_cast h.pow_eq_one

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

Goal state before:
pp: case neg
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I).arg =
    ↑(↑i - ↑n) / ↑n * (2 * Real.pi)

Tactic:
← Complex.cos_sub_two_pi,

Goal state after:
case neg
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (Complex.cos (↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I).arg =
    ↑(↑i - ↑n) / ↑n * (2 * Real.pi)
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⁻¹
int_A : ∫ (v : V), ‖f v - f (v + i w)‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖
⊢ ∫ (v : V) in A, ‖f v - f (v + i w)‖ < 2 * ε

Tactic:
clear int_A

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) in A, ‖f v - f (v + i w)‖ < 2 * ε
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case right
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] := ⋯
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := ⋯
⊢ degree 0 < B.degree

Tactic:
· simpa only [degree_zero, bot_lt_iff_ne_bot, Ne, degree_eq_bot] using Bmo.ne_zero

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

Goal state before:
pp: case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a α : R
hα : α ^ n = a
⊢ (Multiset.map (fun x ↦ ζ ^ x * α) (Multiset.range n)).card = n

Tactic:
Multiset.card_map,

Goal state after:
case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a α : R
hα : α ^ n = a
⊢ (Multiset.range n).card = n
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
⊢ Tendsto (fun x ↦ ∫ (v : V), 𝐞 (-x v) • f v ∂volume) (cocompact (StrongDual ℝ V)) (𝓝 0)

Tactic:
let A := (InnerProductSpace.toDual ℝ V).symm

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
⊢ Tendsto (fun x ↦ ∫ (v : V), 𝐞 (-x v) • f v ∂volume) (cocompact (StrongDual ℝ V)) (𝓝 0)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
h1 : ∃ m, ↑1 ↑↑μ' = ↑↑μ' ^ m
h : μ' ^ 1 = μ' ^ h1.choose
⊢ 1 = ↑1

Tactic:
exact Nat.cast_one.symm

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

Goal state before:
pp: K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
⊢ Basis (Fin (minpoly K x).natDegree) K ↥K[x]

Tactic:
have hST : Function.Injective (algebraMap (K[(x : S)]) S) := Subtype.coe_injective
  have hx' :
    IsIntegral K (⟨x, subset_adjoin (Set.mem_singleton x)⟩ : K[(x : S)]) := by
    apply (isIntegral_algebraMap_iff hST).mp
    convert! hx
  apply Basis.mk (v := fun i : Fin _ ↦ ⟨x, subset_adjoin (Set.mem_singleton x)⟩ ^ (i : ℕ))
  · have : LinearIndependent K _ := linearIndependent_pow
      (⟨x, self_mem_adjoin_singleton _ _⟩ : K[x])
    rwa [← minpoly.algebraMap_eq hST] at this
  · rintro ⟨y, hy⟩ _
    have := hx'.mem_span_pow (y := ⟨y, hy⟩)
    rw [← minpoly.algebraMap_eq hST] at this
    apply this
    rw [adjoin_singleton_eq_range_aeval] at hy
    obtain ⟨f, rfl⟩ := (aeval x).mem_range.mp hy
    use f
    ext
    exact aeval_algebraMap_apply S (⟨x, _⟩ : K[x]) _

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

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = g_poly.natDegree
⊢ Module.finrank (ZMod p) (GaloisField p n) = n

Tactic:
have nat_degree_eq : g_poly.natDegree = p ^ n :=
    FiniteField.X_pow_card_pow_sub_X_natDegree_eq _ h hp

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = g_poly.natDegree
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ Module.finrank (ZMod p) (GaloisField p n) = n
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✝¹ : IsCyclotomicExtension S A B
inst✝ : IsDomain B
f g : B ≃ₐ[A] B
H : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n ∧ f r = g r
x : B
hx : x ∈ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
⊢ f x = g x

Tactic:
induction hx using Algebra.adjoin_induction with
  | mem y hy =>
    obtain ⟨n, hn, h1, h2⟩ := hy
    obtain ⟨r, hr1, hr2⟩ := H n hn h1
    have := NeZero.mk h1
    obtain ⟨m, -, rfl⟩ := hr1.eq_pow_of_pow_eq_one h2
    simp [hr2]
  | algebraMap y => simp
  | add x y hx hy ihx ihy => simp [ihx, ihy]
  | mul x y hx hy ihx ihy => simp [ihx, ihy]

Goal state after:
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
inst✝¹ : IsDomain B
ζ : B
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
x : B
hx : map (algebraMap A B) (cyclotomic n A) ≠ 0 ∧ (aeval x) (cyclotomic n A) = 0
⊢ n ≠ 0 ∧ ∃ i ∈ n.divisors, (cyclotomic i B).IsRoot x

Tactic:
refine ⟨NeZero.ne n, n, Nat.mem_divisors_self n (NeZero.ne n), ?_⟩

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

Goal state before:
pp: case inr
n : ℤ
m : ℕ
h : IsUnit ↑n
hm : m ≠ 0
this : NeZero m
⊢ IsCoprime (↑m) n

Tactic:
obtain ⟨u, hu⟩ := h

Goal state after:
case inr
n : ℤ
m : ℕ
hm : m ≠ 0
this : NeZero m
u : (ZMod m)ˣ
hu : ↑u = ↑n
⊢ IsCoprime (↑m) n
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : Algebra (ZMod p) K
inst✝ : Finite K
this : Fintype K
⊢ (Polynomial.map (algebraMap (ZMod p) K) (X ^ Nat.card K - X)).Splits

Tactic:
rw [Nat.card_eq_fintype_card]

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : Algebra (ZMod p) K
inst✝ : Finite K
this : Fintype K
⊢ (Polynomial.map (algebraMap (ZMod p) K) (X ^ Fintype.card K - X)).Splits
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'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
h₁ : ∑ x, ψ b * ψ x = ∑ a, ψ a
h₂ : ∑ a, ψ a = Finset.univ.sum ⇑ψ
⊢ ∑ a, ψ a = 0

Tactic:
← Finset.mul_sum,

Goal state after:
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
h₁ : ψ b * ∑ i, ψ i = ∑ a, ψ a
h₂ : ∑ a, ψ a = Finset.univ.sum ⇑ψ
⊢ ∑ a, ψ a = 0
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
⊢ CharP K' p

Tactic:
rw [← Algebra.charP_iff (ZMod p) 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
⊢ CharP (ZMod p) p
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case right.inv
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
y x : AlgebraicClosure K
hx : x ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
ihx : f x ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
⊢ f x⁻¹ ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
rw [map_inv₀]
    exact inv_mem ihx

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

Goal state before:
pp: F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Finite L
inst✝ : Finite K
h : Module.finrank F K ∣ Module.finrank F L
⊢ Fintype.card (K →ₐ[F] L) = Module.finrank F K

Tactic:
Fintype.card_eq_nat_card,

Goal state after:
F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Finite L
inst✝ : Finite K
h : Module.finrank F K ∣ Module.finrank F L
⊢ Nat.card (K →ₐ[F] L) = Module.finrank F K
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
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
inst✝ : NeZero ↑n
x✝ : n ≠ 0
this✝ : NeZero ↑n
this : NeZero ↑n
μ : CyclotomicField n K
hμ : IsPrimitiveRoot μ n
⊢ μ ∈ {b | b ^ n = 1}

Tactic:
apply (isRoot_of_unity_iff (NeZero.pos n) (CyclotomicField n K)).mpr

Goal state after:
case refine_1
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
inst✝ : NeZero ↑n
x✝ : n ≠ 0
this✝ : NeZero ↑n
this : NeZero ↑n
μ : CyclotomicField n K
hμ : IsPrimitiveRoot μ n
⊢ ∃ i ∈ n.divisors, (cyclotomic i (CyclotomicField n K)).IsRoot μ
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ y, ∑ x, χ y * ψ (x * (y - 1)) = ↑(Fintype.card R)

Tactic:
← Finset.mul_sum,

Goal state after:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ x, χ x * ∑ i, ψ (i * (x - 1)) = ↑(Fintype.card R)
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s✝ t : Multiset α
a : α
s : Multiset α
hs : IsMin s
⊢ IsMin s.card

Tactic:
rw [isMin_iff_eq_bot.1 hs]; exact isMin_bot

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Function.Odd (𝓕 Φ) ↔ Function.Odd Φ

Tactic:
have h {f : ZMod N → ℂ} (hf : f.Odd) : (𝓕 f).Odd := by
    simp only [Function.Odd, ← congr_fun (dft_comp_neg f), funext hf, ← Pi.neg_apply, map_neg,
      implies_true]
  refine ⟨fun hΦ x ↦ ?_, h⟩
  simpa only [neg_neg, dft_dft, ← smul_neg, smul_right_inj (NeZero.ne (N : ℂ))] using h hΦ (-x)

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

Goal state before:
pp: α : Type u_1
s✝ t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin s.val

Tactic:
rw [isMin_iff_eq_bot.1 hs]; exact isMin_bot

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

Goal state before:
pp: α : Type u_1
s✝ t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin #s

Tactic:
rw [isMin_iff_eq_bot.1 hs]; exact isMin_bot

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
⊢ ∫⁻ (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 ∂μ) x ^ (1 - (↑(#s) - 1) * p) * ∏ x_1 ∈ s, (∫⋯∫⁻_{x_1}, ∫⋯∫⁻_{i}, f ∂μ ∂μ) x ^ p

Tactic:
set X := update x i

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
⊢ ∫⁻ (t : A i), f (X t) ^ (1 - ↑(#s) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p ∂μ i ≤
    (∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - (↑(#s) - 1) * p) * ∏ x_1 ∈ s, (∫⋯∫⁻_{x_1}, ∫⋯∫⁻_{i}, f ∂μ ∂μ) x ^ p
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 : T.IsPositive
c : 𝕜
hc : 0 ≤ c
hc' : (starRingEnd 𝕜) c = c
x : E
⊢ 0 ≤ re c * re ⟪T x, x⟫ - im c * im ⟪T x, x⟫

Tactic:
conj_eq_iff_im.mp hc',

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
c : 𝕜
hc : 0 ≤ c
hc' : (starRingEnd 𝕜) c = c
x : E
⊢ 0 ≤ re c * re ⟪T x, x⟫ - 0 * im ⟪T x, x⟫