mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case e'_3
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 : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
this✝ : MemLp (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume
this : MemLp (fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))) 2 volume
x : E
⊢ ((fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) * fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))) x = 1

Tactic:
Pi.mul_apply

Goal state after:
case e'_3
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 : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
this✝ : MemLp (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume
this : MemLp (fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))) 2 volume
x : E
⊢ ↑((1 + ‖x‖ ^ 2) ^ (s / 2)) * ↑((1 + ‖x‖ ^ 2) ^ (-s / 2)) = 1
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
f : α → ℂ := fun b ↦ if a = b then 1 else 0
h₀ : (∑ i, ((complexBasis α).repr f) i • (complexBasis α) i) 0 = f 0
h₁ : (∑ i, ((complexBasis α).repr f) i • (complexBasis α) i) a = f a
⊢ False

Tactic:
simp only [complexBasis_apply, Fintype.sum_apply, Pi.smul_apply, h, smul_eq_mul, mul_one,
    map_zero_eq_one, if_pos rfl, if_neg ha, f] at h₀ h₁

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
f : α → ℂ := fun b ↦ if a = b then 1 else 0
h₀ : ∑ x, ((complexBasis α).repr fun b ↦ if a = b then 1 else 0) x = 0
h₁ : ∑ x, ((complexBasis α).repr fun b ↦ if a = b then 1 else 0) x = 1
⊢ False
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
w : V
hw : w ≠ 0
⊢ (starRingEnd ℝ) (1 / (2 * ‖w‖ ^ 2)) * ‖w‖ ^ 2 = 1 / 2

Tactic:
RCLike.conj_to_real,

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
w : V
hw : w ≠ 0
⊢ 1 / (2 * ‖w‖ ^ 2) * ‖w‖ ^ 2 = 1 / 2
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

pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ (ArithmeticFunction.prodPrimeFactors fun p ↦ (↑ζ + f) p) n = ∑ d ∈ n.divisors, f d

Tactic:
· simp_rw [prodPrimeFactors_apply hn.ne_zero, add_apply, natCoe_apply]
    apply prod_congr rfl; intro p hp
    rw [zeta_apply_ne (prime_of_mem_primeFactorsList <| List.mem_toFinset.mp hp).ne_zero, cast_one]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ (ArithmeticFunction.prodPrimeFactors fun p ↦ (↑ζ + f) p) n = ∑ d ∈ n.divisors, f d
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:
rw [zsmul_eq_mul]

Goal state after:
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
⊢ (∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) → ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
intro h
    let G := fun (n : ℕ) => (∑ i ∈ n.divisors, f i)
    intro n hn hnP
    suffices ∑ d ∈ n.divisors, μ (n / d) • G d = f n by
      rw [sum_divisorsAntidiagonal' (f := fun x y => μ x • g y), ← this, sum_congr rfl]
      intro d hd
      rw [← h d (pos_of_mem_divisors hd) <| hs d n (dvd_of_mem_divisors hd) hnP]
    rw [← sum_divisorsAntidiagonal' (f := fun x y => μ x • G y)]
    apply sum_eq_iff_sum_smul_moebius_eq.mp _ n hn
    intro _ _; rfl

Goal state after:
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:
rw [zsmul_eq_mul]

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

Goal state before:
pp: case left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖ ≤ ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf : (⇑f =O[atBot] fun x ↦ |x| ^ (-b)) ∧ ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
⊢ (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[atBot] fun x ↦ |x| ^ (-b)

Tactic:
refine (isBigO_of_le atBot ?_).trans (isBigO_norm_Icc_restrict_atBot hb hf.1 (-r) r)
    simp_rw [norm_norm]; exact this

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (X ^ n - C 1).Monic
⊢ (nthRoots n 1).card = n

Tactic:
exact IsPrimitiveRoot.card_nthRoots_one h

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

Goal state before:
pp: case e_f
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
w : StrongDual ℝ V
v : V
⊢ 𝐞 (-w v) • f v = 𝐞 (-(starRingEnd ℝ) ⟪A w, v⟫) • f v

Tactic:
RCLike.conj_to_real,

Goal state after:
case e_f
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
w : StrongDual ℝ V
v : V
⊢ 𝐞 (-w v) • f v = 𝐞 (-⟪A w, v⟫) • f v
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : (cyclotomic n K).IsRoot μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
this : μ ^ orderOf μ = 1
⊢ False

Tactic:
rw [isRoot_of_unity_iff ho] at this

Goal state after:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : (cyclotomic n K).IsRoot μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
this : ∃ i ∈ (orderOf μ).divisors, (cyclotomic i K).IsRoot μ
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
⊢ cyclotomic p ℚ ∣ P ↔ ∀ (i j : Fin p), α i = α j

Tactic:
refine ⟨fun ⟨c, hc⟩ ↦ ?_, fun H ↦ ⟨C (α 0), Polynomial.ext fun i ↦ if h : i < p then ?_ else ?_⟩⟩

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
x✝ : cyclotomic p ℚ ∣ P
c : ℚ[X]
hc : P = cyclotomic p ℚ * c
⊢ ∀ (i j : Fin p), α i = α j

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
H : ∀ (i j : Fin p), α i = α j
i : ℕ
h : i < p
⊢ P.coeff i = (cyclotomic p ℚ * C (α 0)).coeff i

case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
H : ∀ (i j : Fin p), α i = α j
i : ℕ
h : ¬i < p
⊢ P.coeff i = (cyclotomic p ℚ * C (α 0)).coeff i
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case e'_3
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
⊢ ∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y) = eval (x / y) (∏ ζ ∈ nthRootsFinset n 1, (X - C ζ)) * y ^ #(nthRootsFinset n 1)

Tactic:
simp [eval_prod, prod_mul_pow_card, sub_mul, hy]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
⊢ ∏ ζ ∈ nthRootsFinset n 1, ((algebraMap R K) x - ζ * (algebraMap R K) y) =
    ∏ x_1 ∈ nthRootsFinset n 1, ((algebraMap R K) x - (algebraMap R K) x_1 * (algebraMap R K) y)

Tactic:
refine (prod_nbij (algebraMap R K) (fun a ha ↦ map_mem_nthRootsFinset_one ha _)
    (fun a _ b _ H ↦ FaithfulSMul.algebraMap_injective R K H) (fun a ha ↦ ?_) (fun _ _ ↦ rfl)).symm

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
a : K
ha : a ∈ ↑(nthRootsFinset n 1)
⊢ a ∈ ⇑(algebraMap R K) '' ↑(nthRootsFinset n 1)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn : n✝ ∈ S ∪ T
hn' : n✝ ≠ 0
⊢ ∃ r, IsPrimitiveRoot r n✝

Tactic:
rcases hn with hn | hn

Goal state after:
case refine_1.inl
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn' : n✝ ≠ 0
hn : n✝ ∈ S
⊢ ∃ r, IsPrimitiveRoot r n✝

case refine_1.inr
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn' : n✝ ≠ 0
hn : n✝ ∈ T
⊢ ∃ r, IsPrimitiveRoot r n✝
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
L : Type v
inst✝⁴ : CommRing L
ζ : L
hζ : IsPrimitiveRoot ζ n
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Algebra K L
hodd : Odd n
hz : (Algebra.norm K) (ζ ^ n) = (Algebra.norm K) 1
⊢ (Algebra.norm K) ζ = 1

Tactic:
rw [← (algebraMap K L).map_one, Algebra.norm_algebraMap, one_pow, map_pow, ← one_pow n] at hz

Goal state after:
n : ℕ
L : Type v
inst✝⁴ : CommRing L
ζ : L
hζ : IsPrimitiveRoot ζ n
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Algebra K L
hodd : Odd n
hz : (Algebra.norm K) ζ ^ n = 1 ^ n
⊢ (Algebra.norm K) ζ = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : Units.mk0 (q - 1).toNNReal ⋯ ^ φ n < Units.mk0 ‖eval (↑q) (cyclotomic n ℂ)‖₊ ⋯
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)

Tactic:
simp only [← Units.val_lt_val, Units.val_pow_eq_pow_val, Units.val_mk0, ← NNReal.coe_lt_coe,
      hq'.le, coe_nnnorm, NNReal.coe_pow, Real.coe_toNNReal', sub_nonneg, sup_of_le_left] at this
    convert! this
    rw [eq_comm]
    simp [cyclotomic_nonneg n hq'.le]

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

Goal state before:
pp: case refine_1
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
⊢ η ∈ K⟮η + 1⟯

Tactic:
nth_rw 2 [← add_sub_cancel_right η 1]
        exact sub_mem (IntermediateField.mem_adjoin_simple_self K (η + 1)) (one_mem _)

Goal state after:
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
inst✝ : IsCyclotomicExtension S K L
this : Algebra.IsIntegral K L
h : (IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}).toSubalgebra = ⊤.toSubalgebra
⊢ Algebra.IsSeparable K L

Tactic:
rw [← AlgEquiv.Algebra.isSeparable_iff <|
    (IntermediateField.equivOfEq (IntermediateField.toSubalgebra_injective h)).trans
      IntermediateField.topEquiv, IntermediateField.isSeparable_adjoin_iff_isSeparable]

Goal state after:
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
this : Algebra.IsIntegral K L
h : (IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}).toSubalgebra = ⊤.toSubalgebra
⊢ ∀ x ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}, IsSeparable K x
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
hpri : Fact (Nat.Prime p)
hcyc : IsCyclotomicExtension {p} K L
h : p ≠ 2
hirr : Irreducible (cyclotomic (p ^ (0 + 1)) K)
hζ : IsPrimitiveRoot ζ (p ^ (0 + 1))
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
⊢ (Algebra.norm K) (ζ - 1) = ↑p

Tactic:
simpa using norm_sub_one_of_prime_ne_two hζ hirr h

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
z : ↥(rootsOfUnity n ℂ)
⊢ (rootsOfUnitytoCircle n).toHomUnits z ∈ rootsOfUnity n Circle

Tactic:
rw [mem_rootsOfUnity', MonoidHom.coe_toHomUnits, ← map_pow, ← (rootsOfUnitytoCircle n).map_one]

Goal state after:
n : ℕ
inst✝ : NeZero n
z : ↥(rootsOfUnity n ℂ)
⊢ (rootsOfUnitytoCircle n) (z ^ n) = (rootsOfUnitytoCircle n) 1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
a : Rˣ
⊢ (⇑χ₁ * ⇑χ₂) ↑a = χ₁ ↑a * χ₂ ↑a

Tactic:
Pi.mul_apply

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

Goal state before:
pp: n : ℕ
inst✝⁸ : NeZero n
S✝ T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSepClosed K
inst✝ : CharZero K
S : Set ℕ
⊢ IsCyclotomicExtension S K K

Tactic:
by
  rw [IsCyclotomicExtension.eq_self_sdiff_zero]
  exact IsSepClosed.isCyclotomicExtension _ K fun _ _ h ↦ ⟨Nat.cast_ne_zero.mpr h⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R 1
⊢ χ = 1

Tactic:
by
  ext
  simp [Units.eq_one]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
inst✝ : NeZero n
this : NeZero (conductor 1)
⊢ primitiveCharacter 1 = 1

Tactic:
eq_one_iff_conductor_eq_one,

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
inst✝ : NeZero n
this : NeZero (conductor 1)
⊢ (primitiveCharacter 1).conductor = 1
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
⊢ gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = ↑(Fintype.card R)

Tactic:
simp only [gaussSum, AddChar.inv_apply, Finset.sum_mul, Finset.mul_sum, MulChar.inv_apply']
  conv =>
    enter [1, 2, x, 2, y]
    rw [mul_mul_mul_comm, ← map_mul, ← map_add_eq_mul, ← sub_eq_add_neg]
--  conv in _ * _ * (_ * _) => rw [mul_mul_mul_comm, ← map_mul, ← map_add_eq_mul, ← sub_eq_add_neg]
  simp_rw [gaussSum_mul_aux hχ ψ]
  rw [Finset.sum_comm]
  classical -- to get `[DecidableEq R]` for `sum_mulShift`
  simp_rw [← Finset.mul_sum, sum_mulShift _ hψ, sub_eq_zero, apply_ite, Nat.cast_zero, mul_zero]
  rw [Finset.sum_ite_eq' Finset.univ (1 : R)]
  simp only [Finset.mem_univ, map_one, one_mul, if_true]

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
⊢ (fun x ↦ x) =O[𝓝 0] fun x ↦ x

Tactic:
isBigO_refl

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

Goal state before:
pp: case pos.mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
u : Finset α
hut : u ⊆ t
⊢ s ⊆ u ∪ s ∧ u ∪ s ⊆ t

Tactic:
exact ⟨subset_union_right, union_subset hut hst⟩

Goal state after:
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
hT' : T ≠ 0
α : 𝕜
h : (α • T).IsPositive
x : E
hx : 0 < ⟪x, T x⟫
⊢ ?m.78

Tactic:
simpa [inner_smul_right] using h.inner_nonneg_right x

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

Goal state before:
pp: case refine_2
𝕜 : 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
⊢ Disjoint q (qᗮ ⊓ p)

Tactic:
simp [disjoint_iff, ← inf_assoc, Submodule.inf_orthogonal_eq_bot q]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
⊢ [(↑p).rangeᗮ = (↑p).ker, IsStarNormal p, IsSelfAdjoint p, p.IsPositive].TFAE

Tactic:
by
  tfae_have 2 ↔ 3 := hp.isSelfAdjoint_iff_isStarNormal.symm
  tfae_have 3 ↔ 4 := hp.isPositive_iff_isSelfAdjoint.symm
  tfae_have 3 ↔ 1 := p.isSelfAdjoint_iff_isSymmetric.eq ▸
    (LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range hp.toLinearMap)
  tfae_finish

Goal state after:
Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace X
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}
x y : X
h : edist x y < δ
n : ℕ
⊢ (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) / ↑n ≤ (∑ _k ∈ Finset.range n, ε) / ↑n

Tactic:
by
      gcongr
      refine hδε _ _ ?_
      simpa using (hf.iterate _).edist_le_mul_of_le h.le

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

Goal state before:
pp: case e'_4.e'_5
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p' : ℝ≥0
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
n' : ℝ≥0 := (↑n).conjExponent
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hp : 1 ≤ 1
hp' : (↑p')⁻¹ = ↑1⁻¹ - (↑n)⁻¹
h2p : ↑1 < ↑n
hnp : 0 < ↑n - ↑1
⊢ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑1) = ↑(eLpNormLESNormFDerivOneConst μ ↑n')

Tactic:
· norm_cast
      simp_rw [n', n, eLpNormLESNormFDerivOfEqInnerConst]
      simp only [n, NNReal.coe_one] at hnp
      field_simp
      simp

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

Goal state before:
pp: case neg.inl
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p' : ℝ≥0
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
n' : ℝ≥0 := (↑n).conjExponent
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hp : 1 ≤ 1
hp' : (↑p')⁻¹ = ↑1⁻¹ - (↑n)⁻¹
h2p : ↑1 < ↑n
hnp : 0 < ↑n - ↑1
⊢ eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑1) * eLpNorm (fderiv ℝ u) (↑1) μ

pp: case neg.inr
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
⊢ eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
· convert! eLpNorm_le_eLpNorm_fderiv_one μ hu h2u hn using 2
    · suffices (p' : ℝ) = n' by simpa using this
      rw [← inv_inj, hp']
      simp [field, n', NNReal.conjExponent, *]
    · norm_cast
      simp_rw [n', n, eLpNormLESNormFDerivOfEqInnerConst]
      simp only [n, NNReal.coe_one] at hnp
      field_simp
      simp

Goal state after:
case neg.inr
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
⊢ eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