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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
hL : Continuous fun p ↦ (L p.1) p.2
f : V →ᵇ ℂ
⊢ f ∈ (charAlgHom he hL).range ↔ ∃ w, ⇑f = fun x ↦ w.coeff.sum fun a z ↦ z * ↑(e ((L x) a))

Tactic:
simp [BoundedContinuousFunction.ext_iff, funext_iff, eq_comm]

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)
𝕝 : Type u_5
inst✝⁶ : CommSemiring 𝕝
inst✝⁵ : StarRing 𝕝
inst✝⁴ : Algebra 𝕝 𝕜
inst✝³ : StarModule 𝕝 𝕜
inst✝² : SMulCommClass ℝ 𝕝 𝕜
inst✝¹ : (i : ι) → Module 𝕝 (E i)
inst✝ : ∀ (i : ι), IsScalarTower 𝕝 𝕜 (E i)
c : 𝕝
w : ι → ℝ
f g : (i : ι) → E i
⊢ ∑ x, w x • (starRingEnd 𝕝) c • ⟪f x, g x⟫_𝕜 = star c • ∑ i, w i • ⟪f i, g i⟫_𝕜

Tactic:
starRingEnd_apply,

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)
𝕝 : Type u_5
inst✝⁶ : CommSemiring 𝕝
inst✝⁵ : StarRing 𝕝
inst✝⁴ : Algebra 𝕝 𝕜
inst✝³ : StarModule 𝕝 𝕜
inst✝² : SMulCommClass ℝ 𝕝 𝕜
inst✝¹ : (i : ι) → Module 𝕝 (E i)
inst✝ : ∀ (i : ι), IsScalarTower 𝕝 𝕜 (E i)
c : 𝕝
w : ι → ℝ
f g : (i : ι) → E i
⊢ ∑ x, w x • star c • ⟪f x, g x⟫_𝕜 = star c • ∑ i, w i • ⟪f i, g i⟫_𝕜
Module: Mathlib.Analysis.RCLike.Inner

Goal state before:
pp: ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ ↦ ⟪f k₁, f k₂⟫ₙ_[𝕜] = 0
h✝ : Nonempty ι
⊢ Pairwise fun k₁ k₂ ↦ ⟪f k₁, f k₂⟫_[𝕜] = 0

Tactic:
simpa [wInner_cWeight_eq_smul_wInner_one, ← NNRat.cast_smul_eq_nnqsmul 𝕜] using hinner

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

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : Module.Finite ℤ R
A B : Submodule R K
n : ℕ
hn : n ≠ 0
hfg : A.FG
h : ∀ ⦃x : K⦄, x ∈ map (LinearMap.mulLeft R ↑n) A → x ∈ B
this✝ : A.toAddSubgroup.FG
this : (AddSubgroup.map (nsmulAddMonoidHom n) A.toAddSubgroup).IsFiniteRelIndex A.toAddSubgroup
⊢ ∀ ⦃x : K⦄, x ∈ AddSubgroup.map (nsmulAddMonoidHom n) A.toAddSubgroup → x ∈ B.toAddSubgroup

Tactic:
simpa using h

Goal state after:
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case h
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 s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
x : E
⊢ ‖↑((1 + ‖x‖ ^ 2) ^ ((s' - s) / 2))‖ ≤ 1

Tactic:
Complex.norm_real,

Goal state after:
case h
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 s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
x : E
⊢ ‖(1 + ‖x‖ ^ 2) ^ ((s' - s) / 2)‖ ≤ 1
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
⊢ ⟪i w, w⟫ = 1 / 2

Tactic:
rw [inner_smul_left, inner_self_eq_norm_sq_to_K, RCLike.ofReal_real_eq_id, id,
      RCLike.conj_to_real, ← div_div, div_mul_cancel₀]

Goal state after:
case h
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
⊢ ‖w‖ ^ 2 ≠ 0
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n k : ℕ+
⊢ k.Coprime n → (m * k).gcd n = m.gcd n

Tactic:
rw [mul_comm]; apply Coprime.gcd_mul_left_cancel

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

Goal state before:
pp: 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 : ℝ
⊢ ∀ (x_1 : ↑↑K),
    ‖(ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))) x_1‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖

Tactic:
rintro ⟨y, hy⟩

Goal state after:
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
⊢ ‖(ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))) ⟨y, hy⟩‖ ≤
    ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
⊢ i = j

Tactic:
by
  wlog hij : i ≤ j generalizing i j
  · exact (this hj hi H.symm (le_of_not_ge hij)).symm
  apply le_antisymm hij
  rw [← tsub_eq_zero_iff_le]
  apply Nat.eq_zero_of_dvd_of_lt _ (lt_of_le_of_lt tsub_le_self hj)
  apply h.dvd_of_pow_eq_one
  rw [← ((h.isUnit (Nat.ne_zero_of_lt hi)).pow i).mul_left_inj, ← pow_add,
    tsub_add_cancel_of_le hij, H, one_mul]

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

Goal state before:
pp: n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i ∈ n.divisors.erase 1, cyclotomic i R = ∑ i ∈ range n, X ^ i

Tactic:
suffices (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) = ∑ i ∈ Finset.range n, X ^ i by
    simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow,
      Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) this

Goal state after:
n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ = ∑ i ∈ range n, X ^ i
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))
A : V ≃L[ℝ] V'
⊢ Tendsto (fun w ↦ ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (StrongDual ℝ V)) (𝓝 0)

Tactic:
borelize V'

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'
this✝¹ : MeasurableSpace V' := borel V'
this✝ : BorelSpace V'
⊢ Tendsto (fun w ↦ ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (StrongDual ℝ V)) (𝓝 0)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
m : ℕ
hnm : cyclotomic 0 R = cyclotomic m R
⊢ 0 = m

Tactic:
rw [cyclotomic_zero] at hnm

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
m : ℕ
hnm : 1 = cyclotomic m R
⊢ 0 = m
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

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

Tactic:
simpa using h

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

Goal state before:
pp: R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
x✝ : 0 < 1
⊢ cyclotomic (p * m) R = cyclotomic m R ^ (p - p ^ (1 - 1))

Tactic:
Nat.sub_self,

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic n R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic n R))

Tactic:
rcases n with (_ | _ | _ | n)
  · simp only [cyclotomic_zero, eval_one, zero_lt_one, implies_true, zero_le_one, and_self]
  · simp
  · simp only [zero_add, reduceAdd, cyclotomic_two, eval_add, eval_X, eval_one]
    constructor <;> intro <;> linarith
  · constructor <;> intro <;> [skip; apply le_of_lt] <;> apply cyclotomic_pos (by lia)

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

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : ζ' ∈ primitiveRoots n ℂ
⊢ q - 1 ≤ ‖↑q - ζ'‖

Tactic:
mem_primitiveRoots hn

Goal state after:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ q - 1 ≤ ‖↑q - ζ'‖
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case e'_5
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ q = ‖↑q‖

Tactic:
Complex.norm_real,

Goal state after:
case e'_5
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ q = ‖q‖
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : ζ' ∈ primitiveRoots n ℂ
⊢ ‖↑q - ζ'‖ ≤ q + 1

Tactic:
mem_primitiveRoots hn

Goal state after:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ ‖↑q - ζ'‖ ≤ q + 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case e'_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ q = ‖↑q‖

Tactic:
Complex.norm_real,

Goal state after:
case e'_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ q = ‖q‖
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
⊢ Algebra.IsIntegral A B

Tactic:
← (Subalgebra.equivOfEq _ _ ((IsCyclotomicExtension.iff_adjoin_eq_top S A B).1 ‹_›).2
    |>.trans Subalgebra.topEquiv).isIntegral_iff

