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

Goal state before:
pp: q i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2

Tactic:
← mul_pow ωb ω,

Goal state after:
q i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb * ω) ^ 2 ^ i - 2 = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m : Matrix (Fin 2) (Fin 2) R
v : Fin 2 → R
⊢ m *ᵥ v = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1]

Tactic:
by
  ext i
  fin_cases i <;>
  simp [mulVec_eq_sum]

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

Goal state before:
pp: case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
x✝ : 𝒢.HasDetOne
g : GL n R
hg : g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1

pp: case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
x✝ : 𝒢.HasDetOne
g : GL n R
hg : -g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1

Tactic:
· exact HasDetOne.det_eq hg

Goal state after:
case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
x✝ : 𝒢.HasDetOne
g : GL n R
hg : -g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : FunLike F ℍ ℂ
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ (-⇑f) ∣[k] γ = -⇑f

Tactic:
SlashAction.neg_slash,

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : FunLike F ℍ ℂ
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ -⇑f ∣[k] γ = -⇑f
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : (x 0).gcd (x 1) = 1
⊢ ((↑r * x) 0).gcd ((↑r * x) 1) = r

Tactic:
simp [Int.gcd_mul_left, hx]

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

Goal state before:
pp: r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : (x 0).gcd (x 1) = 1
⊢ ((↑r * x) 0).gcd ((↑r * x) 1) = r

Tactic:
by simp [Int.gcd_mul_left, hx]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
h : z ∈ 𝒟ᵒ
this : 1 < z.re * z.re + z.im * z.im
⊢ 3 < 4 * z.im ^ 2

Tactic:
have := h.2

Goal state after:
z : ℍ
h : z ∈ 𝒟ᵒ
this✝ : 1 < z.re * z.re + z.im * z.im
this : |z.re| < 1 / 2
⊢ 3 < 4 * z.im ^ 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‖
t : NNReal
h : τ.im = ↑t
ht : 0 < t
⊢ max (t ^ k) ((1 / t) ^ k) / ‖↑(t ^ k)‖₊ = max 1 (1 / t ^ k) ^ 2

Tactic:
(pow_left_mono 2).map_max,

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‖
t : NNReal
h : τ.im = ↑t
ht : 0 < t
⊢ max (t ^ k) ((1 / t) ^ k) / ‖↑(t ^ k)‖₊ = max (1 ^ 2) ((1 / t ^ k) ^ 2)
Module: Mathlib.Order.Filter.AtTopBot.Interval

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Tendsto (fun p ↦ Icc p.1 p.2) (atBot ×ˢ atTop) atTop

Tactic:
by
  simpa [tendsto_atTop, ← coe_subset, Set.subset_def, -eventually_and]
    using fun b i _ ↦ (eventually_le_atBot i).prod_mk (eventually_ge_atTop i)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hnorm
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
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
⊢ ‖↑z‖ = ‖↑(1 +ᵥ ρ)‖

Tactic:
rw [norm_def, h, coe_vadd, ofReal_one,
        show 1 + (ρ : ℂ) = -ρ ^ 2 by grind [ρ_sq], norm_neg, norm_pow, norm_ρ, Real.sqrt_one,
        one_pow]

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

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * deriv ((F - G) ∘ ↑ofComplex) ↑z =
    (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z - (2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z

Tactic:
show (F - G) ∘ ofComplex = F ∘ ofComplex - G ∘ ofComplex from rfl,

Goal state after:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex - G ∘ ↑ofComplex) ↑z =
    (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z - (2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl.inl
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 0
h : (g = T ∨ g = -T) ∧ z.re = -1 / 2
⊢ (g • z).im = z.im

Tactic:
rcases h with ⟨(rfl | rfl), -⟩

Goal state after:
case inl.inl.inl
g✝ : SL(2, ℤ)
z✝¹ : ℍ
g : SL(2, ℤ)
z✝ z : ℍ
hz : z ∈ 𝒟
hg : T • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) T)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑T 1 0
hc : ↑T 1 0 = 0
⊢ (T • z).im = z.im

case inl.inl.inr
g✝ : SL(2, ℤ)
z✝¹ : ℍ
g : SL(2, ℤ)
z✝ z : ℍ
hz : z ∈ 𝒟
hg : -T • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (-T))) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑(-T) 1 0
hc : ↑(-T) 1 0 = 0
⊢ (-T • z).im = z.im
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl.inr.inl
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 0
h : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2
⊢ (g • z).im = z.im

