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

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

Tactic:
ext z

Goal state after:
c : ℂ
F : ℍ → ℂ
hF : MDiff F
z : ℍ
⊢ D (c • F) z = (c • D F) z
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
⊢ D (F * G) = D F * G + F * D G

Tactic:
ext z

Goal state after:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ D (F * G) z = (D F * G + F * D G) z
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F : ℍ → ℂ
n : ℕ
hF : MDiff F
⊢ D (F ^ n) = ↑n * F ^ (n - 1) * D F

Tactic:
ext z

Goal state after:
F : ℍ → ℂ
n : ℕ
hF : MDiff F
z : ℍ
⊢ D (F ^ n) z = (↑n * F ^ (n - 1) * D F) z
Module: Mathlib.NumberTheory.ModularForms.Derivative

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

Tactic:
ext z

Goal state after:
k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ serreDerivative k (F + G) z = (serreDerivative k F + serreDerivative k G) z
Module: Mathlib.NumberTheory.ModularForms.Derivative

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

Tactic:
ext z

Goal state after:
k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ serreDerivative k (F - G) z = (serreDerivative k F - serreDerivative k G) z
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k c : ℂ
F : ℍ → ℂ
hF : MDiff F
⊢ serreDerivative k (c • F) = c • serreDerivative k F

Tactic:
ext z

Goal state after:
k c : ℂ
F : ℍ → ℂ
hF : MDiff F
z : ℍ
⊢ serreDerivative k (c • F) z = (c • serreDerivative k F) z
Module: Mathlib.NumberTheory.ModularForms.Derivative

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

Tactic:
ext z

Goal state after:
k₁ k₂ : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ serreDerivative (k₁ + k₂) (F * G) z = (serreDerivative k₁ F * G + F * serreDerivative k₂ G) z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (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 • ρ
this : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
⊢ 1 + -2⁻¹ = 2⁻¹

Tactic:
norm_num

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

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
⊢ D (F ∣[k] g) = fun z ↦
    (↑(↑g).det)⁻¹ * (D F ∣[k + 2] g) z - ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F ∣[k] g) z

Tactic:
ext z

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
⊢ D (F ∣[k] g) z = (↑(↑g).det)⁻¹ * (D F ∣[k + 2] g) z - ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F ∣[k] g) z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (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 • ρ
this : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
⊢ -2⁻¹ - 2⁻¹ = -1

Tactic:
norm_num

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

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
hdet : (↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ))).det = 1
⊢ D (F ∣[k] γ) =
    D F ∣[k + 2] γ - fun z ↦
      ↑k * (2 * ↑π * I)⁻¹ *
          (↑(↑γ 1 0) /
            denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
        (F ∣[k] γ) z

Tactic:
ext z

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
hdet : (↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ))).det = 1
z : ℍ
⊢ D (F ∣[k] γ) z =
    (D F ∣[k + 2] γ - fun z ↦
        ↑k * (2 * ↑π * I)⁻¹ *
            (↑(↑γ 1 0) /
              denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
          (F ∣[k] γ) z)
      z
Module: Mathlib.NumberTheory.ModularForms.Derivative

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

Tactic:
ext z

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
z : ℍ
⊢ (serreDerivative (↑k) F ∣[k + 2] γ) z = serreDerivative (↑k) (F ∣[k] γ) z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ 1 / ↑z / 2 + ↑π * I / 12 * E2 z = (↑z ^ (1 / 2 + 2⁻¹))⁻¹ / 2 + ↑π * I / 12 * E2 z

Tactic:
norm_num

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

Goal state before:
pp: ⊢ Δ ∣[12] ModularGroup.T = Δ

Tactic:
ext z

Goal state after:
z : ℍ
⊢ (Δ ∣[12] ModularGroup.T) z = Δ z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
x : ℂ
hx : x ∈ S
⊢ (fun s ↦ cexp (2 * ↑π * I * ↑m * s / ↑p)) = fun s ↦ cexp (2 * ↑π * I * ↑m / ↑p * s)

Tactic:
ext z

Goal state after:
k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
x : ℂ
hx : x ∈ S
z : ℂ
⊢ cexp (2 * ↑π * I * ↑m * z / ↑p) = cexp (2 * ↑π * I * ↑m / ↑p * z)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : f =O[atTop] fun n ↦ ↑n ^ l
⊢ (fun n ↦ (2 * ↑π * I * ↑n / ↑p) ^ k) = fun n ↦ (2 * ↑π * I / ↑p) ^ k * ↑n ^ k

Tactic:
ext z

Goal state after:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : f =O[atTop] fun n ↦ ↑n ^ l
z : ℕ
⊢ (2 * ↑π * I * ↑z / ↑p) ^ k = (2 * ↑π * I / ↑p) ^ k * ↑z ^ k
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: ⊢ Δ ∣[12] ModularGroup.S = Δ

Tactic:
ext z

Goal state after:
z : ℍ
⊢ (Δ ∣[12] ModularGroup.S) z = Δ z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: this :
  (Summable fun n ↦ (1 / 2) ^ (n + 1)) →
    (∀ (k : ℕ), Tendsto (fun x ↦ -x ^ (k + 1)) (𝓝 0) (𝓝 0)) →
      (∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖n‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)) →
        Tendsto (fun n ↦ ∏' (k : ℕ), (1 + -n ^ (k + 1))) (𝓝 0) (𝓝 1)
⊢ |1 / 2| < 1

Tactic:
norm_num

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

Goal state before:
pp: this :
  (Summable fun n ↦ (1 / 2) ^ (n + 1)) →
    (∀ (k : ℕ), Tendsto (fun x ↦ -x ^ (k + 1)) (𝓝 0) (𝓝 0)) →
      (∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖n‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)) →
        Tendsto (fun n ↦ ∏' (k : ℕ), (1 + -n ^ (k + 1))) (𝓝 0) (𝓝 1)
⊢ 0 < 1 / 2

Tactic:
norm_num

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

Goal state before:
pp: ⊢ 0 < 1 / 2

Tactic:
norm_num

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

Goal state before:
pp: k : ℕ
h0 : (fun n ↦ 1) =O[atTop] fun n ↦ ↑n ^ 1
⊢ 0 < 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
a b : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext z

Goal state after:
k : ℤ
a b : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
z : ℍ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
c : ℂ
a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext z

Goal state after:
k : ℤ
c : ℂ
a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
z : ℍ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext z

Goal state after:
k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
z : ℍ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext z

Goal state after:
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12)
z : ℍ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: ⊢ 3 ≤ 2 + 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: ⊢ ↑(2 + 2) < 12

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: ⊢ 3 ≤ 3 + 3

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: ⊢ ↑(3 + 3) < 12

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
a b : ℤ
this : Summable fun i ↦ (↑b - ↑a) * ((↑i * ↑z + ↑a) * (↑i * ↑z + ↑b))⁻¹
⊢ Summable fun m ↦ 1 / (↑m * ↑z + ↑a) - 1 / (↑m * ↑z + ↑b)

Tactic:
rw [← Finset.summable_compl_iff (s := {0})] at *

Goal state after:
z : ℍ
a b : ℤ
this : Summable fun x ↦ (↑b - ↑a) * ((↑↑x * ↑z + ↑a) * (↑↑x * ↑z + ↑b))⁻¹
⊢ Summable fun x ↦ 1 / (↑↑x * ↑z + ↑a) - 1 / (↑↑x * ↑z + ↑b)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
e : ℕ+
z : ℍ
he : 0 < (↑↑e * ↑z).im
⊢ 0 < 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mpr
g : SL(2, ℤ)
⊢ ↑{ coe := (-↑I)⁻¹, coe_im_pos := ⋯ } = ↑I

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
⊢ ¬↑1 + ↑ρ = ↑ρ

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this : HasSum (fun n ↦ cexp (↑π * I * ↑(n + 1) ^ 2 * τ) * 2) (jacobiTheta τ + (1 - 1 * 2))
⊢ 1 - 1 * 2 = -1

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
ext z

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

Goal state before:
pp: y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 0 = z.im
⊢ 1 / 2 < 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing

Goal state before:
pp: ⊢ (PowerSeries.coeff 1) (qExpansion 1 ⇑E₄CubeSubE₆SqForm) = 1728

Tactic:
by
  rw [E₄CubeSubE₆SqForm_qExpansion_eq]
  norm_num [PowerSeries.coeff_mul, Finset.Nat.antidiagonal_succ, E₄_qExpansion_coeff_one,
    E₆_qExpansion_coeff_one, E_qExpansion_coeff_zero _ ⟨2, rfl⟩,
    E_qExpansion_coeff_zero _ ⟨3, rfl⟩]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing

Goal state before:
pp: case e_6
⊢ modularForm CuspForm.discriminant = (1 / 1728) • (E₄.pow 3 - E₆.pow 2)

Tactic:
ext z

Goal state after:
case e_6
z : ℍ
⊢ (modularForm CuspForm.discriminant) z = ((1 / 1728) • (E₄.pow 3 - E₆.pow 2)) z
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
x✝ : ℍ
⊢ 0 x✝ = 0 x✝

Tactic:
Pi.zero_apply,

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
x✝ : ℍ
⊢ 0 = 0 x✝
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n

Tactic:
obtain hyx | hyx := le_total y x

Goal state after:
case inl
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n

case inr
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : x ≤ y
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
⊢ emultiplicity 2 (x ^ 2 ^ n - y ^ 2 ^ n) = emultiplicity 2 (x - y) + ↑n

Tactic:
by
  simp only [pow_two_pow_sub_pow_two_pow n, emultiplicity_mul Int.prime_two,
    Finset.emultiplicity_prod Int.prime_two, add_comm, Nat.cast_one, Finset.sum_const,
    Finset.card_range, nsmul_one, Int.two_pow_two_pow_add_two_pow_two_pow hx hxy]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

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

Tactic:
obtain hyx | hyx := le_total y x

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

case inr
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : x ≤ y
⊢ 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: x n : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ padicValNat 2 (x ^ n - 1) + 1 = padicValNat 2 (x + 1) + padicValNat 2 (x - 1) + padicValNat 2 n

Tactic:
by
  simpa using pow_two_sub_pow h1x (by grind) hx hn hneven

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
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ 1 ≠ 0

Tactic:
norm_num

Goal state after:
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

pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : polarSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ normAtComplexPlaces (↑(polarSpaceCoord K).symm x) w = normAtComplexPlaces (mixedSpaceOfRealSpace x.1) w

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

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : polarSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ normAtComplexPlaces (↑(polarSpaceCoord K).symm x) w = normAtComplexPlaces (mixedSpaceOfRealSpace x.1) w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx' : x ∈ ⇑(mixedEmbedding K) '' Set.range ⇑(algebraMap (𝓞 K) K)
hx : mixedEmbedding.norm x ≠ 0
u : (𝓞 K)ˣ
hu : u • x ∈ fundamentalCone K
⊢ ∃ u, u • x ∈ integerSet K

Tactic:
obtain ⟨_, ⟨x, rfl⟩, _, rfl⟩ := hx'

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : 𝓞 K
hx : mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) x)) ≠ 0
hu : u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x) ∈ fundamentalCone K
⊢ ∃ u, u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x) ∈ integerSet K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_1.refine_3
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ : normAtAllPlaces a ∈ ⋂ w, {x | x ↑w ≠ 0}
⊢ normAtComplexPlaces (mixedSpaceOfRealSpace (normAtAllPlaces a)) = normAtAllPlaces a

Tactic:
normAtComplexPlaces_normAtAllPlaces

Goal state after:
case refine_1.refine_3
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ : normAtAllPlaces a ∈ ⋂ w, {x | x ↑w ≠ 0}
⊢ normAtAllPlaces a = normAtAllPlaces a
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case e'_3.e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w₁ w₂ : InfinitePlace K
e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)
e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)
g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm
h_col :
  |((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
          id).det| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
h :
  |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (Fin.succAbove 0)).det| =
    |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id
          (f.symm w₂).succAbove).det|
⊢ (reindex g g)
      ((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm)) id) =
    (of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (f.symm w₂).succAbove

Tactic:
ext; simp only [ne_eq, Equiv.coe_trans, reindex_apply, submatrix_apply, Function.comp_apply,
          Equiv.apply_symm_apply, id_eq, of_apply]; rfl

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
⊢ ∑ w ∈ (placesOver L v).toFinset, v.inertiaDeg w = Module.finrank K L

Tactic:
← union_ramifiedPlacesOver_unramifiedPlacesOver L v,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
⊢ ∑ w ∈ (ramifiedPlacesOver L v ∪ unramifiedPlacesOver L v).toFinset, v.inertiaDeg w = Module.finrank K L
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case pos
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
this : span ℤ (Set.range ⇑(basisOfIsMaxRank hu)) ≤ span ℤ (Set.range ⇑(basisOfIsMaxRank hv))
⊢ ↑((Subgroup.toAddSubgroup (Subgroup.closure (Set.range u)) ⊔ (logEmbedding K).ker).relIndex
        (Subgroup.toAddSubgroup (Subgroup.closure (Set.range v)) ⊔ (logEmbedding K).ker)) =
    ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K))

Tactic:
logEmbedding_ker,

Goal state after:
case pos
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
this : span ℤ (Set.range ⇑(basisOfIsMaxRank hu)) ≤ span ℤ (Set.range ⇑(basisOfIsMaxRank hv))
⊢ ↑((Subgroup.toAddSubgroup (Subgroup.closure (Set.range u)) ⊔ Subgroup.toAddSubgroup (torsion K)).relIndex
        (Subgroup.toAddSubgroup (Subgroup.closure (Set.range v)) ⊔ Subgroup.toAddSubgroup (torsion K))) =
    ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K))
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case pos
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
this : span ℤ (Set.range ⇑(basisOfIsMaxRank hu)) ≤ span ℤ (Set.range ⇑(basisOfIsMaxRank hv))
⊢ regOfFamily u / regOfFamily v =
    ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K))

Tactic:
rw [regOfFamily_of_isMaxRank hu, regOfFamily_of_isMaxRank hv,
      covolume_div_covolume_eq_relIndex _ _ this, span_basisOfIsMaxRank hu,
      span_basisOfIsMaxRank hv, AddSubgroup.relIndex_map_map, logEmbedding_ker,
      ← OrderIso.map_sup, ← OrderIso.map_sup, ← Subgroup.relIndex_toAddSubgroup]

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

Goal state before:
pp: case hsep
m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
ζ : 𝓞 K := ⋯
h₁ : ¬p ∣ exponent ζ
h₂ :
  Irreducible ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∧
    (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).Monic ∧
      ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)
h₃ :
  P.ramificationIdx ℤ =
    multiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
⊢ (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)).Separable

Tactic:
· exact (zeta_spec m ℚ K).toInteger_isPrimitiveRoot.separable_minpoly_mod hm

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
c : ℕ
⊢ (univ.sup fun φ ↦ ‖φ (↑c * α)‖₊) = ↑c * univ.sup fun φ ↦ ‖φ α‖₊

Tactic:
simp [NNReal.mul_finset_sup]

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

Goal state before:
pp: case calc_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ ‖σ' α * ∏ τ ∈ univ.erase σ', τ α‖ ≤ ‖σ' α‖ * ∏ τ ∈ univ.erase σ', ‖τ α‖

Tactic:
Complex.norm_mul

Goal state after:
case calc_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ ‖σ' α‖ * ‖∏ τ ∈ univ.erase σ', τ α‖ ≤ ‖σ' α‖ * ∏ τ ∈ univ.erase σ', ‖τ α‖