mathlib-initiative/mathlib-tactics huggingface dataset:
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
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : ℕ → R := fun n ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ d ∈ n.divisors, μ (n / d) • G d = f n

Tactic:
← sum_divisorsAntidiagonal' (f := fun x y => μ x • G y)

Goal state after:
case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : ℕ → R := fun n ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ i ∈ n.divisorsAntidiagonal, μ i.1 • G i.2 = f n
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
⊢ (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x ↦ |x| ^ (-b)

Tactic:
have : ∀ x : ℝ,
      ‖(f.comp (ContinuousMap.addRight x)).restrict K‖ ≤ ‖f.restrict (Icc (x - r) (x + r))‖ := by
    intro x
    rw [ContinuousMap.norm_le _ (norm_nonneg _)]
    rintro ⟨y, hy⟩
    refine (le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨y + x, ?_⟩)
    · simp_rw [ContinuousMap.restrict_apply, ContinuousMap.comp_apply, ContinuousMap.coe_addRight]
    · exact ⟨by linarith [(hr hy).1], by linarith [(hr hy).2]⟩

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
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖ ≤ ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
⊢ (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x ↦ |x| ^ (-b)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

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

Tactic:
refine (Nat.le_of_dvd hk (k.gcd_dvd_left l)).eq_of_not_lt fun h' ↦ ?_

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
h' : k.gcd l < k
⊢ False
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ∈ rootsOfUnity n ℂ
⊢ ↑1 ^ 2 = 1

Tactic:
ofReal_one,

Goal state after:
ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ∈ rootsOfUnity n ℂ
⊢ 1 ^ 2 = 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
m : ℕ
left✝ : m < n
⊢ 1 ^ m * a = a

Tactic:
one_pow,

Goal state after:
case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
m : ℕ
left✝ : m < n
⊢ 1 * a = a
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 μ
⊢ IsPrimitiveRoot μ n

Tactic:
have hμn : μ ^ n = 1 := by
    rw [isRoot_of_unity_iff hnpos _]
    exact ⟨n, n.mem_divisors_self hnpos.ne', hμ⟩

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
⊢ IsPrimitiveRoot μ n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
μ : R
hf : Function.Injective ⇑(algebraMap R (FractionRing R))
this : NeZero ↑n
⊢ (cyclotomic n (FractionRing R)).IsRoot ((algebraMap R (FractionRing R)) μ) ↔
    IsPrimitiveRoot ((algebraMap R (FractionRing R)) μ) n

Tactic:
←
    isRoot_cyclotomic_iff'

Goal state after:
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
μ : R
hf : Function.Injective ⇑(algebraMap R (FractionRing R))
this : NeZero ↑n
⊢ (cyclotomic n (FractionRing R)).IsRoot ((algebraMap R (FractionRing R)) μ) ↔
    (cyclotomic n (FractionRing R)).IsRoot ((algebraMap R (FractionRing R)) μ)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
this : C r ∣ (C a * X - 1) ^ p - -1 ^ p
⊢ C r ∣ (C a * X - 1) ^ p + 1

Tactic:
one_pow,

Goal state after:
case refine_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
this : C r ∣ (C a * X - 1) ^ p - -1
⊢ C r ∣ (C a * X - 1) ^ p + 1
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
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i✝ : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
⊢ IsIntegral R ((B.basis.repr B'.gen) i)

Tactic:
← h,

Goal state after:
K : Type u_1
S : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing S
inst✝⁴ : Algebra K S
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i✝ : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
⊢ IsIntegral R ((B.basis.repr ((aeval B.gen) P)) i)
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
⊢ cyclotomic (n * p) R = cyclotomic n R ^ (p - 1)

Tactic:
let : Algebra (ZMod p) R := ZMod.algebra _ _

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) R = cyclotomic n R ^ (p - 1)
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
⊢ cyclotomic (n * p) R = cyclotomic n R ^ p

Tactic:
let : Algebra (ZMod p) R := ZMod.algebra _ _

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) R = cyclotomic n R ^ p
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (cyclotomic (p.lcm q) K)
⊢ φ (p.lcm q) ≤ Module.finrank K L

Tactic:
rcases Nat.eq_zero_or_pos p with (rfl | hppos)
  · simp
  rcases Nat.eq_zero_or_pos q with (rfl | hqpos)
  · simp
  let z := x ^ (p / factorizationLCMLeft p q) * y ^ (q / factorizationLCMRight p q)
  let k := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩
  have : IsPrimitiveRoot z k := hx.pow_mul_pow_lcm hy hppos.ne' hqpos.ne'
  have := IsPrimitiveRoot.adjoin_isCyclotomicExtension K this
  convert! Submodule.finrank_le (Subalgebra.toSubmodule (adjoin K { z }))
  rw [show Nat.lcm p q = (k : ℕ) from rfl] at hirr
  simpa using! (IsCyclotomicExtension.finrank (Algebra.adjoin K {z}) hirr).symm

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

Goal state before:
pp: case refine_1
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)
x✝ : IsCyclotomicExtension S A B
hprim : ∀ {n : ℕ}, n ∈ S → n ≠ 0 → ∃ r, IsPrimitiveRoot r n
adjoin_roots✝ : ∀ (x : B), x ∈ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
⊢ S ⊆ {0, 1}

pp: case refine_2
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}
⊢ IsCyclotomicExtension S A B

Tactic:
· refine subset_pair_iff.mpr fun s hs ↦ or_iff_not_imp_left.mpr fun hs' ↦ ?_
    obtain ⟨ζ, hζ⟩ := hprim hs hs'
    exact mod_cast hζ.unique (IsPrimitiveRoot.of_subsingleton ζ)

Goal state after:
case refine_2
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}
⊢ IsCyclotomicExtension S A B
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 ^ Module.finrank K L
⊢ (Algebra.norm K) ζ = 1

Tactic:
one_pow,

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

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
hn : IsPrimePow n
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic n K)
h : n ≠ 2
this : succ 1 < n
hprime : Fact (Nat.Prime n.minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }
⊢ (Algebra.norm K) (ζ - 1) = ↑n.minFac

Tactic:
rw [sub_one_norm_eq_eval_cyclotomic hζ this hirr]

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
hn : IsPrimePow n
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic n K)
h : n ≠ 2
this : succ 1 < n
hprime : Fact (Nat.Prime n.minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }
⊢ ↑(eval 1 (cyclotomic n ℤ)) = ↑n.minFac
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case succ.refine_2
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ (aeval 0) (X ^ (n✝ + 1) ^ n - X) = 0

Tactic:
← coeff_zero_eq_aeval_zero'

Goal state after:
case succ.refine_2
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ (algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ((X ^ (n✝ + 1) ^ n - X).coeff 0) = 0
Module: Mathlib.Data.ZMod.Units

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

Tactic:
obtain ⟨a₀, (ha₀ : _ = d * _)⟩ := a.val.gcd_dvd_left N

Goal state after:
case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
inst✝ : Finite R
e : AddChar R R'
r x : R
h : x * r = 0
h' : ¬x = 0
⊢ ¬(e.mulShift r).mulShift x ≠ 1

Tactic:
by simp only [mulShift_mulShift, mul_comm r, h, mulShift_zero, not_ne_iff]

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

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this✝ : Finite K
this : Fintype K
⊢ IsSplittingField (ZMod p) K (X ^ p ^ n - X)

Tactic:
← h,

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this✝ : Finite K
this : Fintype K
⊢ IsSplittingField (ZMod p) K (X ^ Nat.card K - X)
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₁ : ∑ a, ψ (b + a) = ∑ a, ψ a
⊢ ∑ a, ψ a = 0

Tactic:
simp_rw [map_add_eq_mul] 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₁ : ∑ x, ψ b * ψ x = ∑ a, ψ a
⊢ ∑ a, ψ a = 0
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2) * 1 ^ (n / 4)

Tactic:
one_pow,

Goal state after:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2) * 1
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'ˣ
⊢ ∀ (a : R), ¬IsUnit a → (if hx : IsUnit a then ↑(f hx.unit) else 0) = 0

Tactic:
intro a ha
    simp only [ha, not_false_iff, dif_neg]

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'
χ : MulChar R R'
a✝ : Rˣ
⊢ (1 * χ) ↑a✝ = χ ↑a✝

Tactic:
simp only [one_mul, Pi.mul_apply, MulChar.coeToFun_mul, MulChar.one_apply_coe]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d m : ℕ
inst✝ : NeZero n
hχ : χ.FactorsThrough d
hd : d ∣ m
hm : m ∣ n
⊢ χ.FactorsThrough m

Tactic:
by
  refine (factorsThrough_iff_ker_unitsMap hm).mpr fun x hx ↦ ?_
  apply (factorsThrough_iff_ker_unitsMap hχ.dvd).mp hχ
  rw [MonoidHom.mem_ker] at hx ⊢
  rw [← ZMod.unitsMap_comp hd hm, MonoidHom.comp_apply, hx, map_one]

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

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
A : Type u
K : Type w
inst✝² : CommRing A
inst✝¹ : Field K
inst✝ : Algebra A K
μ : CyclotomicField n K
h : IsPrimitiveRoot μ n
⊢ CyclotomicRing n A K = ↥A[μ]

Tactic:
← IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic h,

Goal state after:
n : ℕ
inst✝³ : NeZero n
A : Type u
K : Type w
inst✝² : CommRing A
inst✝¹ : Field K
inst✝ : Algebra A K
μ : CyclotomicField n K
h : IsPrimitiveRoot μ n
⊢ CyclotomicRing n A K = ↥(adjoin A ((cyclotomic n A).rootSet (CyclotomicField n K)))
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ : MulChar R R'
hχ : χ.IsQuadratic
f : R' →+* R''
⊢ (χ.ringHomComp f).IsQuadratic

Tactic:
by
  intro a
  rcases hχ a with (ha | ha | ha) <;> simp [ha]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = 0
⊢ 0 ^ p = 0

Tactic:
rw [zero_pow (@Fact.out p.Prime).ne_zero]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case hi
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a ∈ univ, a + x ∈ univ

pp: case i_inj
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a₁ ∈ univ, ∀ a₂ ∈ univ, a₁ + x = a₂ + x → a₁ = a₂

pp: case i_surj
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ b ∈ univ, ∃ a, ∃ (_ : a ∈ univ), a + x = b

pp: case h
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a ∈ univ, χ x * φ a * ψ (x + a) = χ x * φ (a + x - x) * ψ (a + x)

Tactic:
· simp only [mem_univ, forall_const]

Goal state after:
case i_inj
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a₁ ∈ univ, ∀ a₂ ∈ univ, a₁ + x = a₂ + x → a₁ = a₂

case i_surj
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ b ∈ univ, ∃ a, ∃ (_ : a ∈ univ), a + x = b

case h
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ ∀ a ∈ univ, χ x * φ a * ψ (x + a) = χ x * φ (a + x - x) * ψ (a + x)
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case convert_1
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ ↑(#s) * p ≤ 1

Tactic:
refine le_trans ?_ hp
    gcongr
    suffices (s.card : ℝ) + 1 ≤ #ι by linarith
    rw [← card_add_card_compl s]
    norm_cast
    gcongr
    have hi' : sᶜ.Nonempty := ⟨i, by rwa [Finset.mem_compl]⟩
    rwa [← card_pos] at hi'

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
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f.closure.IsClosed

Tactic:
rw [IsClosed, ← hf.graph_closure_eq_closure_graph]
  exact f.graph.isClosed_topologicalClosure

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) ∈ f.closure.graph
⊢ (0, x) ∈ f'.graph

Tactic:
← h,

Goal state after:
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) ∈ f.closure.graph
⊢ (0, x) ∈ f.inverse.graph.topologicalClosure
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
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
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
h2γ : γ * n' = p'
h3γ : (↑γ - 1) * q = ↑p'
⊢ eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
have h4γ : (γ : ℝ) ≠ 0 := (zero_lt_one.trans h1γ).ne'

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
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
h2γ : γ * n' = p'
h3γ : (↑γ - 1) * q = ↑p'
h4γ : ↑γ ≠ 0
⊢ eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: case mp
𝕜 : 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
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
x : F × E
hx : x.1 ∈ T†.domain
h : ↑T† ⟨x.1, ⋯⟩ = x.2
a : E
ha : a ∈ T.domain
⊢ ⟪↑T ⟨a, ⋯⟩, x.1⟫ - ⟪a, x.2⟫ = 0

Tactic:
← h,

Goal state after:
case mp
𝕜 : 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
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
x : F × E
hx : x.1 ∈ T†.domain
h : ↑T† ⟨x.1, ⋯⟩ = x.2
a : E
ha : a ∈ T.domain
⊢ ⟪↑T ⟨a, ⋯⟩, x.1⟫ - ⟪a, ↑T† ⟨x.1, ⋯⟩⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.SingularValues

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
n : ℕ
⊢ ¬n < finrank 𝕜 ↥T.range ↔ finrank 𝕜 ↥T.range ≤ n

Tactic:
not_lt

Goal state after:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
n : ℕ
⊢ finrank 𝕜 ↥T.range ≤ n ↔ finrank 𝕜 ↥T.range ≤ n