Tactic:
rcases h with ⟨(rfl | rfl), -⟩

Goal state after:
case inl.inr.inl.inl
g✝ : SL(2, ℤ)
z✝¹ : ℍ
g : SL(2, ℤ)
z✝ z : ℍ
hz : z ∈ 𝒟
hg : T⁻¹ • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) T⁻¹)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑T⁻¹ 1 0
hc : ↑T⁻¹ 1 0 = 0
⊢ (T⁻¹ • z).im = z.im

case inl.inr.inl.inr
g✝ : SL(2, ℤ)
z✝¹ : ℍ
g : SL(2, ℤ)
z✝ z : ℍ
hz : z ∈ 𝒟
hg : -T⁻¹ • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (-T⁻¹))) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑(-T⁻¹) 1 0
hc : ↑(-T⁻¹) 1 0 = 0
⊢ (-T⁻¹ • z).im = z.im
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl.inr.inr.inl
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 0
h : g = 1
⊢ (g • z).im = z.im

Tactic:
rcases h with ⟨(rfl | rfl), -⟩

Goal state after:
case inl.inr.inr.inl
g✝ : SL(2, ℤ)
z✝¹ : ℍ
g : SL(2, ℤ)
z✝ z : ℍ
hz : z ∈ 𝒟
hg : 1 • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) 1)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑1 1 0
hc : ↑1 1 0 = 0
⊢ (1 • z).im = z.im
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl.inr.inr.inr
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 0
h : g = -1
⊢ (g • z).im = z.im

Tactic:
rcases h with ⟨(rfl | rfl), -⟩

Goal state after:
case inl.inr.inr.inr
g✝ : SL(2, ℤ)
z✝¹ : ℍ
g : SL(2, ℤ)
z✝ z : ℍ
hz : z ∈ 𝒟
hg : -1 • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (-1))) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑(-1) 1 0
hc : ↑(-1) 1 0 = 0
⊢ (-1 • z).im = z.im
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
⊢ (↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ))).det = 1

Tactic:
← Matrix.GeneralLinearGroup.val_det_apply

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
⊢ ↑(Matrix.GeneralLinearGroup.det
        (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ))) =
    1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inl.inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(T * S) 1 0
hc : ↑(T * S) 1 0 = 1
hd : ↑(T * S) 1 1 = 0
hz : 1 +ᵥ ρ ∈ 𝒟
hg : (T * S) • (1 +ᵥ ρ) ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T * S))) ↑(1 +ᵥ ρ)‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T * S))) ↑(1 +ᵥ ρ)) = 1

Tactic:
show T * S = ⟨!![1, -1; 1, 0], by simp⟩ by decide

Goal state after:
case inr.inl.inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(T * S) 1 0
hc : ↑(T * S) 1 0 = 1
hd : ↑(T * S) 1 1 = 0
hz : 1 +ᵥ ρ ∈ 𝒟
hg : (T * S) • (1 +ᵥ ρ) ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T * S))) ↑(1 +ᵥ ρ)‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) ⟨!![1, -1; 1, 0], ⋯⟩)) ↑(1 +ᵥ ρ)) = 1
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: p p4 p6 : PowerSeries ℂ
c4 c6 : ℂ
hp4_0 : PowerSeries.constantCoeff p4 = 1
hp6_0 : PowerSeries.constantCoeff p6 = 1
hp4_1 : (PowerSeries.coeff 1) p4 = 240
hp6_1 : (PowerSeries.coeff 1) p6 = -504
hqc4 : c4 • p4 = p ^ 2
hqc6 : c6 • p6 = p ^ 3
⊢ p = 0

Tactic:
let D := (c4 • p4) ^ 3 - (c6 • p6) ^ 2

Goal state after:
p p4 p6 : PowerSeries ℂ
c4 c6 : ℂ
hp4_0 : PowerSeries.constantCoeff p4 = 1
hp6_0 : PowerSeries.constantCoeff p6 = 1
hp4_1 : (PowerSeries.coeff 1) p4 = 240
hp6_1 : (PowerSeries.coeff 1) p6 = -504
hqc4 : c4 • p4 = p ^ 2
hqc6 : c6 • p6 = p ^ 3
D : PowerSeries ℂ := (c4 • p4) ^ 3 - (c6 • p6) ^ 2
⊢ p = 0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: p p4 p6 : PowerSeries ℂ
c4 c6 : ℂ
hp4_0 : PowerSeries.constantCoeff p4 = 1
hp6_0 : PowerSeries.constantCoeff p6 = 1
hp4_1 : (PowerSeries.coeff 1) p4 = 240
hp6_1 : (PowerSeries.coeff 1) p6 = -504
hqc4 : c4 • p4 = p ^ 2
hqc6 : c6 • p6 = p ^ 3
D : PowerSeries ℂ := (c4 • p4) ^ 3 - (c6 • p6) ^ 2
hD0 : (PowerSeries.coeff 0) D = c4 ^ 3 - c6 ^ 2
⊢ p = 0

Tactic:
have hD1 : D.coeff 1 = 720 * c4 ^ 3 + 1008 * c6 ^ 2 := by
    simp [D, pow_succ, PowerSeries.coeff_mul, Finset.Nat.antidiagonal_succ]
    grind

Goal state after:
p p4 p6 : PowerSeries ℂ
c4 c6 : ℂ
hp4_0 : PowerSeries.constantCoeff p4 = 1
hp6_0 : PowerSeries.constantCoeff p6 = 1
hp4_1 : (PowerSeries.coeff 1) p4 = 240
hp6_1 : (PowerSeries.coeff 1) p6 = -504
hqc4 : c4 • p4 = p ^ 2
hqc6 : c6 • p6 = p ^ 3
D : PowerSeries ℂ := (c4 • p4) ^ 3 - (c6 • p6) ^ 2
hD0 : (PowerSeries.coeff 0) D = c4 ^ 3 - c6 ^ 2
hD1 : (PowerSeries.coeff 1) D = 720 * c4 ^ 3 + 1008 * c6 ^ 2
⊢ p = 0
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: y : ℝ
hy : 1 ≤ y
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) ≤ 2 / (1 - rexp (-(π * 1))) * ‖rexp (-π * τ.im)‖

Tactic:
rw [Real.norm_eq_abs, Real.abs_exp, hτ, neg_mul]

Goal state after:
y : ℝ
hy : 1 ≤ y
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-(π * y))) * rexp (-(π * y)) ≤ 2 / (1 - rexp (-(π * 1))) * rexp (-(π * y))
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
⊢ HasSum (fun i ↦ (PowerSeries.coeff i) (qExpansion (h Γ) ⇑f) / ↑i ^ s) (↑(h Γ) ^ (-s) * L hk f s)

Tactic:
convert! hΛ.mul_right (2 / Gammaℂ s * h Γ ^ (-s)) using 1

Goal state after:
case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
⊢ (fun i ↦ (PowerSeries.coeff i) (qExpansion (h Γ) ⇑f) / ↑i ^ s) = fun i ↦
    ↑π ^ (-s) * Gamma s * (PowerSeries.coeff i) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑i / h Γ) ^ s *
      (2 / s.Gammaℂ * ↑(h Γ) ^ (-s))

case e'_6
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
⊢ ↑(h Γ) ^ (-s) * L hk f s = Λ hk f s * (2 / s.Gammaℂ * ↑(h Γ) ^ (-s))
Module: Mathlib.NumberTheory.Multiplicity

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

pp: x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ n ≠ 0

pp: x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x - y ≠ 0

pp: x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x + y ≠ 0

pp: x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x ^ n - y ^ n ≠ 0

Tactic:
· exact Nat.two_pow_sub_pow hxy hx hneven

Goal state after:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ n ≠ 0

x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x - y ≠ 0

x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x + y ≠ 0

x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x ^ n - y ^ n ≠ 0
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
n : Type u_3
inst✝² : Finite n
X : Type u_4
inst✝¹ : TopologicalSpace X
A : n → ι → Type u_5
inst✝ : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst✝ j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst✝¹] (f ∘ Pi.map fun x ↦ inclusion (A x) (C x) hS)
x : (j : n) → Πʳ (i : ι), [A j i, C j i]
S : Set ι := {i | ∀ (j : n), (x j) i ∈ C j i}
hS : cofinite ≤ 𝓟 S
x' : (j : n) → Πʳ (i : ι), [A j i, C j i]_[𝓟 S] := fun j ↦ mk (fun i ↦ (x j) i) ⋯
⊢ Tendsto f (𝓝 x) (𝓝 (f x))

Tactic:
have hxx' : Pi.map (fun j ↦ inclusion _ _ hS) x' = x := rfl

Goal state after:
ι : Type u_1
n : Type u_3
inst✝² : Finite n
X : Type u_4
inst✝¹ : TopologicalSpace X
A : n → ι → Type u_5
inst✝ : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst✝ j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst✝¹] (f ∘ Pi.map fun x ↦ inclusion (A x) (C x) hS)
x : (j : n) → Πʳ (i : ι), [A j i, C j i]
S : Set ι := {i | ∀ (j : n), (x j) i ∈ C j i}
hS : cofinite ≤ 𝓟 S
x' : (j : n) → Πʳ (i : ι), [A j i, C j i]_[𝓟 S] := fun j ↦ mk (fun i ↦ (x j) i) ⋯
hxx' : Pi.map (fun j ↦ inclusion (A j) (C j) hS) x' = x
⊢ Tendsto f (𝓝 x) (𝓝 (f x))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

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

Tactic:
by
    change Continuous fun x : realMixedSpace K ↦ (fun w ↦ if hw : w.IsReal then x.1 ⟨w, hw⟩ else
      (x.2 ⟨w, not_isReal_iff_isComplex.mp hw⟩).1, fun w ↦ (x.2 w).2)
    refine .prodMk (continuous_pi fun w ↦ ?_) (by fun_prop)
    split_ifs <;> fun_prop

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
⊢ logMap (x * y) = logMap x + logMap y

Tactic:
by
  ext w
  simp_rw [Pi.add_apply, logMap_apply]
  rw [map_mul, map_mul, Real.log_mul, Real.log_mul hx hy, add_mul]
  · ring
  · exact mixedEmbedding.norm_ne_zero_iff.mp hx w
  · exact mixedEmbedding.norm_ne_zero_iff.mp hy w

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
φ ψ : K →+* ℂ
σ τ : Gal(K/↥K⁺)
hφ : ComplexEmbedding.IsConj φ σ
hψ : ComplexEmbedding.IsConj ψ τ
this : Nat.card Gal(K/↥K⁺) = 2
⊢ σ = τ

Tactic:
Nat.card_eq_two_iff' 1

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCMField K
φ ψ : K →+* ℂ
σ τ : Gal(K/↥K⁺)
hφ : ComplexEmbedding.IsConj φ σ
hψ : ComplexEmbedding.IsConj ψ τ
this : ∃! y, y ≠ 1
⊢ σ = τ
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
⊢ 2 = Module.finrank (↥K⁺) K

Tactic:
IsQuadraticExtension.finrank_eq_two

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
⊢ 2 = 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a b : ↑(integerSet K)
x✝ : a ≈ b
u : ↥(torsion K)
hu : (fun m ↦ m • b) u = a
⊢ intNorm a = intNorm b

Tactic:
← Nat.cast_inj (R := ℝ),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a b : ↑(integerSet K)
x✝ : a ≈ b
u : ↥(torsion K)
hu : (fun m ↦ m • b) u = a
⊢ ↑(intNorm a) = ↑(intNorm b)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a b : ↑(integerSet K)
x✝ : a ≈ b
u : ↥(torsion K)
hu : (fun m ↦ m • b) u = a
⊢ mixedEmbedding.norm ↑a = mixedEmbedding.norm ↑b

Tactic:
← hu,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a b : ↑(integerSet K)
x✝ : a ≈ b
u : ↥(torsion K)
hu : (fun m ↦ m • b) u = a
⊢ mixedEmbedding.norm ↑((fun m ↦ m • b) u) = mixedEmbedding.norm ↑b
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
n : ℕ
x✝ : ↑(integerSet K)
⊢ mixedEmbedding.norm ↑x✝ = ↑n ↔ absNorm ↑↑((integerSetEquiv K) x✝).1 = n

