mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ ↑ζ • f' = g' ↔ μ • g' = f'

pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ μ • g' = f' ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
· constructor <;> intro h <;>
      simp only [← h, ← mul_smul, moebius_mul_coe_zeta, coe_zeta_mul_moebius, one_smul]

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ μ • g' = f' ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
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
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
refine
    { pow_eq_one := by rw [← pow_mul', pow_mul, h.pow_eq_one, one_pow]
      dvd_of_pow_eq_one := fun l hl ↦ h.dvd_of_pow_eq_one l ?_ }

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
⊢ ζ ^ l = 1
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: f : 𝓢(ℝ, ℂ)
x : ℝ
⊢ ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), (𝓕 f) ↑n * (fourier n) ↑x

Tactic:
by
  -- We know that Schwartz functions are `O(‖x ^ (-b)‖)` for *every* `b`; for this argument we take
  -- `b = 2` and work with that.
  apply Real.tsum_eq_tsum_fourier_of_rpow_decay f.continuous one_lt_two
    (f.isBigO_cocompact_rpow (-2)) ((𝓕 f).isBigO_cocompact_rpow (-2))

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

Goal state before:
pp: q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ n.natAbs.Coprime q.den

Tactic:
apply Nat.Coprime.coprime_mul_left (k := 2)

Goal state after:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ (2 * n.natAbs).Coprime q.den
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
e : (fun x ↦ ζ ^ x) i = (fun x ↦ ζ ^ x) j
⊢ i = j

Tactic:
exact hζ.pow_inj hi hj e

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

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
⊢ ζ ^ l = 1

Tactic:
rw [← inv_inj, ← inv_pow, hl, inv_one]

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

Goal state before:
pp: case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
this : 0 ≤ -i
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
lift -i to ℕ using this with i' hi'

Goal state after:
case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ IsPrimitiveRoot (ζ ^ i) k
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
⊢ IsCoprime (if i * 2 ≤ n then ↑i else ↑i - ↑n) ↑n

Tactic:
case =>

Goal state after:
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
⊢ ζ ^ m * α ∈ nthRoots n a

Tactic:
mem_nthRoots hn,

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
⊢ (ζ ^ m * α) ^ n = a
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case refine_1.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:
obtain ⟨_, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one <|
        (hζ₁.pow_eq_one_iff_dvd _).mpr <| k₁.dvd_lcm_left k₂

Goal state after:
case refine_1.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₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
this : NeZero (k₁.lcm k₂)
w✝ : ℕ
left✝ : w✝ < k₁.lcm k₂
hζ₁ : IsPrimitiveRoot (ζ ^ w✝) k₁
⊢ ζ ^ w✝ ∈ ↑S[ζ]
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ #{ val := nthRoots n 1, nodup := ⋯ } = n

Tactic:
card_mk,

Goal state after:
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ (nthRoots n 1).card = n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (algebraMap R[X] (RatFunc R)) (cyclotomic n R) =
    ∏ i ∈ n.divisorsAntidiagonal, (algebraMap R[X] (RatFunc R)) (X ^ i.2 - 1) ^ μ i.1

Tactic:
by
  rcases n.eq_zero_or_pos with (rfl | hpos)
  · simp
  have h : ∀ n : ℕ, 0 < n → (∏ i ∈ Nat.divisors n, algebraMap _ (RatFunc R) (cyclotomic i R)) =
      algebraMap _ _ (X ^ n - 1 : R[X]) := by
    intro n hn
    rw [← prod_cyclotomic_eq_X_pow_sub_one hn R, map_prod]
  rw [(prod_eq_iff_prod_pow_moebius_eq_of_nonzero (fun n hn => _) fun n hn => _).1 h n hpos] <;>
    simp_rw [Ne, IsFractionRing.to_map_eq_zero_iff]
  · simp [cyclotomic_ne_zero]
  · intro n hn
    apply Monic.ne_zero
    apply monic_X_pow_sub_C _ (ne_of_gt hn)

Goal state after:
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case neg
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
⊢ IsIntegral R ((B.basis.repr ((algebraMap R A) (Q.coeff ↑⟨j, hj⟩) * B.basis ⟨j, hj⟩)) i)

Tactic:
IsScalarTower.algebraMap_apply R S A,

Goal state after:
case neg
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
⊢ IsIntegral R ((B.basis.repr ((algebraMap S A) ((algebraMap R S) (Q.coeff ↑⟨j, hj⟩)) * B.basis ⟨j, hj⟩)) i)
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case inr.inr
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)
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩
this✝ : IsPrimitiveRoot z ↑k
this : IsCyclotomicExtension {↑k} K ↥K[z]
⊢ φ (p.lcm q) ≤ Module.finrank K L

Tactic:
convert! Submodule.finrank_le (Subalgebra.toSubmodule (adjoin K { z }))

Goal state after:
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)
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩
this✝ : IsPrimitiveRoot z ↑k
this : IsCyclotomicExtension {↑k} K ↥K[z]
⊢ φ (p.lcm q) = Module.finrank K ↥(Subalgebra.toSubmodule K[z])
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case pos
K : Type u
L : Type v
inst✝⁵ : CommRing L
ζ : L
inst✝⁴ : Field K
inst✝³ : Algebra K L
inst✝² : IsDomain L
inst✝¹ : NeZero 2
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
hirr : Irreducible (cyclotomic 2 K)
⊢ (-1) ^ Module.finrank K L = -1

Tactic:
IsCyclotomicExtension.finrank _ hirr

Goal state after:
case pos
K : Type u
L : Type v
inst✝⁵ : CommRing L
ζ : L
inst✝⁴ : Field K
inst✝³ : Algebra K L
inst✝² : IsDomain L
inst✝¹ : NeZero 2
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsCyclotomicExtension {2} K L
hirr : Irreducible (cyclotomic 2 K)
⊢ (-1) ^ φ 2 = -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
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝ : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this : FiniteDimensional K L := finiteDimensional {n} K L
⊢ (algebraMap K E) ((Algebra.norm K) (ζ - 1)) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))

Tactic:
let := IsCyclotomicExtension.isGalois {n} K L

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
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝¹ : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝ : FiniteDimensional K L := finiteDimensional {n} K L
this : IsGalois K L := isGalois {n} K L
⊢ (algebraMap K E) ((Algebra.norm K) (ζ - 1)) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

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

Tactic:
simp only [Finset.mem_attach, Subtype.exists, ←
      NNReal.coe_lt_coe, ← Units.val_lt_val, Units.val_mk0 _, coe_nnnorm]

Goal state after:
case convert_6
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∃ a, ∃ (_ : a ∈ primitiveRoots n ℂ), True ∧ ↑(q - 1).toNNReal < ‖↑q - a‖
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case convert_6
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
⊢ ∃ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖↑q - ↑i‖₊ ⋯ < Units.mk0 (q + 1).toNNReal ⋯

Tactic:
simp only [Finset.mem_attach, Subtype.exists, ←
      NNReal.coe_lt_coe, ← Units.val_lt_val, Units.val_mk0 _, coe_nnnorm]

Goal state after:
case convert_6
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
⊢ ∃ a, ∃ (_ : a ∈ primitiveRoots n ℂ), True ∧ ‖↑q - a‖ < ↑(q + 1).toNNReal
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
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
key : ∀ b ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}, IsAlgebraic K b
⊢ IsCyclotomicExtension S K ↥(adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})

Tactic:
exact Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot S K L h

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

Goal state before:
pp: case pos
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
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
replace hs : s = k := le_antisymm hs (Nat.sub_eq_zero_iff_le.mp hks)

Goal state after:
case pos
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)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s
Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

Goal state before:
pp: case refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ n ∣ Monoid.exponent ↥(rootsOfUnity n M)

Tactic:
· nth_rewrite 1 [h.eq_orderOf]
    rw [← (h.isUnit NeZero.out).unit_spec, orderOf_units]
    let ζ' : rootsOfUnity n M := ⟨(h.isUnit NeZero.out).unit, ?_⟩
    · rw [← Subgroup.orderOf_mk]
      exact Monoid.order_dvd_exponent ζ'
    simp only [mem_rootsOfUnity]
    rw [← Units.val_inj, Units.val_pow_eq_pow_val, IsUnit.unit_spec, h.pow_eq_one, Units.val_one]

Goal state after:
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
inst✝ : IsCyclotomicExtension {n} K L
x : L
⊢ x ^ n = 1 → X ^ n - 1 ≠ 0

Tactic:
exact fun _ => X_pow_sub_C_ne_zero (NeZero.pos n) (1 : L)

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : Fintype M
inst✝¹ : DecidableEq M
R : Type u_2
inst✝ : CommMonoidWithZero R
inst_cyc : IsCyclic Mˣ
ζ : ↥(rootsOfUnity (Fintype.card Mˣ) R)
⊢ ↑↑((fun χ ↦ ⟨χ.toUnitHom (Classical.choose ⋯), ⋯⟩) ((fun ζ ↦ ofRootOfUnity ⋯ ⋯) ζ)) = ↑↑ζ

Tactic:
simp only [toUnitHom_eq, coe_equivToUnitHom, ofRootOfUnity_spec]

Goal state after:
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''
f : R' →+* R''
hf : Function.Injective ⇑f
χ : MulChar R R'
⊢ χ.ringHomComp f = 1 ↔ χ = 1

