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

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
⊢ HasFDerivAt (fun p ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

Tactic:
have hVmem : (z, τ) ∈ V := ⟨hz, hτ'⟩

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
⊢ HasFDerivAt (fun p ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
⊢ ∑' (n : ℤ), f_int k a t n = ∑' (n : ℕ), f_nat k a t n + ∑' (n : ℕ), f_nat k (1 - a) t n

Tactic:
convert!
    ((summable_f_nat k a ht).hasSum.int_rec (summable_f_nat k (1 - a) ht).hasSum).tsum_eq using
    3 with n

Goal state after:
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
n : ℤ
⊢ f_int k a t n = Int.rec (f_nat k a t) (f_nat k (1 - a) t) n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: z τ : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ) *
      (cexp (-↑π * I * (τ + 2 * (z * τ))) * (jacobiTheta₂' (z * τ) τ - 2 * ↑π * I * jacobiTheta₂ (z * τ) τ) /
          (2 * ↑π * I) +
        (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * jacobiTheta₂ (z * τ) τ) +
          cexp (-↑π * I * (τ + 2 * (z * τ))) * jacobiTheta₂ (z * τ) τ)) =
    cexp (↑π * I * z ^ 2 * τ) * (jacobiTheta₂' (z * τ) τ / (2 * ↑π * I) + z * jacobiTheta₂ (z * τ) τ)

Tactic:
generalize jacobiTheta₂ (z * τ) τ = J

Goal state after:
z τ J : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ) *
      (cexp (-↑π * I * (τ + 2 * (z * τ))) * (jacobiTheta₂' (z * τ) τ - 2 * ↑π * I * J) / (2 * ↑π * I) +
        (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * J) + cexp (-↑π * I * (τ + 2 * (z * τ))) * J)) =
    cexp (↑π * I * z ^ 2 * τ) * (jacobiTheta₂' (z * τ) τ / (2 * ↑π * I) + z * J)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: z τ : ℂ
⊢ jacobiTheta₂'' (z + 1) τ = jacobiTheta₂'' z τ

Tactic:
by
  simp only [jacobiTheta₂'', add_mul z 1, one_mul, jacobiTheta₂'_add_left', jacobiTheta₂_add_left']
  generalize jacobiTheta₂ (z * τ) τ = J
  generalize jacobiTheta₂' (z * τ) τ = J'
  -- clear denominator
  simp_rw [div_add' _ _ _ two_pi_I_ne_zero, ← mul_div_assoc]
  refine congr_arg (· / (2 * π * I)) ?_
  -- get all exponential terms to left
  rw [mul_left_comm _ (cexp _), ← mul_add, mul_assoc (cexp _), ← mul_add, ← mul_assoc (cexp _),
    ← Complex.exp_add]
  congrm (cexp ?_ * ?_) <;> ring

Goal state after:
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
⊢ completedHurwitzZetaEven₀ 0 (1 - s) = completedCosZeta₀ 0 s

Tactic:
completedHurwitzZetaEven₀_one_sub

Goal state after:
s : ℂ
⊢ completedCosZeta₀ 0 s = completedCosZeta₀ 0 s
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
⊢ completedHurwitzZetaEven 0 (1 - s) = completedRiemannZeta s

Tactic:
← completedCosZeta_zero,

Goal state after:
s : ℂ
⊢ completedHurwitzZetaEven 0 (1 - s) = completedCosZeta 0 s
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: k : ℕ
m : ℕ := 2 ^ k.primesBelow.card
N₀ : ℕ := 2 * m ^ 2
hN₀ : N₀ = 2 * m ^ 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p
this : 2 * ↑(2 * m ^ 2) - ↑m * ↑(2 * m) ≤ 2 * ↑(2 * m ^ 2) * S
⊢ 1 / 2 ≤ S

Tactic:
cast_mul,

Goal state after:
k : ℕ
m : ℕ := 2 ^ k.primesBelow.card
N₀ : ℕ := 2 * m ^ 2
hN₀ : N₀ = 2 * m ^ 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p
this : 2 * (↑2 * ↑(m ^ 2)) - ↑m * ↑(2 * m) ≤ 2 * (↑2 * ↑(m ^ 2)) * S
⊢ 1 / 2 ≤ S
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: k : ℕ
m : ℕ := 2 ^ k.primesBelow.card
N₀ : ℕ := 2 * m ^ 2
hN₀ : N₀ = 2 * m ^ 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p
this : 2 * (↑2 * ↑(m ^ 2)) - ↑m * ↑(2 * m) ≤ 2 * (↑2 * ↑(m ^ 2)) * S
⊢ 1 / 2 ≤ S

Tactic:
cast_mul,

Goal state after:
k : ℕ
m : ℕ := 2 ^ k.primesBelow.card
N₀ : ℕ := 2 * m ^ 2
hN₀ : N₀ = 2 * m ^ 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p
this : 2 * (↑2 * ↑(m ^ 2)) - ↑m * (↑2 * ↑m) ≤ 2 * (↑2 * ↑(m ^ 2)) * S
⊢ 1 / 2 ≤ S
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
χ : DirichletCharacter R n✝
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ χ ↑p.1 * f p.1 * (χ ↑p.2 * g p.2) = χ ↑(p.1 * p.2) * (f p.1 * g p.2)

Tactic:
cast_mul,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
χ : DirichletCharacter R n✝
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ χ ↑p.1 * f p.1 * (χ ↑p.2 * g p.2) = χ (↑p.1 * ↑p.2) * (f p.1 * g p.2)
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ L (fun n ↦ ↑(Λ n)) s = -deriv riemannZeta s / riemannZeta s

Tactic:
suffices deriv (L 1) s = deriv riemannZeta s by
    rw [LSeries_vonMangoldt_eq hs, ← LSeries_one_eq_riemannZeta hs, this]

Goal state after:
s : ℂ
hs : 1 < s.re
⊢ deriv (L 1) s = deriv riemannZeta s
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.inl.inr.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : 0 < c
⊢ |a| ^ n + |c| ^ n = |b| ^ n

Tactic:
simp only [abs_of_pos, abs_of_neg, hn.neg_pow, neg_add_eq_iff_eq_add,
        *]

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: case pos
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this✝ : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit ↑p
⊢ (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ = (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s))

Tactic:
MulChar.map_nonunit _ this,

Goal state after:
case pos
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this✝ : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit ↑p
⊢ (1 - 0 * ↑p ^ (-s))⁻¹ = (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s))
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
h : PythagoreanTriple x0 y0 z0
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑k) (y0 * ↑k / ↑k) (↑k * z0 / ↑k)

Tactic:
Int.mul_ediv_cancel _ hk,

Goal state after:
case neg
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
h : PythagoreanTriple x0 y0 z0
hk : ↑k ≠ 0
⊢ PythagoreanTriple x0 (y0 * ↑k / ↑k) (↑k * z0 / ↑k)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
h : PythagoreanTriple x0 y0 z0
hk : ↑k ≠ 0
⊢ PythagoreanTriple x0 (y0 * ↑k / ↑k) (↑k * z0 / ↑k)

Tactic:
Int.mul_ediv_cancel _ hk,

Goal state after:
case neg
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
h : PythagoreanTriple x0 y0 z0
hk : ↑k ≠ 0
⊢ PythagoreanTriple x0 y0 (↑k * z0 / ↑k)
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
⊢ ∑' (p : Primes) (k : ℕ),
      χ (↑↑p ^ (k + 1)) * ↑(↑p ^ (k + 1)) ^ (-s) * ↑(Λ (↑p ^ (k + 1))) / ↑(Real.log (↑↑p ^ (k + 1))) =
    ∑' (n : { n // IsPrimePow n }), f ↑n

Tactic:
rw [← tsum_primes_pow_eq]

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
⊢ ∑' (p : Primes) (k : ℕ),
      χ (↑↑p ^ (k + 1)) * ↑(↑p ^ (k + 1)) ^ (-s) * ↑(Λ (↑p ^ (k + 1))) / ↑(Real.log (↑↑p ^ (k + 1))) =
    ∑' (p : Primes) (n : ℕ), f (↑p ^ (n + 1))

N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
⊢ Summable fun n ↦ f ↑n
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inl.inl
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp2✝ : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(m.gcd n)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hp2 : p ∣ Int.natAbs 2
hp2' : p = 2
⊢ ↑p ∣ m ^ 2 - n ^ 2 → False

Tactic:
hp2'

Goal state after:
case inl.inl
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp2✝ : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(m.gcd n)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hp2 : p ∣ Int.natAbs 2
hp2' : p = 2
⊢ ↑2 ∣ m ^ 2 - n ^ 2 → False
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
have hcr := pow_ne_zero r hc

Goal state after:
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
⊢ IsCoprime (C u * a ^ p) (C v * b ^ q)

Tactic:
rw [isCoprime_mul_units_left hu.isUnit_C hv.isUnit_C]

Goal state after:
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
⊢ IsCoprime (a ^ p) (b ^ q)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case mpr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ → mk φ = mk ψ

Tactic:
rintro (⟨h⟩ | ⟨h⟩)
    · exact congr_arg mk h
    · rw [← mk_conjugate_eq]
      exact congr_arg mk h

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

Goal state before:
pp: case neg.«0»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑x = 0
hc : 0 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1

pp: case neg.«1»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑x = 1
hc : 1 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1

pp: case neg.«2»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑x = 2
hc : 2 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1

Tactic:
· linarith [orderOf_pos_iff.2 ((CommGroup.mem_torsion x.1).1 x.2)]

Goal state after:
case neg.«1»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑x = 1
hc : 1 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1

case neg.«2»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑x = 2
hc : 2 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case e'_2.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝¹ x✝ : { x // mkComplex x = ⟨w, hw⟩ }
h :
  (match x✝¹ with
    | ⟨φ, hφ⟩ => ⟨↑φ, ⋯⟩) =
    match x✝ with
    | ⟨φ, hφ⟩ => ⟨↑φ, ⋯⟩
⊢ x✝¹ = x✝

Tactic:
Subtype.mk_eq_mk,

Goal state after:
case e'_2.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝¹ x✝ : { x // mkComplex x = ⟨w, hw⟩ }
h : ↑↑x✝¹ = ↑↑x✝
⊢ x✝¹ = x✝
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x✝ : { w // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (f ζ) k
him : |(f ζ).re| = ‖f ζ‖
this : ‖f ζ‖ = 1
⊢ (f ζ).re = 1 ∨ (f ζ).re = -1

Tactic:
rwa [← him, ← abs_one, abs_eq_abs] at this

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
⊢ ((basisMatrix K)ᵀ⁻¹ *ᵥ fun j ↦ (canonicalEmbedding K) ((algebraMap (𝓞 K) K) α) j) i =
    ↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)

Tactic:
rw [inv_mulVec_eq_vec (canonicalEmbedding_eq_basisMatrix_mulVec ((algebraMap (𝓞 K) K) α))]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
K : Type u_2
inst✝³ : Field K
inst✝² : IsTotallyReal K
inst✝¹ : Algebra F K
inst✝ : Algebra.IsAlgebraic F K
W : InfinitePlace K
⊢ (W.comap (algebraMap F K)).IsReal

Tactic:
exact IsReal.comap _ (IsTotallyReal.isReal W)

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

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsRamified k w
⊢ conjugate (w.comap (algebraMap k K)).embedding = (conjugate w.embedding).comp (algebraMap k K)

Tactic:
simp [conjugate_comp, comap_embedding_of_isReal _ ((isRamified_iff.1 h).2)]

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

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsRamified k w
⊢ ¬ComplexEmbedding.IsReal (conjugate w.embedding)

Tactic:
simpa using isComplex_iff.1 <| h.isComplex

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

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnmixed k φ
hv : ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ ComplexEmbedding.IsReal (mk φ).embedding

Tactic:
by simp [embedding_mk_eq_of_isReal, h hv]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : mixedSpace K
⊢ (∃ w, (normAtPlace w) x ≠ 0) ↔ ¬∀ (w : InfinitePlace K), (normAtPlace w) x = 0

Tactic:
not_forall

Goal state after:
K : Type u_1
inst✝ : Field K
x : mixedSpace K
⊢ (∃ w, (normAtPlace w) x ≠ 0) ↔ ∃ x_1, ¬(normAtPlace x_1) x = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
⊢ IsCompact (convexBodySum K B)

Tactic:
rw [Metric.isCompact_iff_isClosed_bounded]
  refine ⟨?_, convexBodySum_isBounded K B⟩
  convert! IsClosed.preimage (convexBodySumFun_continuous K) (isClosed_Icc : IsClosed (Set.Icc 0 B))
  ext
  simp [convexBodySumFun_nonneg]

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
hv : ¬∀ (x : K), (conjugate v.embedding) x = v.embedding x
⊢ ¬∀ (x : L), (conjugate w.embedding) x = w.embedding x

Tactic:
not_forall

Goal state after:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
hv : ∃ x, ¬(conjugate v.embedding) x = v.embedding x
⊢ ∃ x, ¬(conjugate w.embedding) x = w.embedding x
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case h
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
x : K
hx :
  ¬(conjugate (mk (w.embedding.comp (algebraMap K L))).embedding) x =
      (mk (w.embedding.comp (algebraMap K L))).embedding x
⊢ ¬(conjugate w.embedding) ((algebraMap K L) x) = w.embedding ((algebraMap K L) x)

Tactic:
rcases embedding_mk_eq (w.embedding.comp (algebraMap K L)) with (_ | _)

Goal state after:
case h.inl
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
x : K
hx :
  ¬(conjugate (mk (w.embedding.comp (algebraMap K L))).embedding) x =
      (mk (w.embedding.comp (algebraMap K L))).embedding x
h✝ : (mk (w.embedding.comp (algebraMap K L))).embedding = w.embedding.comp (algebraMap K L)
⊢ ¬(conjugate w.embedding) ((algebraMap K L) x) = w.embedding ((algebraMap K L) x)

case h.inr
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
x : K
hx :
  ¬(conjugate (mk (w.embedding.comp (algebraMap K L))).embedding) x =
      (mk (w.embedding.comp (algebraMap K L))).embedding x
h✝ : (mk (w.embedding.comp (algebraMap K L))).embedding = conjugate (w.embedding.comp (algebraMap K L))
⊢ ¬(conjugate w.embedding) ((algebraMap K L) x) = w.embedding ((algebraMap K L) x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case pos.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ : |(w₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ (w₀.embedding ↑a).im ^ 2 < ↑B ^ 2

Tactic:
rw [sq_lt_sq, NNReal.abs_eq, ← NNReal.sq_sqrt B]

Goal state after:
case pos.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ : |(w₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B ^ 2)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K

Tactic:
obtain ⟨⟨x, hx⟩, h_nz, h_mem⟩ := exists_ne_zero_mem_lattice_of_measure_mul_two_pow_le_measure
      h_fund (fun _ ↦ convexBodySum_neg_mem K B) (convexBodySum_convex K B)
      (convexBodySum_compact K B) h

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
x : mixedSpace K
hx : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨x, hx⟩ ≠ 0
h_mem : ↑⟨x, hx⟩ ∈ convexBodySum K B
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝ : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
hw : w.IsReal
⊢ (normAtPlace w) (fun w ↦ x ↑w, fun w ↦ ↑(x ↑w)) = x w

pp: case inr
K : Type u_1
inst✝ : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
hw : w.IsComplex
⊢ (normAtPlace w) (fun w ↦ x ↑w, fun w ↦ ↑(x ↑w)) = x w

Tactic:
· rw [normAtPlace_apply_of_isReal hw, Real.norm_of_nonneg hx]

Goal state after:
case inr
K : Type u_1
inst✝ : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
hw : w.IsComplex
⊢ (normAtPlace w) (fun w ↦ x ↑w, fun w ↦ ↑(x ↑w)) = x w
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:

Tactic:
(2 : ℝ) < (4 / 9) * (3 * π / 4) ^ 2 := by
      nlinarith [Real.pi_gt_three]
    _ ≤ (4 / 9 : ℝ) * (3 * π / 4) ^ finrank ℚ K := by
      gcongr
      linarith [Real.pi_gt_three]
    _ ≤ |(discr K : ℝ)| := mod_cast abs_discr_ge h

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
a : 𝓞 K
ha : a ∈ ↑↑J
h_nz : (Algebra.linearMap (𝓞 K) K) a ≠ 0
I₀ : Ideal (𝓞 K)
h_nm :
  ↑↑(absNorm ↑J * absNorm I₀) ≤
    ↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K)! /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
hI : span {a} = ↑J * I₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ := ⟨I₀, ⋯⟩
⊢ ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)

Tactic:
cast_mul,

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
a : 𝓞 K
ha : a ∈ ↑↑J
h_nz : (Algebra.linearMap (𝓞 K) K) a ≠ 0
I₀ : Ideal (𝓞 K)
h_nm :
  ↑(↑(absNorm ↑J) * ↑(absNorm I₀)) ≤
    ↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K)! /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
hI : span {a} = ↑J * I₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ := ⟨I₀, ⋯⟩
⊢ ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)