Goal state after:
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsCyclotomicExtension S A B
⊢ Algebra.IsIntegral A ↥(adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
ζ : B
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
⊢ adjoin A ((cyclotomic n A).rootSet B) = adjoin A {b | ∃ a ∈ {n}, a ≠ 0 ∧ b ^ a = 1}

Tactic:
simp only [mem_singleton_iff, exists_eq_left]
  refine le_antisymm (adjoin_mono fun x hx => ?_) (adjoin_le fun x hx => ?_)
  · rw [mem_rootSet'] at hx
    simp only [mem_ofPred_eq]
    rw [isRoot_of_unity_iff (NeZero.pos n)]
    refine ⟨NeZero.ne n, n, Nat.mem_divisors_self n (NeZero.ne n), ?_⟩
    rw [IsRoot.def, ← map_cyclotomic n (algebraMap A B), eval_map_algebraMap]
    exact hx.2
  · simp only [mem_ofPred_eq] at hx
    obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx.2
    refine SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin ?_) _)
    rw [mem_rootSet', map_cyclotomic, ← eval_map_algebraMap, map_cyclotomic, ← IsRoot]
    exact ⟨cyclotomic_ne_zero n B, hζ.isRoot_cyclotomic (NeZero.pos n)⟩

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

Goal state before:
pp: case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
let d := a.val.gcd N

Goal state after:
case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d
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ζ : IsPrimitiveRoot ζ p
h : p ≠ 2
hirr : Irreducible (cyclotomic (p ^ (0 + 1)) K)
⊢ (Algebra.norm K) (ζ - 1) = ↑p

Tactic:
replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simp [hζ]

Goal state after:
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))
⊢ (Algebra.norm K) (ζ - 1) = ↑p
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) (2 ^ (k - k).succ)
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Tactic:
Nat.sub_self,

Goal state after:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) (2 ^ succ 0)
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case right
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})
⊢ Normal K ↥(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})

Tactic:
IntermediateField.normal_iff_forall_map_le

Goal state after:
case right
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})
⊢ ∀ (σ : AlgebraicClosure K →ₐ[K] AlgebraicClosure K),
    IntermediateField.map σ (IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ≤
      IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
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
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
hk : k ≠ 0
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
by_cases htwo : p ^ (k - s + 1) = 2
  · obtain ⟨hp, hks⟩ := (Nat.prime_two.pow_eq_iff).1 htwo
    simp only [add_eq_right] at hks
    replace hs : s = k := le_antisymm hs (Nat.sub_eq_zero_iff_le.mp hks)
    simp only [hp, hs] at hζ hirr hcycl ⊢
    obtain ⟨k₁, hk₁⟩ := Nat.exists_eq_succ_of_ne_zero hk
    rw [hζ.norm_pow_sub_one_two hirr, hk₁, _root_.pow_succ', pow_mul, neg_eq_neg_one_mul,
      mul_pow, neg_one_sq, one_mul, ← pow_mul, ← _root_.pow_succ']
    simp
  · exact hζ.norm_pow_sub_one_of_prime_pow_ne_two hirr hs htwo

Goal state after:
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:
rw [← Finset.mul_sum, h₂] at h₁

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 * Finset.univ.sum ⇑ψ = Finset.univ.sum ⇑ψ
h₂ : ∑ a, ψ a = Finset.univ.sum ⇑ψ
⊢ ∑ a, ψ a = 0
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Finite Rˣ
χ : MulChar R ℂ
val✝ : Fintype Rˣ
a : Rˣ
⊢ (star χ) ↑a = χ⁻¹ ↑a

Tactic:
simp only [inv_apply_eq_inv']

Goal state after:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Finite Rˣ
χ : MulChar R ℂ
val✝ : Fintype Rˣ
a : Rˣ
⊢ (star χ) ↑a = (χ ↑a)⁻¹
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
x y : R
| χ (y * x⁻¹) * ψ (y + -x)

Tactic:
← sub_eq_add_neg

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 y : R
| χ (y * x⁻¹) * ψ (y - x)
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 - ‖0‖ ^ p - 0) = fun x ↦ ‖x‖ ^ p

Tactic:
by simp [zero_lt_one.trans hp |>.ne']

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = χ (↑p ^ n) * gaussSum χ ψ
⊢ gaussSum χ ψ ^ p ^ (n + 1) = χ (↑p ^ (n + 1)) * gaussSum χ ψ

Tactic:
rw [pow_succ, pow_mul, ih, mul_pow, hχ.gaussSum_frob _ hp, ← mul_assoc, pow_succ, map_mul,
      ← pow_apply' χ fp.1.ne_zero ((p : R) ^ n), hχ.pow_char p]

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

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
k j : ZMod N
⊢ stdAddChar (-(j * k)) • Φ (-j) = stdAddChar (-((Equiv.neg (ZMod N)) j * -k)) • Φ ((Equiv.neg (ZMod N)) j)

Tactic:
by rw [Equiv.neg_apply, neg_mul_neg]

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
X : A i → (a : ι) → A a := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
⊢ (∫⋯∫⁻_{i}, f ∂μ) x ^ p *
      ((∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) * ∏ j ∈ s, (∫⁻ (t : A i), (∫⋯∫⁻_{j}, f ∂μ) (X t) ∂μ i) ^ p) =
    (∫⋯∫⁻_{i}, f ∂μ) x ^ p * ((∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p)

Tactic:
congr! 2
              · rw [lmarginal_singleton]
              refine prod_congr rfl fun j hj => ?_
              have hi' : i ∉ ({j} : Finset ι) := by
                simp only [Finset.mem_singleton] at hj ⊢
                exact fun h ↦ hi (h ▸ hj)
              rw [lmarginal_insert _ hf hi']

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 : E
⊢ (adjoint comul) (x ⊗ₜ[𝕜] (adjoint counit) One.one) = x

Tactic:
← lTensor_tmul,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x : E
⊢ (adjoint comul) ((LinearMap.lTensor E (adjoint counit)) (x ⊗ₜ[𝕜] One.one)) = x
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
r : 𝕜
x : E
⊢ (adjoint comul) ((LinearMap.rTensor E (adjoint counit)) (r ⊗ₜ[𝕜] x)) = (adjoint comul) (x ⊗ₜ[𝕜] (adjoint counit) r)

Tactic:
← lTensor_tmul,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ (adjoint comul) ((LinearMap.rTensor E (adjoint counit)) (r ⊗ₜ[𝕜] x)) =
    (adjoint comul) ((LinearMap.lTensor E (adjoint counit)) (x ⊗ₜ[𝕜] r))
Module: Mathlib.Analysis.InnerProductSpace.ExteriorPower

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : ↥(⋀[ℝ]^n E)
h : ∀ i ∈ Finset.univ, ((Module.Basis.exteriorPower n (stdOrthonormalBasis ℝ E).toBasis).repr x) i ^ 2 = 0
⊢ ∀ (i : ↑(Set.powersetCard (Fin (Module.finrank ℝ E)) n)),
    ((Module.Basis.exteriorPower n (stdOrthonormalBasis ℝ E).toBasis).repr x) i =
      ((Module.Basis.exteriorPower n (stdOrthonormalBasis ℝ E).toBasis).repr 0) i

Tactic:
simpa using h

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

Goal state before:
pp: case pos
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
v : V
h : 0 < ‖v‖
⊢ C * ‖v‖ * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖ * ‖v‖

Tactic:
calc
      C * ‖v‖ * ‖v‖ ≤ B v v := coercivity v
      _ = ⟪B♯ v, v⟫_ℝ := (continuousLinearMapOfBilin_apply B v v).symm
      _ ≤ ‖B♯ v‖ * ‖v‖ := real_inner_le_norm (B♯ v) v

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

Goal state before:
pp: V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
v : V
h : ¬0 < ‖v‖
⊢ v = 0

Tactic:
simpa using h

Goal state after:
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
x : E
hx : x ∈ f.closure.domain
hx' : (x, 0) ∈ closure[instTopologicalSpaceProd] ↑f.graph
⊢ ∃ a b, (a, b) ∈ closure[instTopologicalSpaceProd] ↑f.graph ∧ b = 0 ∧ a = x

Tactic:
exact ⟨x, 0, hx', rfl, rfl⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
a : 𝕜
x : F
hx : x ∈ {y | Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)}
⊢ a • x ∈ {y | Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)}

Tactic:
rw [Set.mem_ofPred_eq, LinearMap.map_smulₛₗ] at *
    exact hx.const_smul (conj a)

Goal state after: