mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ IsZeroAtImInfty ((c • f.toSlashInvariantForm).toFun ∣[k] g)

Tactic:
simp_rw [IsZeroAtImInfty, Filter.ZeroAtFilter, SlashInvariantForm.toFun_eq_coe,
        FunLike.coe_smul, toSlashInvariantForm_coe, ← smul_one_smul ℂ c ⇑f,
        smul_slash]
      exact (f.zero_at_cusps' hc g hg).smul _

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℍ → E
a : ℝ
ha : a > 0
ha' : f =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)
⊢ IsZeroAtImInfty f

Tactic:
refine ha'.trans_tendsto <| (Real.tendsto_exp_atBot.comp ?_).comp tendsto_comap

Goal state after:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℍ → E
a : ℝ
ha : a > 0
ha' : f =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)
⊢ Tendsto (HMul.hMul (-a)) atTop atBot
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
this✝ : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI : c = ↑UpperHalfPlane.I ^ k * c
h2I2 : c = ↑(⟨2, ⋯⟩ • UpperHalfPlane.I) ^ k * c
this : 2 ^ k = 1 ↔ k = 0
⊢ k = 0 ∨ c = 0

Tactic:
simpa [mul_zpow, zpow_ne_zero, this] using h2I2.symm.trans hI

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: case h.left
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
⊢ ↑r * x ∈ gammaSet 1 r 0

pp: case h.right
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
⊢ ↑r * x / ↑r = x

Tactic:
· rw [mem_gammaSet_one, Int.isCoprime_iff_gcd_eq_one] at hx
      exact ⟨Subsingleton.eq_zero _, by simp [Int.gcd_mul_left, hx]⟩

Goal state after:
case h.right
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
⊢ ↑r * x / ↑r = x
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: case h.right
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
⊢ ↑r * x / ↑r = x

Tactic:
ext i
      simp_all [NeZero.ne r]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case e'_7
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
this : (f ∘ ↑ofComplex) =O[I∞] (1 ∘ ↑ofComplex)
x✝ : ℍ
⊢ f x✝ - valueAtInfty f =
    ((fun z ↦ (f ∘ ↑ofComplex) z - Periodic.cuspFunction h (f ∘ ↑ofComplex) 0) ∘ UpperHalfPlane.coe) x✝

Tactic:
simpa [cuspFunction] using
    (cuspFunction_apply_zero hh (analyticAt_cuspFunction_zero hh hfper hfhol hfbdd) hfper).symm

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
⊢ ‖f τ‖ ≤ √C / τ.im ^ (↑k / 2)

Tactic:
← sq_le_sq₀ (by positivity) (by positivity),

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
⊢ ‖f τ‖ ^ 2 ≤ (√C / τ.im ^ (↑k / 2)) ^ 2
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h : 0 < ‖↑τ.im ^ ↑k‖
⊢ ‖f τ‖ ≤ √C * max 1 (1 / τ.im ^ ↑k)

Tactic:
← sq_le_sq₀ (by positivity) (by positivity),

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h : 0 < ‖↑τ.im ^ ↑k‖
⊢ ‖f τ‖ ^ 2 ≤ (√C * max 1 (1 / τ.im ^ ↑k)) ^ 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic

Goal state before:
pp: k : ℤ
N : ℕ
inst✝ : NeZero N
hk : 3 ≤ k
a : Fin 2 → ZMod N
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ c.IsBoundedAt (⇑(eisensteinSeriesSIF a k)) k

Tactic:
rw [OnePoint.isBoundedAt_iff_forall_SL2Z hc]

Goal state after:
k : ℤ
N : ℕ
inst✝ : NeZero N
hk : 3 ≤ k
a : Fin 2 → ZMod N
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ ∀ (γ : SL(2, ℤ)),
    (Matrix.SpecialLinearGroup.mapGL ℝ) γ • OnePoint.infty = c →
      UpperHalfPlane.IsBoundedAtImInfty (⇑(eisensteinSeriesSIF a k) ∣[k] γ)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case neg
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
h0 : ↑b * ↑z + ↑n + 1 ≠ 0
⊢ (↑b * ↑z + ↑n + 1)⁻¹ * ((↑b * ↑z + ↑n) ^ 2)⁻¹ + δ ![b, n] + ((↑b * ↑z + ↑n)⁻¹ - (↑b * ↑z + ↑n + 1)⁻¹) =
    ((↑b * ↑z + ↑n) ^ 2)⁻¹

Tactic:
have h1 : (b : ℂ) * z + n ≠ 0 := linear_ne_zero (cd := ![b, n]) z (by aesop)

Goal state after:
case neg
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
h0 : ↑b * ↑z + ↑n + 1 ≠ 0
h1 : ↑b * ↑z + ↑n ≠ 0
⊢ (↑b * ↑z + ↑n + 1)⁻¹ * ((↑b * ↑z + ↑n) ^ 2)⁻¹ + δ ![b, n] + ((↑b * ↑z + ↑n)⁻¹ - (↑b * ↑z + ↑n + 1)⁻¹) =
    ((↑b * ↑z + ↑n) ^ 2)⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable

Goal state before:
pp: ⊢ MDiff E2

Tactic:
UpperHalfPlane.mdifferentiable_iff

Goal state after:
⊢ DifferentiableOn ℂ (E2 ∘ ↑ofComplex) {z | 0 < z.im}
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F : ℍ → ℂ
hF : MDiff F
⊢ MDiff (D F)

Tactic:
UpperHalfPlane.mdifferentiable_iff

Goal state after:
F : ℍ → ℂ
hF : DifferentiableOn ℂ (F ∘ ↑ofComplex) {z | 0 < z.im}
⊢ DifferentiableOn ℂ (D F ∘ ↑ofComplex) {z | 0 < z.im}
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝¹ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this✝ : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
this : S • ρ = T • ρ
⊢ -S • ρ = 1 +ᵥ ρ

Tactic:
SL_neg_smul,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝¹ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this✝ : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
this : S • ρ = T • ρ
⊢ S • ρ = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ serreDerivative k (F + G) z = (serreDerivative k F + serreDerivative k G) z

Tactic:
simp [serreDerivative, normalizedDerivOfComplex_add F G hF hG]

Goal state after:
k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ D F z + D G z - k * 12⁻¹ * EisensteinSeries.E2 z * (F z + G z) =
    D F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z + (D G z - k * 12⁻¹ * EisensteinSeries.E2 z * G z)
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
z : ℍ
⊢ (serreDerivative (↑k) F ∣[k + 2] γ) z = serreDerivative (↑k) (F ∣[k] γ) z

Tactic:
have hLHS : (serreDerivative (k : ℂ) F ∣[k + 2] γ) z =
      (D F ∣[k + 2] γ) z - ↑k * 12⁻¹ * ((EisensteinSeries.E2 ∣[(2 : ℤ)] γ) z * (F ∣[k] γ) z) := by
    grind [ModularForm.SL_slash_apply, serreDerivative_apply, Pi.mul_apply,
      congrFun (ModularForm.mul_slash_SL2 2 k γ EisensteinSeries.E2 F) z]

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
z : ℍ
hLHS :
  (serreDerivative (↑k) F ∣[k + 2] γ) z =
    (D F ∣[k + 2] γ) z - ↑k * 12⁻¹ * ((EisensteinSeries.E2 ∣[2] γ) z * (F ∣[k] γ) z)
⊢ (serreDerivative (↑k) F ∣[k + 2] γ) z = serreDerivative (↑k) (F ∣[k] γ) z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: ⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
UpperHalfPlane.mdifferentiable_iff

Goal state after:
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : f =O[atTop] fun n ↦ ↑n ^ l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace ↑K
c : C(↑K, ℂ) := { toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
n : ℕ
z : ℂ
hz : z ∈ K
h0 : ‖cexp (2 * ↑π * I * z / ↑p)‖ ^ n ≤ ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ ^ n
hr : ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ < 1
⊢ ‖cexp (2 * ↑π * I * ↑n * z / ↑p)‖ = ‖cexp (2 * ↑π * I * z / ↑p) ^ n‖

Tactic:
← exp_nsmul'

Goal state after:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : f =O[atTop] fun n ↦ ↑n ^ l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace ↑K
c : C(↑K, ℂ) := { toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
n : ℕ
z : ℂ
hz : z ∈ K
h0 : ‖cexp (2 * ↑π * I * z / ↑p)‖ ^ n ≤ ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ ^ n
hr : ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ < 1
⊢ ‖cexp (2 * ↑π * I * ↑n * z / ↑p)‖ = ‖cexp (2 * ↑π * I * ↑n * z / ↑p)‖
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this✝¹ : T • z ≠ z
this✝ : T⁻¹ • z ≠ z
this : ↑z ≠ -↑I
hzI : (-↑z)⁻¹ * 1 = ↑z
⊢ z = I

Tactic:
inv_mul_eq_iff_eq_mul₀ (neg_ne_zero.mpr z.ne_zero),

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this✝¹ : T • z ≠ z
this✝ : T⁻¹ • z ≠ z
this : ↑z ≠ -↑I
hzI : 1 = -↑z * ↑z
⊢ z = I
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mpr
g : SL(2, ℤ)
⊢ (S * T) • ρ = ρ ∧ ρ = -S • T • ρ

Tactic:
SL_neg_smul,

Goal state after:
case mpr
g : SL(2, ℤ)
⊢ (S * T) • ρ = ρ ∧ ρ = S • T • ρ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
⊢ DifferentiableAt ℂ jacobiTheta τ

Tactic:
funext jacobiTheta_eq_jacobiTheta₂

Goal state after:
τ : ℂ
hτ : 0 < τ.im
⊢ DifferentiableAt ℂ (jacobiTheta₂ 0) τ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mp
y : ℝ
z : ℂ
⊢ z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y → z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

pp: case mpr
y : ℝ
z : ℂ
⊢ z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} → z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y

Tactic:
· rintro ⟨⟨z, hz⟩, h, rfl⟩
    exact ⟨hz.le, h.2, h.1.2, by simpa [Complex.normSq_eq_norm_sq] using h.1.1⟩

Goal state after:
case mpr
y : ℝ
z : ℂ
⊢ z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} → z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ IsBoundedAtImInfty ((SlashInvariantForm.trace ℋ f).toFun ∣[k] γ)

Tactic:
rw [SlashInvariantForm.trace, IsBoundedAtImInfty, Filter.BoundedAtFilter,
      SlashAction.sum_slash, Finset.sum_fn]

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ (fun a ↦ ∑ c, (quotientFunc f c ∣[k] γ) a) =O[atImInfty] 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
this : ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ (i + 1) + y ^ 2 ^ (i + 1)

Tactic:
show (2 ^ (1 + 1) : ℤ) = 4 by simp,

Goal state after:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
this : ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
⊢ ¬4 ∣ x ^ 2 ^ (i + 1) + y ^ 2 ^ (i + 1)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ.hn
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
⊢ ¬2 ∣ k

Tactic:
contrapose hpn

Goal state after:
case succ.hn
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
hpn : 2 ∣ k
⊢ 2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case inl
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity ↑2 ↑(x ^ n - y ^ n) + 1 = emultiplicity ↑2 ↑(x + y) + emultiplicity ↑2 ↑(x - y) + emultiplicity 2 n

Tactic:
simp only [Int.ofNat_sub hyx, Int.ofNat_sub (pow_le_pow_left' hyx _), Int.natCast_add,
      Int.natCast_pow]

Goal state after:
case inl
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity (↑2) (↑x ^ n - ↑y ^ n) + 1 =
    emultiplicity (↑2) (↑x + ↑y) + emultiplicity (↑2) (↑x - ↑y) + emultiplicity 2 n
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case inl
x y : ℕ
hxy : ↑2 ∣ ↑(x - y)
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity (↑2) (↑x ^ n - ↑y ^ n) + 1 =
    emultiplicity (↑2) (↑x + ↑y) + emultiplicity (↑2) (↑x - ↑y) + emultiplicity 2 n

Tactic:
Int.ofNat_sub hyx

Goal state after:
case inl
x y : ℕ
hxy : ↑2 ∣ ↑x - ↑y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity (↑2) (↑x ^ n - ↑y ^ n) + 1 =
    emultiplicity (↑2) (↑x + ↑y) + emultiplicity (↑2) (↑x - ↑y) + emultiplicity 2 n
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
i : Fin (rank K)
⊢ (basisOfIsMaxRank hu) i = (logEmbedding K) (Additive.ofMul (u i))

Tactic:
by
  simp [basisOfIsMaxRank, Basis.coe_reindex, Equiv.symm_symm, Function.comp_apply,
    coe_basisOfPiSpaceOfLinearIndependent]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ Continuous (measurableEquivRealMixedSpacePolarSpace K).invFun

Tactic:
change Continuous fun x : polarSpace K ↦
      (⟨fun w ↦ x.1 w.val, fun w ↦ ⟨x.1 w.val, x.2 w⟩⟩ : realMixedSpace K)

Goal state after:
K : Type u_1
inst✝ : Field K
⊢ Continuous fun x ↦ (fun w ↦ x.1 ↑w, fun w ↦ (x.1 ↑w, x.2 w))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : polarSpace K
w : InfinitePlace K
hw : w.IsReal
⊢ normAtComplexPlaces (↑(polarSpaceCoord K).symm x) w = normAtComplexPlaces (mixedSpaceOfRealSpace x.1) w

Tactic:
simp [normAtComplexPlaces_apply_isReal ⟨w, hw⟩, mixedSpaceOfRealSpace_apply]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasurableSet (fundamentalCone K)

Tactic:
refine MeasurableSet.diff ?_ ?_
  · unfold logMap
    refine MeasurableSet.preimage (ZSpan.fundamentalDomain_measurableSet _) <|
      measurable_pi_iff.mpr fun w ↦ measurable_const.mul ?_
    exact (continuous_normAtPlace _).measurable.log.sub <|
      (mixedEmbedding.continuous_norm _).measurable.log.mul measurable_const
  · exact measurableSet_eq_fun (mixedEmbedding.continuous_norm K).measurable measurable_const

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ c • x ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
rw [Set.mem_preimage, logMap_real_smul hx.2 hc]

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ logMap x ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : mixedSpace K
ha : a ∈ integerSet K
⊢ ∃! x, (mixedEmbedding K) ↑x = a

Tactic:
by
  obtain ⟨_, ⟨x, rfl⟩⟩ := mem_integerSet.mp ha
  refine Function.Injective.existsUnique_of_mem_range ?_ (Set.mem_range_self x)
  exact (mixedEmbedding_injective K).comp RingOfIntegers.coe_injective

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
ζ : ↥(torsion K)
⊢ ↑((unitsMulComplexConjInv K) ↑ζ) = ↑(ζ ^ 2)

Tactic:
simp [unitsMulComplexConjInv_apply, unitsComplexConj_torsion, pow_two]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ x ∈ idealSet K J ↔ x ∈ fundamentalCone K ∧ ∃ a ∈ ↑↑J, (mixedEmbedding K) ↑a = x

Tactic:
idealSet,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ x ∈ fundamentalCone K ∩ ↑(idealLattice K ((FractionalIdeal.mk0 K) J)) ↔
    x ∈ fundamentalCone K ∧ ∃ a ∈ ↑↑J, (mixedEmbedding K) ↑a = x
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ exponent θ ↔ Codisjoint (comap (algebraMap ℤ (𝓞 K)) (conductor ℤ θ)) (span {↑p})

Tactic:
codisjoint_comm,

Goal state after:
K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ exponent θ ↔ Codisjoint (span {↑p}) (comap (algebraMap ℤ (𝓞 K)) (conductor ℤ θ))
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
h₀ : Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0
⊢ Polynomial.map (Int.castRingHom (ZMod p)) Q ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)

Tactic:
simp only [Multiset.mem_toFinset] at hQ

Goal state after:
K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
h₀ : Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0
hQ :
  Polynomial.map (Int.castRingHom (ZMod p)) Q ∈
    normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
⊢ Polynomial.map (Int.castRingHom (ZMod p)) Q ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : Algebra.IsIntegral ℚ K
inst✝¹ : IsTotallyComplex K
inst✝ : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card ↥(Subgroup.zpowers σ) = 2
this : Finite ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
w : InfinitePlace ↥L
⊢ w.IsReal

Tactic:
obtain ⟨W, rfl⟩ := w.comap_surjective (K := K)

Goal state after:
K : Type u_2
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : Algebra.IsIntegral ℚ K
inst✝¹ : IsTotallyComplex K
inst✝ : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card ↥(Subgroup.zpowers σ) = 2
this : Finite ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
W : InfinitePlace K
⊢ ((fun x ↦ x.comap (algebraMap (↥L) K)) W).IsReal
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
hP0 : P ≠ 0
Q : K[X]
HQ : Q ∈ normalizedFactors P
⊢ P.natDegree ≤ Q.natDegree

Tactic:
hPdeg,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
hP0 : P ≠ 0
Q : K[X]
HQ : Q ∈ normalizedFactors P
⊢ orderOf (unitOfCoprime (p ^ f) ⋯) ≤ Q.natDegree
Module: Mathlib.NumberTheory.NumberField.Ideal.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
I : Ideal (𝓞 K)
inst✝¹ : NumberField K
n : ℕ
inst✝ : NeZero n
ζ : 𝓞 K
hζ : IsPrimitiveRoot ζ n
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime n
⊢ IsPrimitiveRoot ((Ideal.Quotient.mk I) ζ) n

Tactic:
by
  have h : IsPrimitiveRoot hζ.toRootsOfUnity n :=
    IsPrimitiveRoot.coe_submonoidClass_iff.mp <| IsPrimitiveRoot.coe_units_iff.mp hζ
  exact IsPrimitiveRoot.coe_units_iff.mpr <|
    h.map_of_injective <| Ideal.rootsOfUnityMapQuot_injective n hI₁ hI₂

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : ¬IsMaxRank u
⊢ regOfFamily u / regOfFamily v =
    ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K))

Tactic:
· rw [regOfFamily_eq_zero hu, zero_div, eq_comm, Nat.cast_eq_zero]
    have : (Subgroup.closure (Set.range v) ⊔ torsion K).index ≠ 0 := by
      rw [← Subgroup.finiteIndex_iff, ← finiteIndex_iff_sup_torsion_finiteIndex]
      exact isMaxRank_iff_closure_finiteIndex.mp hv
    rwa [← mul_eq_zero_iff_right this, Subgroup.relIndex_mul_index h,
      ← Subgroup.not_finiteIndex_iff, ← finiteIndex_iff_sup_torsion_finiteIndex,
      ← isMaxRank_iff_closure_finiteIndex.not]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝² : NeZero n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
x : K
hx : x ^ n = 1
⊢ σ x = x ^ (↑((galEquivZMod n K) σ)).val

Tactic:
obtain ⟨a, -, rfl⟩ := (zeta_spec n ℚ K).eq_pow_of_pow_eq_one hx

Goal state after:
n : ℕ
inst✝² : NeZero n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
a : ℕ
hx : (zeta n ℚ K ^ a) ^ n = 1
⊢ σ (zeta n ℚ K ^ a) = (zeta n ℚ K ^ a) ^ (↑((galEquivZMod n K) σ)).val
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝² : NeZero n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
x : K
hx : x ^ n = 1
⊢ σ x = x ^ (↑((galEquivZMod n K) σ)).val

Tactic:
by
  obtain ⟨a, -, rfl⟩ := (zeta_spec n ℚ K).eq_pow_of_pow_eq_one hx
  rw [map_pow, pow_right_comm, galEquivZMod, autEquivPow_apply, OneHom.toFun_eq_coe,
    MonoidHom.toOneHom_coe, IsPrimitiveRoot.autToPow_spec]

Goal state after: