mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
⊢ ((Pi.map fun x ↦ ↑polarCoord.symm) '' Set.univ.pi fun x ↦ polarCoord.target) =ᵐ[volume] Set.univ

Tactic:
by
  rw [Set.piMap_image_univ_pi, polarCoord.symm_image_target_eq_source, volume_pi, ← Set.pi_univ]
  exact ae_eq_set_pi fun _ _ ↦ polarCoord_source_ae_eq_univ

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

Goal state before:
pp: s : ℝ
⊢ (∃ m, s = -↑m) → Gamma s = 0

Tactic:
rintro ⟨m, rfl⟩; exact Gamma_neg_nat_eq_zero m

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

Goal state before:
pp: s : ℝ
⊢ (∃ m, s = -↑m) → Gamma s = 0

Tactic:
by rintro ⟨m, rfl⟩; exact Gamma_neg_nat_eq_zero m

Goal state after:
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
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
⊢ Tendsto (fun c ↦ ∫ (w : V), ((↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w) atTop
    (𝓝 (f v))

Tactic:
have A : Tendsto (fun (c : ℝ) ↦ ∫ w : V, (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
      atTop (𝓝 (f v)) := by
    apply tendsto_integral_comp_smul_smul_of_integrable'
    · exact fun x ↦ by positivity
    · rw [integral_const_mul, GaussianFourier.integral_rexp_neg_mul_sq_norm (by positivity)]
      nth_rewrite 2 [← pow_one π]
      rw [← rpow_natCast, ← rpow_natCast, ← rpow_sub pi_pos, ← rpow_mul pi_nonneg,
        ← rpow_add pi_pos]
      ring_nf
      exact rpow_zero _
    · have A : Tendsto (fun (w : V) ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop := by
        rw [tendsto_const_mul_atTop_of_pos (by positivity)]
        apply (tendsto_pow_atTop two_ne_zero).comp tendsto_norm_cobounded_atTop
      have B := tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (finrank ℝ V / 2) 1
        zero_lt_one |>.comp A |>.const_mul (π ^ (-finrank ℝ V / 2 : ℝ))
      rw [mul_zero] at B
      convert! B using 2 with x
      simp only [neg_mul, one_mul, Function.comp_apply, ← mul_assoc, ← rpow_natCast, φ]
      congr 1
      rw [mul_rpow (by positivity) (by positivity), ← rpow_mul pi_nonneg,
        ← rpow_mul (norm_nonneg _), ← mul_assoc, ← rpow_add pi_pos, mul_comm]
      congr <;> ring
    · exact hf
    · exact h'f

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
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun c ↦ ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))
⊢ Tendsto (fun c ↦ ∫ (w : V), ((↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w) atTop
    (𝓝 (f v))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))
⊢ ∫ (x : ℝ), cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b)) =
    (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))

Tactic:
MeasureTheory.integral_mul_const

Goal state after:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))
⊢ (∫ (a : ℝ), cexp (- -b * (↑a + c / (2 * b)) ^ 2)) * cexp (d - c ^ 2 / (4 * b)) =
    (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
b : ℝ
hb : 0 < b
⊢ ∫ (v : V), rexp (-b * ‖v‖ ^ 2) = (π / b) ^ (↑(Module.finrank ℝ V) / 2)

Tactic:
by
  rw [← ofReal_inj]
  convert! integral_cexp_neg_mul_sq_norm (show 0 < (b : ℂ).re from hb) (V := V)
  · change ofRealLI (∫ (v : V), rexp (-b * ‖v‖ ^ 2)) = ∫ (v : V), cexp (-↑b * ↑‖v‖ ^ 2)
    rw [← ofRealLI.integral_comp_comm]
    simp [ofRealLI]
  · rw [← ofReal_div, ofReal_cpow (by positivity)]
    simp

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

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

Tactic:
change f ∈ (charAlgHom he hL).range ↔ _
  simp [BoundedContinuousFunction.ext_iff, funext_iff, eq_comm]

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‖
n : ℤ
x : ℝ
⊢ (e.comp (ContinuousMap.addRight ↑n)) x = e x

Tactic:
have : Periodic e 1 := Periodic.comp (fun x => AddCircle.coe_add_period 1 x) (fourier (-m))

Goal state after:
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‖
n : ℤ
x : ℝ
this : Periodic (⇑e) 1
⊢ (e.comp (ContinuousMap.addRight ↑n)) x = e x
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: f : C(ℝ, ℂ)
h_norm : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n ↦ 𝓕 ⇑f ↑n
x : ℝ
F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }
x✝ : ℤ
⊢ fourierCoeff (⇑F) x✝ = 𝓕 ⇑f ↑x✝

Tactic:
exact Real.fourierCoeff_tsum_comp_add h_norm _

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

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
⊢ cexp (-(↑π * I)) = (-1)⁻¹

Tactic:
exp_neg,

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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
⊢ (cexp (↑π * I))⁻¹ = (-1)⁻¹
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ (X ^ n - C 1).Splits

Tactic:
rw [splits_iff_card_roots, ← nthRoots, IsPrimitiveRoot.card_nthRoots_one h, natDegree_X_pow_sub_C]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℂˣ
⊢ x ^ n = 1 ↔ ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

Tactic:
Units.ext_iff,

Goal state after:
n : ℕ
inst✝ : NeZero n
x : ℂˣ
⊢ ↑(x ^ n) = ↑1 ↔ ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ minpoly ℤ μ ∣ cyclotomic n ℤ

Tactic:
by
  apply minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos)
  simpa [aeval_def, eval₂_eq_eval_map, IsRoot.def] using h.isRoot_cyclotomic hpos

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
⊢ (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0

Tactic:
rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ←
      Nat.cons_self_properDivisors hn.ne_bot, Finset.prod_cons, mul_coeff_zero, coeff_zero_prod,
      hprod, mul_neg, mul_one]

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

Goal state before:
pp: n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : eval ((Nat.castRingHom (ZMod p)) a) (cyclotomic n (ZMod p)) = 0
⊢ eval ((Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0

Tactic:
rw [← prod_cyclotomic_eq_X_pow_sub_one hpos (ZMod p), ← Nat.cons_self_properDivisors hpos.ne',
    Finset.prod_cons, eval_mul, hroot, zero_mul]

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

Goal state before:
pp: n : ℕ
hn : 2 < n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
this : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
⊢ False

Tactic:
have := intermediate_value_univ (-1) 0 (cyclotomic n ℝ).continuous

Goal state after:
n : ℕ
hn : 2 < n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
this✝ : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun x ↦ eval x (cyclotomic n ℝ)
⊢ False
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
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) * cyclotomic n (ZMod p) = (expand (ZMod p) p) (cyclotomic n (ZMod p))

Tactic:
conv_rhs => rw [← map_cyclotomic_int]

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) (ZMod p) * cyclotomic n (ZMod p) =
    (expand (ZMod p) p) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

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

Tactic:
rw [pow_one, Nat.sub_self, pow_zero, mul_comm, cyclotomic_mul_prime_eq_pow_of_not_dvd R hm]

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

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

Tactic:
cyclotomic_mul_prime_dvd_eq_pow R hdiv,

Goal state after:
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ a.succ * m
⊢ cyclotomic (p ^ a.succ * m) R ^ p = cyclotomic m R ^ (p * p ^ (a + 1) - p ^ (a + 2 - 1))
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
⊢ ↑q ≠ 0 ∧ -ζ ≠ 0 ∧ (↑q).arg ≠ (-ζ).arg

Tactic:
refine ⟨mod_cast hq.ne', neg_ne_zero.mpr <| hζ.ne_zero hn.ne', ?_⟩

Goal state after:
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
⊢ (↑q).arg ≠ (-ζ).arg
Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

Goal state before:
pp: case h
n : ℕ
inst✝² : NeZero n
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
hm✝ : HasEnoughRootsOfUnity M n
e : ↥(rootsOfUnity n M) ≃* ↥(rootsOfUnity n N)
m : M
hm : IsPrimitiveRoot m n
⊢ IsPrimitiveRoot (↑(e hm.toRootsOfUnity)) n

Tactic:
IsPrimitiveRoot.coe_submonoidClass_iff

Goal state after:
case h
n : ℕ
inst✝² : NeZero n
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
hm✝ : HasEnoughRootsOfUnity M n
e : ↥(rootsOfUnity n M) ≃* ↥(rootsOfUnity n N)
m : M
hm : IsPrimitiveRoot m n
⊢ IsPrimitiveRoot (e hm.toRootsOfUnity) n
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
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
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this✝¹ : NeZero ↑n
k : K
this✝ : ∀ (z : K), ∃ x, z * (algebraMap A K) ↑x.2 = (algebraMap A K) x.1
z : A
w : ↥(nonZeroDivisors A)
hw : k * (algebraMap A K) ↑(z, w).2 = (algebraMap A K) (z, w).1
this : IsScalarTower A K (CyclotomicField n K) := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ (algebraMap K (CyclotomicField n K)) k *
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
        ↑((algebraMap A (CyclotomicRing n A K)) z, ⟨(algebraMap A (CyclotomicRing n A K)) ↑w, ⋯⟩).2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
      ((algebraMap A (CyclotomicRing n A K)) z, ⟨(algebraMap A (CyclotomicRing n A K)) ↑w, ⋯⟩).1

Tactic:
← IsScalarTower.algebraMap_apply,

Goal state after:
case refine_2
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
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this✝¹ : NeZero ↑n
k : K
this✝ : ∀ (z : K), ∃ x, z * (algebraMap A K) ↑x.2 = (algebraMap A K) x.1
z : A
w : ↥(nonZeroDivisors A)
hw : k * (algebraMap A K) ↑(z, w).2 = (algebraMap A K) (z, w).1
this : IsScalarTower A K (CyclotomicField n K) := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ (algebraMap K (CyclotomicField n K)) k * (algebraMap A (CyclotomicField n K)) ↑w =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
      ((algebraMap A (CyclotomicRing n A K)) z, ⟨(algebraMap A (CyclotomicRing n A K)) ↑w, ⋯⟩).1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
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
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this✝¹ : NeZero ↑n
k : K
this✝ : ∀ (z : K), ∃ x, z * (algebraMap A K) ↑x.2 = (algebraMap A K) x.1
z : A
w : ↥(nonZeroDivisors A)
hw : k * (algebraMap A K) ↑(z, w).2 = (algebraMap A K) (z, w).1
this : IsScalarTower A K (CyclotomicField n K) := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ (algebraMap K (CyclotomicField n K)) k * (algebraMap A (CyclotomicField n K)) ↑w =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
      ((algebraMap A (CyclotomicRing n A K)) z, ⟨(algebraMap A (CyclotomicRing n A K)) ↑w, ⋯⟩).1

Tactic:
← IsScalarTower.algebraMap_apply,

Goal state after:
case refine_2
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
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this✝¹ : NeZero ↑n
k : K
this✝ : ∀ (z : K), ∃ x, z * (algebraMap A K) ↑x.2 = (algebraMap A K) x.1
z : A
w : ↥(nonZeroDivisors A)
hw : k * (algebraMap A K) ↑(z, w).2 = (algebraMap A K) (z, w).1
this : IsScalarTower A K (CyclotomicField n K) := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ (algebraMap K (CyclotomicField n K)) k * (algebraMap A (CyclotomicField n K)) ↑w =
    (algebraMap A (CyclotomicField n K)) z
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 ⋯) ψ
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
⊢ (toUnitHom χ) x = 1

Tactic:
Units.ext_iff,

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.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 ⋯) ψ
x : (ZMod n)ˣ
hx : (ZMod.unitsMap ⋯) x = 1
⊢ (↑x).val ≡ 1 [MOD n.gcd m]

Tactic:
Units.ext_iff,

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 : ↑((ZMod.unitsMap ⋯) x) = ↑1
⊢ (↑x).val ≡ 1 [MOD n.gcd m]
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
a : F
ha : a ≠ 0
hu : IsUnit (χ a)
⊢ hu.unit ^ orderOf χ = 1

Tactic:
Units.ext_iff,

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
a : F
ha : a ≠ 0
hu : IsUnit (χ a)
⊢ ↑(hu.unit ^ orderOf χ) = ↑1
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: case inr
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : ζ ^ n = 1
hζ₂ : ↑ζ = χ a
⊢ χ a ∈ ℤ[μ]

Tactic:
Units.ext_iff,

Goal state after:
case inr
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : ↑(ζ ^ n) = ↑1
hζ₂ : ↑ζ = χ a
⊢ χ a ∈ ℤ[μ]
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
a : ℤ
ha : IsCoprime a ↑n
⊢ χ.primitiveCharacter ↑a = χ ↑a

Tactic:
← changeLevel_eq_cast_of_dvd' χ.primitiveCharacter χ.conductor_dvd_level ha,

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
a : ℤ
ha : IsCoprime a ↑n
⊢ ((changeLevel ⋯) χ.primitiveCharacter) ↑a = χ ↑a
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : Fintype Mˣ
χ : MulChar M R
a✝ : Mˣ
⊢ (χ ^ Fintype.card Mˣ) ↑a✝ = 1 ↑a✝

Tactic:
pow_apply_coe,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : Fintype Mˣ
χ : MulChar M R
a✝ : Mˣ
⊢ χ ↑a✝ ^ Fintype.card Mˣ = 1 ↑a✝
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℤ
hn : NeZero n
⊢ χ ^ m = (changeLevel ⋯) (χ.primitiveCharacter ^ m)

Tactic:
rw [MonoidHom.map_zpow, changeLevel_primitiveCharacter]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝ : NeZero n
d : ℕ
a✝ b✝ : DirichletCharacter R n
hχ : a✝ ∈ {χ | d.Coprime χ.conductor}
hψ : b✝ ∈ {χ | d.Coprime χ.conductor}
⊢ d.Coprime (a✝.conductor.lcm b✝.conductor)

Tactic:
exact (Nat.Coprime.mul_right hχ hψ).coprime_div_right <| Nat.gcd_dvd_mul _ _

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
H : Set (ZMod n)ˣ
χ : DirichletCharacter R n
h : ∀ x ∈ Submonoid.closure H, χ ↑x = 1
u : (↥(Submonoid.map (Units.coeHom (ZMod n)) (Submonoid.closure H)))ˣ
⊢ χ ↑↑u = 1

Tactic:
· obtain ⟨y, hy, hyu⟩ := Submonoid.mem_map.mp u.val.prop
    exact hyu ▸ h _ hy

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 (fun x ↦ ‖fderiv ℝ (fun x ↦ ‖x‖ ^ p) x‖) (𝓝 0) (𝓝 0)

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le (tendsto_const_nhds) ?_
      (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_fderiv_norm_id_rpow _ hp |>.le)

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 (fun x ↦ p * ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ f : ZMod N → ℂ
hf : Function.Even f
⊢ Function.Even (𝓕 f)

Tactic:
simp only [Function.Even, ← congr_fun (dft_comp_neg f), funext hf, implies_true]

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ T μ p f (insert i s) = ∫⋯∫⁻_insert i s, f ^ (1 - ↑(#s) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) ^ p ∂μ

Tactic:
simp_rw [T, card_insert_of_notMem hi]
          congr!
          push_cast
          ring

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : p.IsSymmetricProjection
hq : q.IsSymmetricProjection
x✝ : p ≤ q
a : E
ha : a ∈ p.range
h1 : (q - p).IsSymmetric
h2 : 0 ≤ re ⟪(q - p) a, a⟫
hh : ∀ {T : E →ₗ[𝕜] E}, T.IsSymmetricProjection → re ⟪T a, a⟫ = ‖T a‖ ^ 2
⊢ a ∈ q.range

Tactic:
sub_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : p.IsSymmetricProjection
hq : q.IsSymmetricProjection
x✝ : p ≤ q
a : E
ha : a ∈ p.range
h1 : (q - p).IsSymmetric
h2 : 0 ≤ re ⟪q a - p a, a⟫
hh : ∀ {T : E →ₗ[𝕜] E}, T.IsSymmetricProjection → re ⟪T a, a⟫ = ‖T a‖ ^ 2
⊢ a ∈ q.range
Module: Mathlib.Analysis.InnerProductSpace.ExteriorPower

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
I : Type u_2
inst✝¹ : Fintype I
inst✝ : LinearOrder I
b : OrthonormalBasis I ℝ E
n : ℕ
⊢ Orthonormal ℝ ⇑(Module.Basis.exteriorPower n b.toBasis)

Tactic:
by
    rw [orthonormal_iff_ite]
    intro i j
    rw [exteriorPower.coe_basis, OrthonormalBasis.coe_toBasis]
    exact exteriorPower.innerProductForm_ιMulti_family_of_orthonormal b.orthonormal i j

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
hf : f.toFun.ker = ⊥
⊢ f.inverse.IsClosed ↔ f.IsClosed

Tactic:
rw [IsClosed, inverse_graph hf]

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
hf : f.toFun.ker = ⊥
⊢ IsClosed[instTopologicalSpaceProd] ↑(Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph) ↔ f.IsClosed