mathlib-initiative/mathlib-tactics huggingface dataset:
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
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
hδ2 : ∀ ⦃a b : V⦄, ‖a - b‖ < δ → ‖f a - f b‖ < ε / ↑B
x : V
x✝ : x ∈ A
⊢ ‖x - (x + (1 / (2 * ‖w‖ ^ 2)) • w)‖ < δ

Tactic:
sub_add_cancel_left,

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
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
hδ2 : ∀ ⦃a b : V⦄, ‖a - b‖ < δ → ‖f a - f b‖ < ε / ↑B
x : V
x✝ : x ∈ A
⊢ ‖-((1 / (2 * ‖w‖ ^ 2)) • w)‖ < δ
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : ℕ
hn : Fact (Nat.Prime p)
⊢ cyclotomic p R * (X - 1) = X ^ p - 1

Tactic:
cyclotomic_prime,

Goal state after:
R : Type u_1
inst✝ : Ring R
p : ℕ
hn : Fact (Nat.Prime p)
⊢ (∑ i ∈ range p, X ^ i) * (X - 1) = X ^ p - 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ cyclotomic d ℤ ∣ ∑ i ∈ range n, X ^ i

Tactic:
rw [← prod_cyclotomic_eq_geom_sum hn]

Goal state after:
case inr
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ cyclotomic d ℤ ∣ ∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case refine_1
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
ζ₁ ζ₂ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
this : NeZero (k₁.lcm k₂)
⊢ {ζ₁, ζ₂} ⊆ ↑S[ζ]

Tactic:
refine Set.pair_subset_iff.mpr ⟨?_, ?_⟩
    · obtain ⟨_, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one <|
        (hζ₁.pow_eq_one_iff_dvd _).mpr <| k₁.dvd_lcm_left k₂
      exact Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton S _) _
    · obtain ⟨_, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one <|
        (hζ₂.pow_eq_one_iff_dvd _).mpr <| k₁.dvd_lcm_right k₂
      exact Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton S _) _

Goal state after:
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
x✝¹ : Fin p
x✝ : x✝¹ ∈ Finset.univ
⊢ (C (α x✝¹) * X ^ ↑x✝¹).degree ≤ ↑(p - 1)

Tactic:
grw [degree_C_mul_X_pow_le]; simp; grind

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

Goal state after:
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
⊢ Basis (Fin (minpoly K x).natDegree) K ↥K[x]
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: 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
x✝ : cyclotomic p ℚ ∣ P
c : ℚ[X]
hP' : ↑p.totient + c.degree ≤ ↑(p - 1)
hc : P = cyclotomic p ℚ * c
⊢ ∀ (i j : Fin p), α i = α j

Tactic:
Nat.totient_prime hp

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
x✝ : cyclotomic p ℚ ∣ P
c : ℚ[X]
hP' : ↑(p - 1) + c.degree ≤ ↑(p - 1)
hc : P = cyclotomic p ℚ * c
⊢ ∀ (i j : Fin p), α i = α j
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

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

Tactic:
have : m + k ≠ 0 := (add_pos_of_pos_of_nonneg hm k.zero_le).ne'
    rw [Nat.add_succ, pow_succ, ← cyclotomic_expand_eq_cyclotomic hp <| dvd_pow_self p this] at h
    exact hk (by lia) (of_irreducible_expand hp.ne_zero h)

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

Goal state before:
pp: case mk
p n : ℕ
inst✝¹² : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C✝ : Type w
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsCyclotomicExtension {n} A B
inst✝⁷ : Field K
inst✝⁶ : CommRing L
inst✝⁵ : IsDomain L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst✝² : CommRing C
inst✝¹ : IsDomain C
inst✝ : Algebra K C
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
hn : NeZero ↑n
val✝ : C
property✝ : (aeval val✝) (minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen) = 0
⊢ eval₂ (algebraMap K C) (↑⟨val✝, property✝⟩) (minpoly K ζ) = 0

Tactic:
← aeval_def

Goal state after:
case mk
p n : ℕ
inst✝¹² : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C✝ : Type w
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsCyclotomicExtension {n} A B
inst✝⁷ : Field K
inst✝⁶ : CommRing L
inst✝⁵ : IsDomain L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst✝² : CommRing C
inst✝¹ : IsDomain C
inst✝ : Algebra K C
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
hn : NeZero ↑n
val✝ : C
property✝ : (aeval val✝) (minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen) = 0
⊢ (aeval ↑⟨val✝, property✝⟩) (minpoly K ζ) = 0
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 : f b ∈ Subalgebra.map f (adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
⊢ (algebraMap B C) b ∈ adjoin A {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}

Tactic:
IsScalarTower.toAlgHom_apply,

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 ∈ Subalgebra.map f (adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
⊢ (algebraMap B C) b ∈ adjoin A {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
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✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
hS : S ⊆ {0, 1}
x : B
⊢ x ∈ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}

Tactic:
convert! (mem_top (R := A) : x ∈ ⊤)

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
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ¬ζ = 1

Tactic:
clear_value ζ

Goal state after:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ
hζ : IsPrimitiveRoot ζ n
⊢ ¬ζ = 1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
⊢ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ⊆ {b | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
by aesop

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

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

Tactic:
refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs hs' ↦ ?_, ?_⟩
  · rw [mem_union, mem_singleton_iff] at hs
    obtain hs | rfl := hs
    · exact H.exists_isPrimitiveRoot hs hs'
    · obtain ⟨m, hm, hm', ⟨x, rfl⟩⟩ := h
      obtain ⟨ζ, hζ⟩ := H.exists_isPrimitiveRoot hm hm'
      refine ⟨ζ ^ x, ?_⟩
      have h_xnz : x ≠ 0 := Nat.ne_zero_of_mul_ne_zero_right hm'
      have := hζ.pow_of_dvd h_xnz (dvd_mul_left x s)
      rwa [mul_div_cancel_right₀ _ h_xnz] at this
  · refine _root_.eq_top_iff.2 ?_
    rw [← ((iff_adjoin_eq_top S A B).1 H).2]
    refine adjoin_mono fun x hx ↦ ?_
    simp only [union_singleton, mem_insert_iff, mem_ofPred_eq] at hx ⊢
    obtain ⟨m, hm, hm'⟩ := hx
    exact ⟨m, ⟨Or.inr hm, hm'⟩⟩

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

Goal state before:
pp: case neg.refine_2
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : ¬∃ s ∈ S, s ≠ 0
H : IsCyclotomicExtension {1} A B
⊢ IsCyclotomicExtension ∅ A B

Tactic:
· refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs ↦ (notMem_empty s hs).elim, ?_⟩
      simp [singleton_one]

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

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : ζ.re ≤ 0 ∧ ζ.im = 0
⊢ ζ ≠ 0

Tactic:
clear_value ζ

Goal state after:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ
hζ : IsPrimitiveRoot ζ n
h : ζ.re ≤ 0 ∧ ζ.im = 0
⊢ ζ ≠ 0
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case mem
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 y : B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : y ^ n = 1
⊢ f y = g y

Tactic:
obtain ⟨r, hr1, hr2⟩ := H n hn h1

Goal state after:
case mem
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 y : B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : y ^ n = 1
r : B
hr1 : IsPrimitiveRoot r n
hr2 : f r = g r
⊢ f y = g y
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
this : {b | n ≠ 0 ∧ b ^ n = 1} = ↑(nthRoots n 1).toFinset
⊢ (↑(nthRoots n 1).toFinset).Finite

Tactic:
exact (nthRoots n 1).toFinset.finite_toSet

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

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

pp: case e'_4
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : ‖eval (↑q) (cyclotomic n ℂ)‖ < max (q + 1) 0 ^ φ n
⊢ q + 1 = max (q + 1) 0

Tactic:
· rw [eq_comm]
      simp [cyclotomic_nonneg n hq'.le]

Goal state after:
case e'_4
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : ‖eval (↑q) (cyclotomic n ℂ)‖ < max (q + 1) 0 ^ φ n
⊢ q + 1 = max (q + 1) 0
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case pos
S✝ : Set ℕ
n : ℕ
S : Set ℕ
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
hn : n = 0
⊢ Module.Finite A B

Tactic:
have : insert n S \ {0} = S \ {0} := by simp_all

Goal state after:
case pos
S✝ : Set ℕ
n : ℕ
S : Set ℕ
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
hn : n = 0
this : insert n S \ {0} = S \ {0}
⊢ Module.Finite A B
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: m : ℕ
n : ℤ
h : IsUnit ↑n
⊢ ∃ b, (↑n)⁻¹ * b = 1 ∧ b * (↑n)⁻¹ = 1

Tactic:
exact ⟨n, inv_mul_of_unit _ h, mul_inv_of_unit _ h⟩

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

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
⊢ Nat.card (GaloisField p n) = p ^ n

Tactic:
let b := IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
b : Module.Basis (↥(IsNoetherian.finsetBasisIndex (ZMod p) (GaloisField p n))) (ZMod p) (GaloisField p n) :=
  IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
⊢ Nat.card (GaloisField p n) = p ^ n
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
⊢ IsGalois K L

Tactic:
rw [isGalois_iff]

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
⊢ Algebra.IsSeparable K L ∧ Normal K L
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:
rw [Fintype.card_eq_nat_card, natCard_algHom_of_finrank_dvd h]

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
⊢ ∀ {n : ℕ}, n ∈ {0} → n ≠ 0 → ∃ r, IsPrimitiveRoot r n

Tactic:
by aesop

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

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ ↑↑(toUnits (toCircle x) ^ n) = ↑↑1

Tactic:
simp [← AddChar.map_nsmul_eq_pow]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x✝ : ↥(rootsOfUnity n Circle)
⊢ (fun z ↦ ⟨(rootsOfUnitytoCircle n).toHomUnits z, ⋯⟩)
      ((↑((rootsOfUnityUnitsMulEquiv ℂ n).toMonoidHom.comp (restrictRootsOfUnity Circle.toUnits n))).toFun x✝) =
    x✝

Tactic:
by aesop

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x✝ : ↥(rootsOfUnity n ℂ)
⊢ (↑((rootsOfUnityUnitsMulEquiv ℂ n).toMonoidHom.comp (restrictRootsOfUnity Circle.toUnits n))).toFun
      ((fun z ↦ ⟨(rootsOfUnitytoCircle n).toHomUnits z, ⋯⟩) x✝) =
    x✝

Tactic:
by aesop

Goal state after:
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:
exact (inv_eq_conj <| norm_eq_one_of_mem_rootsOfUnity <| χ.apply_mem_rootsOfUnity a).symm

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
⊢ n ≠ 0

Tactic:
by aesop

Goal state after:
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
inst✝ : IsDomain R
χ : DirichletCharacter R N
he : ¬e.IsPrimitive
hχ : gaussSum χ e ≠ 0
d : ℕ
hd₁ : d ∣ N
hd₂ : d < N
hed : e.mulShift ↑d = 1
this : χ.conductor ≤ d
⊢ ¬χ.IsPrimitive

Tactic:
exact (this.trans_lt hd₂).ne

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

Goal state before:
pp: S : Type u_2
inst✝¹ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst✝ : NoZeroDivisors S
⊢ ψ.Even ∨ ψ.Odd

Tactic:
by
  suffices ψ (-1) ^ 2 = 1 by convert! sq_eq_one_iff.mp this
  rw [← map_pow _, neg_one_sq, map_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
⊢ ‖p‖ * ‖‖x‖ ^ (p - 2)‖ * ‖(innerSL ℝ) x‖ = p * ‖x‖ ^ (p - 1)

Tactic:
simp_rw [norm_rpow_of_nonneg (norm_nonneg _), norm_norm, norm_eq_abs,
    abs_eq_self.mpr <| zero_le_one.trans hp.le, mul_assoc, innerSL_apply_norm]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ p * (‖x‖ ^ (p - 2) * ‖x‖) = p * ‖x‖ ^ (p - 1)
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
⊢ ∫⁻ (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

Tactic:
have hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t) :=
    fun {_} ↦ hf.lmarginal μ |>.comp <| measurable_update _

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
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
⊢ ∫⁻ (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.JointEigenspace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
hA : A.IsSymmetric
hB : B.IsSymmetric
i j : 𝕜 × 𝕜
hij : i ≠ j
v : E
x✝ : v ∈ eigenspace A i.2 ⊓ eigenspace B i.1
hv1 : v ∈ ↑(eigenspace A i.2)
hv2 : v ∈ ↑(eigenspace B i.1)
⊢ i.1 ≠ j.1 ∨ i.2 ≠ j.2

Tactic:
rwa [Ne.eq_def, Prod.ext_iff, not_and_or] at hij

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

Goal state before:
pp: case mpr
𝕜 : 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
g : Submodule 𝕜 (E × F)
x : F × E
h : ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0
⊢ ∀ (u : WithLp 2 (F × E)) (x_1 : E) (x_2 : F),
    (x_1, x_2) ∈ g → toLp 2 (x_2, -x_1) = u → ⟪u.fst, (toLp 2 x).fst⟫ + ⟪u.snd, (toLp 2 x).snd⟫ = 0

Tactic:
intro u a b hab hu

Goal state after:
case mpr
𝕜 : 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
g : Submodule 𝕜 (E × F)
x : F × E
h : ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0
u : WithLp 2 (F × E)
a : E
b : F
hab : (a, b) ∈ g
hu : toLp 2 (b, -a) = u
⊢ ⟪u.fst, (toLp 2 x).fst⟫ + ⟪u.snd, (toLp 2 x).snd⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
⊢ f.normDet = 0 ↔ finrank 𝕜 ↥f.range ≠ finrank 𝕜 U

Tactic:
simp [normDet_eq_zero_iff_ker_ne_bot, ← f.finrank_range_add_finrank_ker]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (fun n ↦ (↑n)⁻¹) atTop (𝓟 (Ioi 0))

Tactic:
refine tendsto_principal.2 (Eventually.of_forall fun n => ?_)

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
n : ℕ
⊢ (↑n)⁻¹ ∈ Ioi 0
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
e : X ≃ᵢ Y
s : Set Y
⊢ dimH (⇑e.symm '' s) = dimH s

Tactic:
e.symm.dimH_image

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
e : X ≃ᵢ Y
s : Set Y
⊢ dimH s = dimH s
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
s : Set F
⊢ dimH (⇑e.symm '' s) = dimH s

Tactic:
e.symm.dimH_image

Goal state after:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
s : Set F
⊢ dimH s = dimH s