Tactic:
by simp_rw [← intNorm_coe, intNorm,
        Nat.cast_inj, integerSetEquiv_apply_fst, absNorm_span_singleton]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h₁ : LinearIndependent ℝ fun w ↦ completeFamily K ↑w
h : completeFamily K w₀ ∈ Submodule.span ℝ (Set.range fun w ↦ completeFamily K ↑w)
this : finrank ℚ K = 0
⊢ False

Tactic:
exact Module.finrank_pos.ne' this

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ regulator K = |(Matrix.of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e i))))).det|

Tactic:
rw [regulator_eq_regOfFamily_fundSystem, regOfFamily_eq_det]

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

Goal state before:
pp: 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
⊢ span ℤ (Set.range ⇑(basisOfIsMaxRank hu)) ≤ span ℤ (Set.range ⇑(basisOfIsMaxRank hv))

Tactic:
← toAddSubgroup_le,

Goal state after:
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
⊢ (span ℤ (Set.range ⇑(basisOfIsMaxRank hu))).toAddSubgroup ≤ (span ℤ (Set.range ⇑(basisOfIsMaxRank hv))).toAddSubgroup
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this✝ : IsGalois ℚ K
h_main : (𝒑.primesOver (𝓞 K)).ncard * (𝒑.ramificationIdxIn (𝓞 K) * 𝒑.inertiaDegIn (𝓞 K)) = Nat.card Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta (p ^ (k + 1)) ℚ K) (p ^ (k + 1))
this : (span {hζ.toInteger - 1}).LiesOver 𝒑
⊢ (𝒑.primesOver (𝓞 K)).ncard = 1

Tactic:
ramificationIdxIn_eq_ramificationIdx 𝒑 (span {hζ.toInteger - 1}) Gal(K/ℚ),

Goal state after:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this✝ : IsGalois ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ (k + 1)) ℚ K) (p ^ (k + 1))
h_main :
  (𝒑.primesOver (𝓞 K)).ncard * ((span {hζ.toInteger - 1}).ramificationIdx ℤ * 𝒑.inertiaDegIn (𝓞 K)) = Nat.card Gal(K/ℚ)
this : (span {hζ.toInteger - 1}).LiesOver 𝒑
⊢ (𝒑.primesOver (𝓞 K)).ncard = 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (p ^ 1)
⊢ (span {hζ✝.toInteger - 1}).ramificationIdx ℤ = p - 1

Tactic:
rw [ramificationIdx_span_zeta_sub_one p 0 hζ, pow_zero, one_mul]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' normLeOne K, ∏ w, ENNReal.ofReal (x ↑w) =
    2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)

Tactic:
normLeOne_eq_preimage,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K,
        ∏ w, ENNReal.ofReal (x ↑w) =
    2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
Module: Mathlib.NumberTheory.NumberField.DirichletDensity

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
hS : S.Finite
s : ℝ
hs : 0 ≤ s
⊢ primeIdealZetaSum S s ≤ ↑S.ncard

Tactic:
replace hS := hS.to_subtype
  grw [primeIdealZetaSum_def, Real.rpow_le_one_of_one_le_of_nonpos] <;>
  simp [Summable.of_finite, Nat.one_le_iff_ne_zero,
    Ideal.absNorm_eq_zero_iff, hs, HeightOneSpectrum.ne_bot]

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
R : Type u_2
inst✝² : CommRing R
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
⊢ Nat.card ↥((intermediateFieldEquivSubgroupChar n K R) F) = Module.finrank ℚ ↥F

Tactic:
unfold intermediateFieldEquivSubgroupChar

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst✝² : CommRing R
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
⊢ Nat.card
      ↥((IsGalois.intermediateFieldEquivSubgroup.trans
            ((subgroupGalEquivSubgroupChar n K R).dual.trans
              (OrderIso.dualDual (Subgroup (DirichletCharacter R n))).symm))
          F) =
    Module.finrank ℚ ↥F