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

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ R ≤ ‖v‖ - ‖-i w‖

Tactic:
le_sub_iff_add_le,

Goal state after:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ R + ‖-i w‖ ≤ ‖v‖
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
⊢ ∀ (l : ℕ), f ζ ^ l = 1 → k ∣ l

Tactic:
rw [h.eq_orderOf]
    intro l hl
    rw [← map_pow, ← map_one f] at hl
    exact orderOf_dvd_of_pow_eq_one (hf hl)

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

Goal state before:
pp: R : Type u_4
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
hζ : IsPrimitiveRoot ζ k
hk : 1 < k
⊢ ∑ x ∈ range k.pred.succ, ζ ^ x = 0

Tactic:
Nat.succ_pred_eq_of_pos (pos_of_gt hk),

Goal state after:
R : Type u_4
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
hζ : IsPrimitiveRoot ζ k
hk : 1 < k
⊢ ∑ x ∈ range k, ζ ^ x = 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
q : R
n : ℕ
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ eval (f q) (cyclotomic n S) = f (eval q (cyclotomic n R))

Tactic:
← map_cyclotomic n f,

Goal state after:
R : Type u_1
S : Type u_2
q : R
n : ℕ
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ eval (f q) (map f (cyclotomic n R)) = f (eval q (cyclotomic n R))
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg.refine_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
hξ : ξ ∈ primitiveRoots k R
⊢ ∃ a, (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ

Tactic:
rw [mem_primitiveRoots (Nat.pos_of_ne_zero h0), h.isPrimitiveRoot_iff] at hξ

Goal state after:
case neg.refine_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
hξ : ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
⊢ ∃ a, (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ
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✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this✝² : MeasurableSpace V' := borel V'
this✝¹ : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : StrongDual ℝ V ≃L[ℝ] StrongDual ℝ V' := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this✝ : (Measure.map (⇑Aₘ) μ).IsAddHaarMeasure
w : StrongDual ℝ V
this : ∫ (v : V), 𝐞 (-w v) • f v ∂μ = ∫ (x : V), 𝐞 (-w (A.symm (Aₘ x))) • f (A.symm (Aₘ x)) ∂μ
⊢ ∫ (v : V), 𝐞 (-w v) • f v ∂μ =
    ((fun w ↦ ∫ (v : V'), 𝐞 (-w v) • (f ∘ ⇑A.symm) v ∂Measure.map (⇑Aₘ) μ) ∘ Adual.toHomeomorph.toCocompactMap.toFun) w

Tactic:
by
    simpa [Function.comp_apply, integral_map_equiv, Adual]

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
⊢ (cyclotomic 1 R).coeff 0 * ∏ x ∈ n.properDivisors.erase 1, (cyclotomic x R).coeff 0 = -1

Tactic:
cyclotomic_one R

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
⊢ (X - 1).coeff 0 * ∏ x ∈ n.properDivisors.erase 1, (cyclotomic x R).coeff 0 = -1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case h
G : Type u_7
G' : Type u_8
inst✝³ : Group G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot (φ g) (Nat.card G)
ha : φ a = 1
k : ℕ
hk : g ^ k = a
⊢ a = 1

Tactic:
rw [← hk, map_pow] at ha

Goal state after:
case h
G : Type u_7
G' : Type u_8
inst✝³ : Group G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot (φ g) (Nat.card G)
k : ℕ
ha : φ g ^ k = 1
hk : g ^ k = a
⊢ a = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
a : K
ha : a ∈ ↑(nthRootsFinset n 1)
⊢ a ∈ ⇑(algebraMap R K) '' ↑(nthRootsFinset n 1)

Tactic:
have := Set.surj_on_of_inj_on_of_ncard_le (s := nthRootsFinset n (1 : R))
    (t := nthRootsFinset n (1 : K)) _ (fun _ hr ↦ map_mem_nthRootsFinset_one hr _)
    (fun a _ b _ H ↦ FaithfulSMul.algebraMap_injective R K H)
    (by simp [h.card_nthRootsFinset, h'.card_nthRootsFinset])

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
a : K
ha : a ∈ ↑(nthRootsFinset n 1)
this : ∀ b ∈ ↑(nthRootsFinset n 1), ∃ a, ∃ (_ : a ∈ ↑(nthRootsFinset n 1)), b = (algebraMap R K) a
⊢ a ∈ ⇑(algebraMap R K) '' ↑(nthRootsFinset n 1)
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
this : 0 < (fun x ↦ ↑x) (eval (↑(-1)) (cyclotomic n ℤ))
⊢ 0 < eval (↑(-1)) (cyclotomic n ℤ)

Tactic:
simpa only [Int.cast_pos] using this

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

Goal state before:
pp: case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
⊢ eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) ≤ 0

Tactic:
have h2 : 2 ∈ n.properDivisors.erase 1 := by
      rw [Finset.mem_erase, mem_properDivisors]
      exact ⟨by decide, even_iff_two_dvd.mp h.1, hn⟩

Goal state after:
case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
⊢ eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) ≤ 0
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: K : Type u_1
F : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : Field F
inst✝ : Algebra F K
⊢ Algebra.adjoin F ((X ^ Fintype.card K - X).rootSet K) = ⊤

Tactic:
classical
    trans Algebra.adjoin F ((roots (X ^ Fintype.card K - X : K[X])).toFinset : Set K)
    · simp only [rootSet, aroots, Polynomial.map_pow, map_X, Polynomial.map_sub]
    · rw [FiniteField.roots_X_pow_card_sub_X, val_toFinset, coe_univ, Algebra.adjoin_univ]

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

Goal state before:
pp: case refine_1
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
⊢ {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1} ⊆ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}

Tactic:
rintro x ⟨n, hn₁ | hn₂, hnpow⟩
      · left; exact ⟨n, hn₁, hnpow⟩
      · right; exact ⟨n, hn₂, hnpow⟩

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

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)

Tactic:
have hn : 0 < n := pos_of_gt hn'
  have hq := zero_lt_one.trans hq'
  have hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖ := by
    intro ζ' hζ'
    rw [mem_primitiveRoots hn] at hζ'
    convert! norm_sub_norm_le (↑q) ζ'
    · rw [Complex.norm_real, Real.norm_of_nonneg hq.le]
    · rw [hζ'.norm'_eq_one hn.ne']
  let ζ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
  have hζ : IsPrimitiveRoot ζ n := Complex.isPrimitiveRoot_exp n hn.ne'
  have hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖ := by
    refine ⟨ζ, (mem_primitiveRoots hn).mpr hζ, ?_⟩
    suffices ¬SameRay ℝ (q : ℂ) ζ by
      convert! lt_norm_sub_of_not_sameRay this <;>
        simp only [hζ.norm'_eq_one hn.ne', Real.norm_of_nonneg hq.le, Complex.norm_real]
    rw [Complex.sameRay_iff]
    push Not
    refine ⟨mod_cast hq.ne', hζ.ne_zero hn.ne', ?_⟩
    rw [Complex.arg_ofReal_of_nonneg hq.le, Ne, eq_comm, hζ.arg_eq_zero_iff hn.ne']
    clear_value ζ
    rintro rfl
    linarith [hζ.unique IsPrimitiveRoot.one]
  have : ¬eval (↑q) (cyclotomic n ℂ) = 0 := by simpa using (cyclotomic_pos' n hq').ne'
  suffices Units.mk0 (Real.toNNReal (q - 1)) (by simp [hq']) ^ totient n <
      Units.mk0 ‖(cyclotomic n ℂ).eval ↑q‖₊ (by simp_all) by
    simp only [← Units.val_lt_val, Units.val_pow_eq_pow_val, Units.val_mk0, ← NNReal.coe_lt_coe,
      hq'.le, coe_nnnorm, NNReal.coe_pow, Real.coe_toNNReal', sub_nonneg, sup_of_le_left] at this
    convert! this
    rw [eq_comm]
    simp [cyclotomic_nonneg n hq'.le]
  simp only [cyclotomic_eq_prod_X_sub_primitiveRoots hζ, eval_prod, eval_C, eval_X, eval_sub,
    nnnorm_prod, Units.mk0_prod]
  convert! Finset.prod_lt_prod' (M := NNRealˣ) _ _
  swap; · exact fun _ => Units.mk0 (Real.toNNReal (q - 1)) (by simp [hq'])
  · simp only [Complex.card_primitiveRoots, prod_const, card_attach]
  · simp only [Finset.mem_attach, forall_true_left, Subtype.forall, ←
      Units.val_le_val, ← NNReal.coe_le_coe, norm_nonneg, Units.val_mk0,
      Real.coe_toNNReal', coe_nnnorm, max_le_iff, tsub_le_iff_right]
    intro x hx
    simpa only [and_true, tsub_le_iff_right] using hfor x hx
  · simp only [Finset.mem_attach, Subtype.exists, ←
      NNReal.coe_lt_coe, ← Units.val_lt_val, Units.val_mk0 _, coe_nnnorm]
    simpa [hq'.le, Real.coe_toNNReal', max_eq_left, sub_nonneg] using hex

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

Goal state before:
pp: K : Type w
L : Type z
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsIntegral K L
n : ℕ
inst✝ : NeZero n
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension {n} K ↥K[ζ]

Tactic:
exact hζ.adjoin_isCyclotomicExtension K

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

Goal state before:
pp: F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Finite L
inst✝ : Finite K
h : Module.finrank F K ∣ Module.finrank F L
⊢ Nat.card (K →ₐ[F] L) = Module.finrank F K

Tactic:
natCard_algHom_of_finrank_dvd h

Goal state after:
F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Finite L
inst✝ : Finite K
h : Module.finrank F K ∣ Module.finrank F L
⊢ Module.finrank F K = Module.finrank F K
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 4 = 1
⊢ χ₄ ↑n = 1

Tactic:
by
  rw [χ₄_nat_mod_four, hn]
  rfl

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

Goal state before:
pp: n : ℕ
hn : n % 4 = 3
⊢ χ₄ ↑n = -1

Tactic:
by
  rw [χ₄_nat_mod_four, hn]
  rfl

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

Goal state before:
pp: R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
a✝ : Nontrivial R
ha : ¬IsUnit a
⊢ 0 = χ 0

Tactic:
MulChar.map_zero χ

Goal state after:
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
a✝ : Nontrivial R
ha : ¬IsUnit a
⊢ 0 = 0
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:
by
  refine (factorsThrough_iff_ker_unitsMap (n.gcd_dvd_left m)).mpr fun x hx ↦
    MonoidHom.mem_ker.mpr ?_
  rw [Units.ext_iff, MulChar.coe_toUnitHom, Units.val_one]
  obtain ⟨z, hz₁, hz₂⟩ : ∃ z : ℕ, z = x.val ∧ (z : ZMod m) = 1 := by
    suffices x.val.val ≡ 1 [MOD n.gcd m] by
      obtain ⟨z, hz₁, hz₂⟩ := Nat.chineseRemainder' this
      refine ⟨z, ?_, ?_⟩
      · simpa [← ZMod.natCast_eq_natCast_iff] using hz₁
      · rwa [← ZMod.natCast_eq_natCast_iff, Nat.cast_one] at hz₂
    rwa [MonoidHom.mem_ker, Units.ext_iff, ZMod.unitsMap_val, ← ZMod.natCast_val,
      Units.val_one, ← Nat.cast_one, ZMod.natCast_eq_natCast_iff] at hx
  have hz₀ : z.gcd (n * m) = 1 := by
    refine Nat.Coprime.mul_right ?_ ?_
    · exact (ZMod.isUnit_iff_coprime _ _).mp <| hz₁ ▸ x.isUnit
    · exact (ZMod.isUnit_iff_coprime _ _).mp <| hz₂ ▸ isUnit_one
  have := changeLevel_eq_cast_of_dvd χ (n.dvd_mul_right m) (ZMod.unitOfCoprime z hz₀)
  simp only [ZMod.coe_unitOfCoprime, dvd_mul_right, ZMod.cast_natCast] at this
  rw [← hz₁, ← this, h]
  have := changeLevel_eq_cast_of_dvd ψ (m.dvd_mul_left n) (ZMod.unitOfCoprime z hz₀)
  simp only [ZMod.coe_unitOfCoprime, dvd_mul_left, ZMod.cast_natCast] at this
  rw [this, hz₂, map_one]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝³ : Field R
inst✝² : Fintype R
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
⊢ ∑ a ∈ {0}ᶜ, ψ a + ψ 0 = 0

Tactic:
← AddChar.sum_eq_zero_of_ne_one hψ,

Goal state after:
R : Type u_1
R' : Type u_2
inst✝³ : Field R
inst✝² : Fintype R
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
⊢ ∑ a ∈ {0}ᶜ, ψ a + ψ 0 = ∑ a, ψ a
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
| ∑ i, ∑ j, χ i * ψ i * (φ j * ψ j) = ∑ t, ∑ x, χ x * φ (t - x) * ψ t

Tactic:
enter [1, 2, x, 2, x_1]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x x_1 : R
| χ x * ψ x * (φ x_1 * ψ x_1)
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:
exact .inr <| hab.trans' <| h.isTop ⟨c, hc⟩

Goal state after:
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
⊢ ∀ ⦃x : Multiset α⦄, x ∈ Set.range val → ∀ ⦃y : Multiset α⦄, y ∈ Set.range val → Set.Icc x y ⊆ Set.range val

Tactic:
rintro _ _ _ ⟨s, rfl⟩ t ht

Goal state after:
α : Type u_1
x✝ : Multiset α
hx✝ : x✝ ∈ Set.range val
s : Finset α
t : Multiset α
ht : t ∈ Set.Icc x✝ s.val
⊢ t ∈ Set.range val
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
⊢ ∀ ⦃x : Set α⦄,
    x ∈ Set.range SetLike.coe → ∀ ⦃y : Set α⦄, y ∈ Set.range SetLike.coe → Set.Icc x y ⊆ Set.range SetLike.coe

Tactic:
rintro _ _ _ ⟨s, rfl⟩ t ht

Goal state after:
α : Type u_1
x✝ : Set α
hx✝ : x✝ ∈ Set.range SetLike.coe
s : Finset α
t : Set α
ht : t ∈ Set.Icc x✝ ↑s
⊢ t ∈ Set.range SetLike.coe
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
ha : a ∉ s
⊢ s ⋖ cons a s ha

Tactic:
simp [← val_covBy_val]

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

Goal state before:
pp: 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)⁻¹
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂μ) ^ p

Tactic:
have hC : C * c ^ p = c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p := by
    rw [h0C, inv_mul_cancel_right₀ (NNReal.rpow_pos hc).ne']

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
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂μ) ^ p
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: 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
⊢ ↑c * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (⇑e.symm) volume ≤
    ↑C * (↑c * ∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂Measure.map (⇑e.symm) volume) ^ p

Tactic:
have hv : ContDiff ℝ 1 v := hu.comp e.symm.contDiff

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
⊢ ↑c * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (⇑e.symm) volume ≤
    ↑C * (↑c * ∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂Measure.map (⇑e.symm) volume) ^ p
Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : LipschitzWith 1 ⇑f
g : E →L[𝕜] ↥(f.eqLocus 1)
hg_proj : ∀ (x : ↥(f.eqLocus 1)), g ↑x = x
hg_ker : ↑(↑g).ker ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(f - 1).range
x : E
⊢ Tendsto (fun x_1 ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 ↑(g x))

Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ : ∃ y, g y = 0 ∧ ∃ z, IsFixedPt f z ∧ x = y + z :=
    ⟨x - g x, by simp [hg_proj], g x, (g x).2, by simp⟩
  /- For a fixed point, the theorem is trivial,
  so it suffices to prove it for `y ∈ LinearMap.ker g`. -/
  suffices Tendsto (birkhoffAverage 𝕜 f _root_.id · y) atTop (𝓝 0) by
    have hgz : g z = z := congr_arg Subtype.val (hg_proj ⟨z, hz⟩)
    simpa [hy, hgz, birkhoffAverage, birkhoffSum, Finset.sum_add_distrib, smul_add]
      using this.add (hz.tendsto_birkhoffAverage 𝕜 _root_.id)
  /- By continuity, it suffices to prove the theorem on a dense subset of `LinearMap.ker g`.
  By assumption, `LinearMap.range (f - 1)` is dense in the kernel of `g`,
  so it suffices to prove the theorem for `y = f x - x`. -/
  have : IsClosed {x | Tendsto (birkhoffAverage 𝕜 f _root_.id · x) atTop (𝓝 0)} :=
    isClosed_setOfPred_tendsto_birkhoffAverage 𝕜 hf uniformContinuous_id continuous_const
  refine closure_minimal (Set.forall_mem_range.2 fun x ↦ ?_) this (hg_ker hy)
  /- Finally, for `y = f x - x` the average is equal to the difference between averages
  along the orbits of `f x` and `x`, and most of the terms cancel. -/
  have : IsBounded (Set.range (_root_.id <| f^[·] x)) :=
    isBounded_iff_forall_norm_le.2 ⟨‖x‖, Set.forall_mem_range.2 fun n ↦ by
      have H : f^[n] 0 = 0 := iterate_map_zero (f : E →+ E) n
      simpa [H] using (hf.iterate n).dist_le_mul x 0⟩
  have H : ∀ n x y, f^[n] (x - y) = f^[n] x - f^[n] y := iterate_map_sub (f : E →+ E)
  simpa [birkhoffAverage, birkhoffSum, Finset.sum_sub_distrib, smul_sub, H]
    using tendsto_birkhoffAverage_apply_sub_birkhoffAverage 𝕜 this

Goal state after: