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

Goal state before:
pp: V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
⊢ Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • 𝓕 f w) volume

Tactic:
have B : Continuous fun p : V × V => (- innerₗ V) p.1 p.2 := continuous_inner.neg

Goal state after:
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
B : Continuous[instTopologicalSpaceProd, _] fun p ↦ ((-innerₗ V) p.1) p.2
⊢ Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • 𝓕 f w) volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: k : ℕ
⊢ Gamma (↑k + 1 / 2) = ↑(2 * k - 1)‼ * √π / 2 ^ k

Tactic:
by
  cases k with
  | zero => simp [-one_div, Gamma_one_half_eq]
  | succ k => simpa [-one_div, mul_add] using Gamma_nat_add_one_add_half k

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
this : Gamma (s + 1) ≠ 0
⊢ Gamma s ≠ 0

Tactic:
Gamma_add_one,

Goal state after:
case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
this : s * Gamma s ≠ 0
⊢ Gamma s ≠ 0

case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
this : Gamma (s + 1) ≠ 0
⊢ s ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e'_2.e'_7.e'_5
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
y : ι → ℝ
⊢ -(b * ↑‖WithLp.toLp 2 y‖ ^ 2) = -b * ∑ i, ↑(y i) ^ 2

Tactic:
simp only [EuclideanSpace.norm_eq, norm_eq_abs, sq_abs, neg_mul, neg_inj, mul_eq_mul_left_iff]

Goal state after:
case e'_2.e'_7.e'_5
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
y : ι → ℝ
⊢ ↑√(∑ x, y x ^ 2) ^ 2 = ∑ i, ↑(y i) ^ 2 ∨ b = 0
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: case a
d : Type u_1
inst✝ : Fintype d
n : d → ℤ
⊢ 1 ≤ ‖mFourier n‖

Tactic:
· refine (le_of_eq ?_).trans ((mFourier n).norm_coe_le_norm fun _ ↦ 0)
    simp only [mFourier, ContinuousMap.coe_mk, fourier_eval_zero, Finset.prod_const_one,
      CStarRing.norm_one]

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

Goal state before:
pp: E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℂ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℂ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : CompleteSpace F₃
inst✝¹ : CompleteSpace F₁
inst✝ : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ (𝓕⁻ (𝓕 (((convolution B) f) g))) x = 𝓕⁻ (fun y ↦ 𝓕 (⇑f ⋆[B, volume] ⇑g) y) x

Tactic:
rw [fourierInv_coe]

Goal state after:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℂ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℂ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : CompleteSpace F₃
inst✝¹ : CompleteSpace F₁
inst✝ : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ 𝓕⁻ (⇑(𝓕 (((convolution B) f) g))) x = 𝓕⁻ (fun y ↦ 𝓕 (⇑f ⋆[B, volume] ⇑g) y) x
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case right
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 : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
⊢ eLpNorm (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume < ∞

Tactic:
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (by norm_num) (by norm_num)]
      suffices h : ∫⁻ a : E, ENNReal.ofReal ‖(1 + ‖a‖ ^ 2) ^ (-s)‖ < ⊤ from by
        norm_cast
        simp_rw [ofReal_norm] at h
        simp_rw [← enorm_pow]
        convert h
        rw [← Real.rpow_mul_natCast (by positivity)]
        simp
      apply ((integrable_rpow_neg_one_add_norm_sq hs).congr _).lintegral_lt_top
      filter_upwards with x
      rw [Real.norm_eq_abs, abs_eq_self.mpr (by positivity)]
      congr
      ring

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

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

Tactic:
simp_rw [fourierCoeff_eq_intervalIntegral _ m 0, div_one, one_smul, zero_add, e, comp_apply,
        coe_mk, Periodic.lift_coe, zsmul_one, smul_eq_mul]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: 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
this : ∑ d ∈ n.divisors, μ (n / d) • G d = f n
d : ℕ
⊢ d ∈ n.divisors → μ (n / d) • g d = μ (n / d) • G d

Tactic:
hd

Goal state after:
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
this : ∑ d ∈ n.divisors, μ (n / d) • G d = f n
d : ℕ
hd : d ∈ n.divisors
⊢ μ (n / d) • g d = μ (n / d) • G d
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: 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 → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
F : ℕ → R := fun n ↦ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d ∈ n.divisors, F d = g n
d : ℕ
⊢ d ∈ n.divisors → f d = F d

Tactic:
hd

Goal state after:
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 → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
F : ℕ → R := fun n ↦ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d ∈ n.divisors, F d = g n
d : ℕ
hd : d ∈ n.divisors
⊢ f d = F d
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: q : ℚ
h : Odd q.num
⊢ IsPrimitiveRoot (cexp (↑π * I * ↑q)) (2 * q.den)

Tactic:
by
  convert! isPrimitiveRoot_exp_rat (q / 2) using 1
  · push_cast
    ring_nf
  · nth_rw 2 [← q.num_div_den]
    rw [mul_comm, div_div, ← Int.cast_ofNat, ← Int.cast_natCast, ← Int.cast_mul,
      ← Rat.divInt_eq_div, ← Nat.cast_ofNat (R := ℤ), ← Nat.cast_mul,
      ← Rat.mk_eq_divInt (nz := by simp)
        (c := Nat.Coprime.mul_right q.reduced h.natAbs.coprime_two_right)]

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic n R ∣ X ^ n - 1

Tactic:
by
  suffices cyclotomic n ℤ ∣ X ^ n - 1 by
    simpa only [map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
      Polynomial.map_X] using Polynomial.map_dvd (Int.castRingHom R) this
  rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  rw [← prod_cyclotomic_eq_X_pow_sub_one hn]
  exact Finset.dvd_prod_of_mem _ (n.mem_divisors_self hn.ne')

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

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

Tactic:
suffices cyclotomic d ℤ ∣ ∑ i ∈ Finset.range n, X ^ i by
    simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
      map_dvd (Int.castRingHom R) this

Goal state after:
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
⊢ cyclotomic d ℤ ∣ ∑ i ∈ range n, X ^ i
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ #(nthRootsFinset n 1) = n

Tactic:
by
  classical
  rw [nthRootsFinset, ← Multiset.toFinset_eq (nthRoots_one_nodup h), card_mk, h.card_nthRoots_one]

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

Goal state before:
pp: case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ n.totient * p ≤ p.totient * n.totient + n.totient

Tactic:
Nat.totient_prime hp,

Goal state after:
case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ n.totient * p ≤ (p - 1) * n.totient + n.totient
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ n.totient * p ≤ n.totient * p.pred.succ

Tactic:
Nat.succ_pred_eq_of_pos hp.pos

Goal state after:
case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ n.totient * p ≤ n.totient * p
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
⊢ ↑⟨val✝, property✝⟩ ∈ primitiveRoots n C

Tactic:
mem_primitiveRoots (NeZero.pos _),

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
⊢ IsPrimitiveRoot (↑⟨val✝, property✝⟩) n
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
⊢ IsCyclotomicExtension {0} A B ↔ ⊥ = ⊤

Tactic:
refine ⟨?_, fun h ↦ singleton_zero_of_bot_eq_top h⟩

Goal state after:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ IsCyclotomicExtension {0} A B → ⊥ = ⊤
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case refine_1
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)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
⊢ η + 1 - 1 ∈ K⟮η + 1⟯

Tactic:
exact sub_mem (IntermediateField.mem_adjoin_simple_self K (η + 1)) (one_mem _)

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 : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
refine ⟨u.val, u.isUnit, ?_⟩

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₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ a = ↑u * ↑d
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case neg
n : ℕ
x : ℤ
h : IsCoprime x ↑n
hn : ¬n = 0
this : NeZero n
⊢ ↑(↑x).val * (↑(↑x).val)⁻¹ = 1

Tactic:
apply coe_mul_inv_eq_one

Goal state after:
case neg
n : ℕ
x : ℤ
h : IsCoprime x ↑n
hn : ¬n = 0
this : NeZero n
⊢ (↑x).val.Coprime n
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
R'' : Type u_1
inst✝ : CommMonoid R''
φ : AddChar R R'
f : R' →* R''
hφ : φ.IsPrimitive
hf : Function.Injective ⇑f
a : R
ha : a ≠ 0
⊢ (f.compAddChar φ).mulShift a ≠ 1

Tactic:
simpa [DFunLike.ext_iff] using (MonoidHom.compAddChar_injective_right f hf).ne (hφ ha)

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
⊢ ¬ringChar F' ∣ p

Tactic:
rcases CharP.char_is_prime_or_zero F' (ringChar F') with hq | hq

Goal state after:
case inl
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hq : Nat.Prime (ringChar F')
⊢ ¬ringChar F' ∣ p

case inr
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hq : ringChar F' = 0
⊢ ¬ringChar F' ∣ p
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ χ₈ ↑n = χ₈ ↑(n % 8)

Tactic:
by
  rw [← ZMod.intCast_mod n 8, Nat.cast_ofNat]

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 n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
⊢ χ.FactorsThrough (n.gcd m)

Tactic:
refine (factorsThrough_iff_ker_unitsMap (n.gcd_dvd_left m)).mpr fun x hx ↦
    MonoidHom.mem_ker.mpr ?_

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
⊢ (toUnitHom χ) x = 1
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'
⊢ ∀ (c : MulChar R R'), χ₁ * χ₂ * c = χ₁ * (χ₂ * c)

Tactic:
χ₃

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ χ₃ : MulChar R R'
⊢ χ₁ * χ₂ * χ₃ = χ₁ * (χ₂ * χ₃)
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
⊢ (χ ↑x)⁻¹ʳ = χ ↑x

Tactic:
rcases hχ x with (h₀ | h₁ | h₂)

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₀ : χ ↑x = 0
⊢ (χ ↑x)⁻¹ʳ = χ ↑x

case inr.inl
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₁ : χ ↑x = 1
⊢ (χ ↑x)⁻¹ʳ = χ ↑x

case inr.inr
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : χ ↑x = -1
⊢ (χ ↑x)⁻¹ʳ = χ ↑x
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ C = adjoin A {x | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ x ^ n_1 = 1} ↔ C = A[ζ]

pp: case hS
n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ ∀ n_1 ∈ {n}, n_1 ≠ 0 → ∃ r, IsPrimitiveRoot r n_1

Tactic:
· simp only [Set.mem_singleton_iff, exists_eq_left]
    suffices adjoin A {b | n ≠ 0 ∧ b ^ n = 1} = adjoin A {ζ} by rw [this]
    apply le_antisymm
    · refine adjoin_le fun x ⟨_, hx⟩ ↦ ?_
      obtain ⟨k, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx
      exact Subalgebra.pow_mem _ (self_mem_adjoin_singleton A ζ) _
    · exact adjoin_mono <| Set.singleton_subset_iff.mpr ⟨NeZero.ne n, hζ.pow_eq_one⟩

Goal state after:
case hS
n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ ∀ n_1 ∈ {n}, n_1 ≠ 0 → ∃ r, IsPrimitiveRoot r n_1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : Odd n
hχ : χ ^ n = 1
⊢ (χ ^ n) (-1) = 1

Tactic:
hχ

Goal state after:
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : Odd n
hχ : χ ^ n = 1
⊢ 1 (-1) = 1
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⋖ t
⊢ ∃ a ∉ s, insert a s = t

Tactic:
by
  simpa using h.exists_finset_cons

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

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
t₁ t₂ : ℝ
h_inner : ⟪b -ᵥ a, c -ᵥ a⟫ = 0
⊢ dist ((AffineMap.lineMap a b) t₁) ((AffineMap.lineMap a c) t₂) ^ 2 = t₁ ^ 2 * dist a b ^ 2 + t₂ ^ 2 * dist a c ^ 2

Tactic:
have hvec : AffineMap.lineMap a b t₁ -ᵥ AffineMap.lineMap a c t₂ =
              t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a) := by
    rw [AffineMap.lineMap_apply, AffineMap.lineMap_apply, vadd_vsub_vadd_cancel_right]
  rw [dist_eq_norm_vsub V, hvec, norm_sub_sq_real, norm_smul, norm_smul,
      Real.norm_eq_abs, Real.norm_eq_abs, inner_smul_left, inner_smul_right, h_inner]
  simp only [mul_zero, sub_zero, mul_pow, sq_abs, ← dist_eq_norm_vsub' V]

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

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p : P
t : ℝ
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
h : dist ((AffineMap.lineMap a p) 1) ((AffineMap.lineMap a b) t) ^ 2 = 1 ^ 2 * dist a p ^ 2 + t ^ 2 * dist a b ^ 2
⊢ dist p ((AffineMap.lineMap a b) t) ^ 2 = dist p a ^ 2 + t ^ 2 * dist a b ^ 2

Tactic:
simp only [AffineMap.lineMap_apply_one, one_pow, one_mul] at h

Goal state after:
V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p : P
t : ℝ
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
h : dist p ((AffineMap.lineMap a b) t) ^ 2 = dist a p ^ 2 + t ^ 2 * dist a b ^ 2
⊢ dist p ((AffineMap.lineMap a b) t) ^ 2 = dist p a ^ 2 + t ^ 2 * dist a b ^ 2
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
⊢ ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p ≤ (∫⁻ (x : ι → ℝ), ‖fderiv ℝ u x‖ₑ) ^ p

Tactic:
calc ∫⁻ x, ‖u x‖ₑ ^ p
      = ∫⁻ x, (‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ))) ^ (#ι : ℝ) := by
        -- a little algebraic manipulation of the exponent
        congr! 2 with x
        rw [← ENNReal.rpow_mul, hp.conjugate_eq]
        field_simp
    _ = ∫⁻ x, ∏ _i : ι, ‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ)) := by
        -- express the left-hand integrand as a product of identical factors
        congr! 2 with x
        simp_rw [prod_const]
        norm_cast
    _ ≤ ∫⁻ x, ∏ i, (∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ) ^ ((1 : ℝ) / (#ι - 1 : ℝ)) := ?_
    _ ≤ (∫⁻ x, ‖fderiv ℝ u x‖ₑ) ^ p := by
        -- apply the grid-lines lemma
        apply lintegral_prod_lintegral_pow_le _ hp
        fun_prop

Goal state after:
ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
⊢ ∫⁻ (x : ι → ℝ), ∏ _i, ‖u x‖ₑ ^ (1 / (↑#ι - 1)) ≤
    ∫⁻ (x : ι → ℝ), ∏ i, (∫⁻ (xᵢ : ℝ), ‖fderiv ℝ u (update x i xᵢ)‖ₑ) ^ (1 / (↑#ι - 1))
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ∃ s, Nonempty (Module.Basis (↥s) 𝕜 E)
⊢ 0 ≤ (traceAux 𝕜 ⋯.some) f

Tactic:
have : FiniteDimensional 𝕜 E := Module.Finite.of_basis h.choose_spec.some

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ∃ s, Nonempty (Module.Basis (↥s) 𝕜 E)
this : FiniteDimensional 𝕜 E
⊢ 0 ≤ (traceAux 𝕜 ⋯.some) f
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⟫
⊢ Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)

Tactic:
have : Continuous ((innerSL 𝕜 w).comp T.domain.subtypeL) := by fun_prop

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)
⊢ Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

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
x : E ⊗[𝕜] F
E' : Submodule 𝕜 E
F' : Submodule 𝕜 F
iE' : Module.Finite 𝕜 ↥E'
iF' : Module.Finite 𝕜 ↥F'
hz : {x} ⊆ ↑(mapIncl E' F').range
⊢ 0 ≤ RCLike.re (inner 𝕜 x x)

Tactic:
obtain ⟨y, rfl⟩ := Set.singleton_subset_iff.mp hz

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
E' : Submodule 𝕜 E
F' : Submodule 𝕜 F
iE' : Module.Finite 𝕜 ↥E'
iF' : Module.Finite 𝕜 ↥F'
y : ↥E' ⊗[𝕜] ↥F'
hz : {(mapIncl E' F') y} ⊆ ↑(mapIncl E' F').range
⊢ 0 ≤ RCLike.re (inner 𝕜 ((mapIncl E' F') y) ((mapIncl E' F') y))