Tactic:
by
  conv_lhs => rw [← (show (1 : MulChar R R').ringHomComp f = 1 by simp)]
  exact (injective_ringHomComp hf).eq_iff

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ⁻¹.conductor = χ.conductor

Tactic:
by
  rw [← zpow_neg_one]
  refine dvd_antisymm (conductor_zpow_dvd ..) ?_
  nth_rewrite 1 [← inv_inv χ, ← zpow_neg_one, ← zpow_neg_one]
  exact conductor_zpow_dvd ..

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

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasFDerivAt (fun x ↦ ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x

Tactic:
apply HasStrictFDerivAt.hasFDerivAt

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ HasStrictFDerivAt (fun x ↦ ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x
Module: Mathlib.Order.Grade

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
s : Flag α
a : ↥s
h : IsMax a
b : α
hab : ↑a ≤ b
c : α
hc : c ∈ s
⊢ b ≤ c ∨ c ≤ b

Tactic:
classical
    exact .inr <| hab.trans' <| h.isTop ⟨c, hc⟩

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto (fderiv ℝ fun x ↦ ‖x‖ ^ p) (𝓝 0) (𝓝 (fderiv ℝ (fun x ↦ ‖x‖ ^ p) 0))

Tactic:
fderiv_norm_rpow (0 : E) hp,

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto (fderiv ℝ fun x ↦ ‖x‖ ^ p) (𝓝 0) (𝓝 ((p * ‖0‖ ^ (p - 2)) • (innerSL ℝ) 0))
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))

Tactic:
let FF := CyclotomicField 8 F

Goal state after:
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case h₂
ι : 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
hi' : sᶜ.Nonempty
⊢ 1 ≤ #sᶜ

Tactic:
← card_pos

Goal state after:
case h₂
ι : 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
hi' : 0 < #sᶜ
⊢ 1 ≤ #sᶜ
Module: Mathlib.Analysis.InnerProductSpace.ExteriorPower

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : LinearOrder ι
b : OrthonormalBasis ι ℝ E
x y : ↥(⋀[ℝ]^n E)
⊢ (innerProductForm x) y =
    ∑ s, ((Module.Basis.exteriorPower n b.toBasis).repr y) s * ((Module.Basis.exteriorPower n b.toBasis).repr x) s

Tactic:
conv_lhs =>
    rw [← (b.toBasis.exteriorPower n).sum_repr x, ← (b.toBasis.exteriorPower n).sum_repr y]

Goal state after:
n : ℕ
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : LinearOrder ι
b : OrthonormalBasis ι ℝ E
x y : ↥(⋀[ℝ]^n E)
⊢ (innerProductForm
        (∑ i, ((Module.Basis.exteriorPower n b.toBasis).repr x) i • (Module.Basis.exteriorPower n b.toBasis) i))
      (∑ i, ((Module.Basis.exteriorPower n b.toBasis).repr y) i • (Module.Basis.exteriorPower n b.toBasis) i) =
    ∑ s, ((Module.Basis.exteriorPower n b.toBasis).repr y) s * ((Module.Basis.exteriorPower n b.toBasis).repr x) s
Module: Mathlib.Analysis.InnerProductSpace.Positive

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

Tactic:
IsIdempotentElem.isPositive_iff_isSymmetric hp.toLinearMap

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
⊢ (↑p).IsSymmetric ↔ IsSelfAdjoint p
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case e_a.e_a
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p
v : (ι → ℝ) → F := u ∘ ⇑e.symm
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ ∫⁻ (y : ι → ℝ), ‖fderiv ℝ u (e.symm y)‖ₑ = ∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂Measure.map (⇑e.symm) volume

Tactic:
rw [lintegral_map _ e.symm.continuous.measurable]

Goal state after:
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p
v : (ι → ℝ) → F := u ∘ ⇑e.symm
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ Measurable fun x ↦ ‖fderiv ℝ u x‖ₑ
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: case mpr
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.closure.toFun.ker = ⊥ → f.inverse.IsClosable

Tactic:
intro h
    use f.closure.inverse
    exact (closure_inverse_graph hf hf' h).symm

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
inst✝ : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), ⟪w, ↑x⟫ = ⟪y, ↑T x⟫
this : Continuous ⇑((innerSL 𝕜) w ∘SL T.domain.subtypeL)
⊢ Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)

Tactic:
convert this

Goal state after:
𝕜 : 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
y : F
w : E
hw : ∀ (x : ↥T.domain), ⟪w, ↑x⟫ = ⟪y, ↑T x⟫
this : Continuous ⇑((innerSL 𝕜) w ∘SL T.domain.subtypeL)
⊢ ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun) = ⇑((innerSL 𝕜) w ∘SL T.domain.subtypeL)
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : A† = A
h : ¬Dense ↑A.domain
x : E
⊢ Continuous ⇑((innerₛₗ 𝕜) x ∘ₗ A†.toFun)

Tactic:
refine (innerSL 𝕜 x).cont.comp ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : A† = A
h : ¬Dense ↑A.domain
x : E
⊢ Continuous ⇑A†.toFun