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

Goal state before:
pp: case hp
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : ↥(Lp F 2 volume) → Prop := ⋯
⊢ IsClosed {b | p b}

Tactic:
apply isClosed_eq

Goal state after:
case hp.hf
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : ↥(Lp F 2 volume) → Prop := ⋯
⊢ Continuous fun y ↦ 𝓕 (toTemperedDistribution y)

case hp.hg
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : ↥(Lp F 2 volume) → Prop := ⋯
⊢ Continuous fun y ↦ toTemperedDistribution (𝓕 y)
Module: Mathlib.Analysis.Fourier.Convolution

Goal state before:
pp: case e_f
𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedAddCommGroup F₂
inst✝⁸ : NormedAddCommGroup F₃
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedSpace 𝕜 F₁
inst✝² : NormedSpace 𝕜 F₂
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℂ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
ξ x : E
⊢ 𝐞 (-inner ℝ x ξ) • ∫ (y : E), (B (f₁ (x - y))) (f₂ y) = ∫ (y : E), 𝐞 (-inner ℝ x ξ) • (B (f₁ (x - y))) (f₂ y)

Tactic:
simp_rw [Circle.smul_def, integral_smul]

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
⊢ (powMonoidHom n).range.FiniteIndex

Tactic:
have := (Group.fg_iff_subgroup_fg B).mpr hB

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
this : Group.FG ↥B
⊢ (powMonoidHom n).range.FiniteIndex
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ), e x * f x = 𝓕 ⇑f ↑m

Tactic:
rw [fourier_real_eq_integral_exp_smul]
      congr 1 with x : 1
      rw [smul_eq_mul, comp_apply, coe_mk, coe_mk, ContinuousMap.toFun_eq_coe, fourier_coe_apply]
      congr 2
      push_cast
      ring

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Periodic

Goal state before:
pp: case e'_2
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n ↦ f.comp (ContinuousMap.addRight (n • p))
this : Summable fun c ↦ f.comp (ContinuousMap.addRight ((Equiv.addRight 1) c • p))
⊢ ∑' (i : ℤ), (f.comp (ContinuousMap.addRight (i • p))) (x + p) =
    ∑' (i : ℤ), (f.comp (ContinuousMap.addRight ((Equiv.addRight 1) i • p))) x

Tactic:
simp [Equiv.coe_addRight, comp_apply, add_one_zsmul, add_comm (_ • p) p, ← add_assoc]

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

Goal state before:
pp: case neg
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ ζ ^ (↑i * i.gcdA k * ↑l) * (ζ ^ (↑k * i.gcdB k)) ^ l = 1

Tactic:
mul_right_comm

Goal state after:
case neg
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ ζ ^ (↑i * ↑l * i.gcdA k) * (ζ ^ (↑k * i.gcdB k)) ^ l = 1
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case right
i : ℤ
n : ℕ
h0 : n ≠ 0
hi : IsCoprime i ↑n
⊢ ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l

Tactic:
· simp only [forall_exists_index]
    have hn0 : (n : ℂ) ≠ 0 := mod_cast h0
    rintro l k hk
    field_simp at hk
    norm_cast at hk
    exact Int.natCast_dvd_natCast.mp <| hi.symm.dvd_of_dvd_mul_right <| hk ▸ dvd_mul_right ..

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (cyclotomic n ℤ).degree = ↑n.totient

Tactic:
rcases n with - | k

Goal state after:
case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (cyclotomic 0 ℤ).degree = ↑(Nat.totient 0)

case succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
k : ℕ
⊢ (cyclotomic (k + 1) ℤ).degree = ↑(k + 1).totient
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
hpos : 0 < n
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ 0 < (cyclotomic n R).degree

Tactic:
rwa [degree_cyclotomic n R, Nat.cast_pos, Nat.totient_pos]

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✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
⊢ Tendsto (fun w ↦ ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (StrongDual ℝ V)) (𝓝 0)

Tactic:
have A : V ≃L[ℝ] V' := toEuclidean

Goal state after:
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
⊢ Tendsto (fun w ↦ ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (StrongDual ℝ V)) (𝓝 0)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case h.inl.hb.inl
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
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hk : Odd n
⊢ 0 ≤ eval x (cyclotomic i R)

Tactic:
refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 ?_)).le <;> rintro rfl

Goal state after:
case h.inl.hb.inl.refine_1
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
hk : Odd n
hi : 0 ≠ 1 ∧ 0 ∣ n ∧ 0 < n
⊢ False

case h.inl.hb.inl.refine_2
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
hk : Odd n
hi : 2 ≠ 1 ∧ 2 ∣ n ∧ 2 < n
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic n (ZMod p) * cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) * cyclotomic n (ZMod p) ^ (p - 1)

Tactic:
rw [← pow_succ', tsub_add_cancel_of_le hp.out.one_lt.le, mul_comm, ← ZMod.expand_card]

Goal state after:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) * cyclotomic n (ZMod p) = (expand (ZMod p) p) (cyclotomic n (ZMod p))
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
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)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : (algebraMap B C) b ∈ adjoin A (⇑f '' {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
⊢ (algebraMap B C) b ∈ adjoin A {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}

Tactic:
refine adjoin_mono (fun y hy => ?_) hb

Goal state after:
case refine_2
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)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : (algebraMap B C) b ∈ adjoin A (⇑f '' {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
y : C
hy : y ∈ ⇑f '' {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}
⊢ y ∈ {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case inr
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : GCDMonoid.lcm l n = 2 * n
ineq : φ n * φ r ≤ φ (GCDMonoid.lcm l n)
rpos : 0 < r
key : r = 2
⊢ l ∣ 2 * n

Tactic:
simpa [← hr] using _root_.dvd_lcm_left _ _

Goal state after:
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 = 1 ^ n
⊢ (Algebra.norm K) ζ = 1

Tactic:
exact StrictMono.injective hodd.strictMono_pow hz

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

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n

Tactic:
by
  have hn : 0 < n := pos_of_gt hn'
  have hq := zero_lt_one.trans hq'
  have hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1 := by
    intro ζ' hζ'
    rw [mem_primitiveRoots hn] at hζ'
    convert! norm_sub_le (↑q) ζ'
    · rw [Complex.norm_real, Real.norm_of_nonneg (zero_le_one.trans_lt hq').le]
    · rw [hζ'.norm'_eq_one hn.ne']
  let ζ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
  have hζ : IsPrimitiveRoot ζ n := Complex.isPrimitiveRoot_exp n hn.ne'
  have hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1 := by
    refine ⟨ζ, (mem_primitiveRoots hn).mpr hζ, ?_⟩
    suffices ¬SameRay ℝ (q : ℂ) (-ζ) by
      convert! norm_add_lt_of_not_sameRay this using 2
      · rw [Complex.norm_real]
        symm
        exact abs_eq_self.mpr hq.le
      · simp [hζ.norm'_eq_one hn.ne']
    rw [Complex.sameRay_iff]
    push Not
    refine ⟨mod_cast hq.ne', neg_ne_zero.mpr <| hζ.ne_zero hn.ne', ?_⟩
    rw [Complex.arg_ofReal_of_nonneg hq.le, Ne, eq_comm]
    intro h
    rw [Complex.arg_eq_zero_iff, Complex.neg_re, neg_nonneg, Complex.neg_im, neg_eq_zero] at h
    have hζ₀ : ζ ≠ 0 := by
      clear_value ζ
      rintro rfl
      exact hn.ne' (hζ.unique IsPrimitiveRoot.zero)
    have : ζ.re < 0 ∧ ζ.im = 0 := ⟨h.1.lt_of_ne ?_, h.2⟩
    · rw [← Complex.arg_eq_pi_iff, hζ.arg_eq_pi_iff hn.ne'] at this
      rw [this] at hζ
      linarith [hζ.unique <| IsPrimitiveRoot.neg_one 0 two_ne_zero.symm]
    · contrapose hζ₀
      apply Complex.ext <;> simp [hζ₀, h.2]
  have : ¬eval (↑q) (cyclotomic n ℂ) = 0 := by simpa using (cyclotomic_pos' n hq').ne.symm
  suffices Units.mk0 ‖(cyclotomic n ℂ).eval ↑q‖₊ (by simp_all) <
      Units.mk0 (Real.toNNReal (q + 1)) (by simp; linarith) ^ totient n by
    simp only [← Units.val_lt_val, Units.val_pow_eq_pow_val, Units.val_mk0, ← NNReal.coe_lt_coe,
      coe_nnnorm, NNReal.coe_pow,
      Real.coe_toNNReal'] at this
    convert! this using 2
    · rw [eq_comm]
      simp [cyclotomic_nonneg n hq'.le]
    rw [eq_comm, max_eq_left_iff]
    linarith
  simp only [cyclotomic_eq_prod_X_sub_primitiveRoots hζ, eval_prod, eval_C, eval_X, eval_sub,
    nnnorm_prod, Units.mk0_prod]
  convert! Finset.prod_lt_prod' (M := NNRealˣ) _ _
  swap; · exact fun _ => Units.mk0 (Real.toNNReal (q + 1)) (by positivity)
  · simp [Complex.card_primitiveRoots]
  · simp only [Finset.mem_attach, forall_true_left, Subtype.forall, ←
      Units.val_le_val, ← NNReal.coe_le_coe, Units.val_mk0,
      coe_nnnorm]
    intro x hx
    have : ‖_‖ ≤ _ := hfor x hx
    simp [this]
  · simp only [Finset.mem_attach, Subtype.exists, ←
      NNReal.coe_lt_coe, ← Units.val_lt_val, Units.val_mk0 _, coe_nnnorm]
    obtain ⟨ζ, hζ, hhζ : ‖_‖ < _⟩ := hex
    exact ⟨ζ, hζ, by simp [hhζ]⟩

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ adjoin A ((cyclotomic n A).rootSet B) = A[ζ]

Tactic:
refine le_antisymm (adjoin_le fun x hx => ?_) (adjoin_mono fun x hx => ?_)
  · suffices hx : x ^ n = 1 by
      obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx
      exact SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin <| mem_singleton ζ) _)
    refine (isRoot_of_unity_iff (NeZero.pos n) B).2 ?_
    refine ⟨n, Nat.mem_divisors_self n (NeZero.ne n), ?_⟩
    rw [mem_rootSet', ← eval_map_algebraMap, map_cyclotomic, ← IsRoot] at hx
    exact hx.2
  · simp only [mem_singleton_iff] at hx
    simpa only [hx, mem_rootSet', map_cyclotomic, ← eval_map_algebraMap, IsRoot] using
      And.intro (cyclotomic_ne_zero n B) (hζ.isRoot_cyclotomic (NeZero.pos n))

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

Goal state before:
pp: case inl
K : Type u_1
inst✝ : Field K
val✝ : Fintype K
⊢ (X ^ Nat.card K - X).Splits

Tactic:
have := (IsSplittingField.splits (L := K) (X ^ (Fintype.card K) - X : K[X]))

Goal state after:
case inl
K : Type u_1
inst✝ : Field K
val✝ : Fintype K
this : (Polynomial.map (algebraMap K K) (X ^ Fintype.card K - X)).Splits
⊢ (X ^ Nat.card K - X).Splits
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
x : CyclotomicField 0 K
this : IsSplittingField K K (cyclotomic 0 K)
⊢ finrank K (CyclotomicField 0 K) = 1

Tactic:
let e : K ≃ₗ[K] (CyclotomicField 0 K) :=
        (Polynomial.IsSplittingField.algEquiv K (Polynomial.cyclotomic 0 K)).toLinearEquiv

Goal state after:
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
x : CyclotomicField 0 K
this : IsSplittingField K K (cyclotomic 0 K)
e : K ≃ₗ[K] CyclotomicField 0 K := ↑(IsSplittingField.algEquiv K (cyclotomic 0 K))
⊢ finrank K (CyclotomicField 0 K) = 1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
x y : R
⊢ (if IsUnit x ∧ IsUnit y then 1 else 0) = if IsUnit x then if IsUnit y then 1 else 0 else 0

Tactic:
split_ifs <;> tauto

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
⊢ R → R'

Tactic:
by classical exact fun x => if hx : IsUnit x then f hx.unit else 0

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ ∀ (x y : MulChar R R'), equivToUnitHom.toFun (x * y) = equivToUnitHom.toFun x * equivToUnitHom.toFun y

Tactic:
by
      intro χ ψ
      ext
      simp only [Equiv.toFun_as_coe, coe_equivToUnitHom, coeToFun_mul, Pi.mul_apply,
        MonoidHom.mul_apply, Units.val_mul]

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

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

Tactic:
have : NeZero (conductor (1 : DirichletCharacter R n)) :=
    ⟨@conductor_one R _ n _ ▸ Nat.one_ne_zero⟩
  rw [eq_one_iff_conductor_eq_one,
    (isPrimitive_def _).1 (1 : DirichletCharacter R n).primitiveCharacter_isPrimitive,
    conductor_one]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℤ
hn : NeZero n
⊢ χ ^ m = (changeLevel ⋯) (χ.primitiveCharacter ^ m)

Tactic:
MonoidHom.map_zpow,

Goal state after:
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℤ
hn : NeZero n
⊢ χ ^ m = (changeLevel ⋯) χ.primitiveCharacter ^ m
Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
u : (ZMod N)ˣ
hu : (ZMod.unitsMap hd) u = 1
⊢ χ ↑u * gaussSum χ e = gaussSum χ e

Tactic:
suffices e.mulShift u = e by conv_lhs => rw [← this, gaussSum_mulShift]

Goal state after:
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
u : (ZMod N)ˣ
hu : (ZMod.unitsMap hd) u = 1
⊢ e.mulShift ↑u = e
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F : IntermediateField K L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension {n} K ↥F ↔ F.toSubalgebra = K[ζ]

Tactic:
exact _root_.isCyclotomicExtension_singleton_iff_eq_adjoin n F.toSubalgebra hζ

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case inr
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'
b : R
hb : b ≠ 0
⊢ ∑ a, χ (a * b⁻¹) * ψ (a - b) = ∑ c, χ c * ψ (b * (c - 1))

Tactic:
· -- case `b ≠ 0`
    refine (Fintype.sum_bijective _ (mulLeft_bijective₀ b hb) _ _ fun x ↦ ?_).symm
    rw [mul_assoc, mul_comm x, ← mul_assoc, mul_inv_cancel₀ hb, one_mul, mul_sub, mul_one]

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‖ ^ p) = fun x ↦ ‖x‖ * ‖x‖ ^ (p - 1)

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

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

Tactic:
by
          -- unfold `T` and reformulate the exponents
          simp_rw [T, card_insert_of_notMem hi]
          congr!
          push_cast
          ring

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) = x • (adjoint counit) y

Tactic:
← _root_.map_smul

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) = (adjoint counit) (x • y)
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) = (adjoint counit) x * (adjoint counit) y

Tactic:
simp_rw [AlgebraOfCoalgebra.mul_def, ← map_tmul, ← adjoint_map, ← comp_apply,
          ← adjoint_comp, ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul,
          adjoint_comp, ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm,
          adjoint_toLinearMap_eq_symm]
        simp only [LinearIsometryEquiv.symm_symm, toLinearEquiv_lidIsometry, adjoint_lTensor,
          coe_comp, LinearEquiv.coe_coe, Function.comp_apply, lTensor_tmul, lid_tmul]
        rw [← smul_eq_mul, ← _root_.map_smul]

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

Goal state before:
pp: case inr
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h✝ : Nonempty ((i : ι) → A i)
inhabited_h : Inhabited ((i : ι) → A i)
H : ∅ ⊆ Finset.univ
⊢ ∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑#ι - 1) * p) * ∏ i, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)

Tactic:
simpa [lmarginal_univ] using GridLines.T_lmarginal_antitone μ hp₀ hp hf H default

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric (T i)
hC : Pairwise (Commute on T)
⊢ (⨆ α, ⨅ j, (T j).eigenspace (α j))ᗮ = ⊥

pp: 𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric (T i)
hC : Pairwise (Commute on T)
⊢ OrthogonalFamily 𝕜 (fun i ↦ ↥(⨅ j, (T j).eigenspace (i j))) fun i ↦ (⨅ j, (T j).eigenspace (i j)).subtypeₗᵢ

Tactic:
· rw [iSup_iInf_eq_top_of_commute hT hC, top_orthogonal_eq_bot]

Goal state after:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric (T i)
hC : Pairwise (Commute on T)
⊢ OrthogonalFamily 𝕜 (fun i ↦ ↥(⨅ j, (T j).eigenspace (i j))) fun i ↦ (⨅ j, (T j).eigenspace (i j)).subtypeₗᵢ