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

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

Tactic:
refine tsum_congr (fun n ↦ ?_)

Goal state after:
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂'_term n z (τ + 2) = jacobiTheta₂'_term n z τ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ ∑' (n : ℤ), 2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * (z + 1) + ↑π * I * ↑n ^ 2 * τ) =
    ∑' (n : ℤ), 2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)

Tactic:
refine tsum_congr (fun n ↦ ?_)

Goal state after:
z τ : ℂ
n : ℤ
⊢ 2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * (z + 1) + ↑π * I * ↑n ^ 2 * τ) =
    2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      cexp (2 * ↑π * I * ↑a * ↑↑(n + 1)) * ↑(rexp (-π * ↑↑(n + 1) ^ 2 * t)) +
        cexp (2 * ↑π * I * ↑a * ↑(-↑(n + 1))) * ↑(rexp (-π * ↑(-↑(n + 1)) ^ 2 * t)))
    (↑(cosKernel (↑a) t) + cexp (2 * ↑π * I * ↑a * 0) * ↑(rexp (-π * 0 ^ 2 * t)) -
      (cexp (2 * ↑π * I * ↑a * 0) * ↑(rexp (-π * 0 ^ 2 * t)) + cexp (2 * ↑π * I * ↑a * 0) * ↑(rexp (-π * 0 ^ 2 * t))))
⊢ HasSum (fun x ↦ ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)

Tactic:
zero_pow two_ne_zero,

Goal state after:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      cexp (2 * ↑π * I * ↑a * ↑↑(n + 1)) * ↑(rexp (-π * ↑↑(n + 1) ^ 2 * t)) +
        cexp (2 * ↑π * I * ↑a * ↑(-↑(n + 1))) * ↑(rexp (-π * ↑(-↑(n + 1)) ^ 2 * t)))
    (↑(cosKernel (↑a) t) + cexp (2 * ↑π * I * ↑a * 0) * ↑(rexp (-π * 0 * t)) -
      (cexp (2 * ↑π * I * ↑a * 0) * ↑(rexp (-π * 0 * t)) + cexp (2 * ↑π * I * ↑a * 0) * ↑(rexp (-π * 0 * t))))
⊢ HasSum (fun x ↦ ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i ≠ 0
⊢ ‖a i * ↑(r i)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re

Tactic:
norm_mul,

Goal state after:
case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i ≠ 0
⊢ ‖a i‖ * ‖↑(r i)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖2 * Real.cos (2 * π * a * (↑n + 1)) * rexp (-π * (↑n + 1) ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 0 1 t n

Tactic:
norm_mul,

Goal state after:
a p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖2 * Real.cos (2 * π * a * (↑n + 1))‖ * ‖rexp (-π * (↑n + 1) ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 0 1 t n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖2 * Real.cos (2 * π * a * (↑n + 1))‖ * ‖rexp (-π * (↑n + 1) ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 0 1 t n

Tactic:
norm_mul,

Goal state after:
a p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖2‖ * ‖Real.cos (2 * π * a * (↑n + 1))‖ * ‖rexp (-π * (↑n + 1) ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 0 1 t n
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: ⊢ abscissaOfAbsConv 1 = 1

Tactic:
abscissaOfAbsConv_one

Goal state after:
⊢ 1 = 1
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ abscissaOfAbsConv 1 < ↑s.re

Tactic:
abscissaOfAbsConv_one

Goal state after:
s : ℂ
hs : 1 < s.re
⊢ 1 < ↑s.re
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case h
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖2 * ↑n * Real.sin (2 * π * a * ↑n) * rexp (-π * ↑n ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 1 0 t n

Tactic:
norm_mul,

Goal state after:
case h
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖2 * ↑n * Real.sin (2 * π * a * ↑n)‖ * ‖rexp (-π * ↑n ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 1 0 t n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case h
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖2 * ↑n * Real.sin (2 * π * a * ↑n)‖ * ‖rexp (-π * ↑n ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 1 0 t n

Tactic:
norm_mul,

Goal state after:
case h
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖2 * ↑n‖ * ‖Real.sin (2 * π * a * ↑n)‖ * ‖rexp (-π * ↑n ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 1 0 t n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case h
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖2 * ↑n‖ * ‖Real.sin (2 * π * a * ↑n)‖ * ‖rexp (-π * ↑n ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 1 0 t n

Tactic:
norm_mul,

Goal state after:
case h
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖2‖ * ‖↑n‖ * ‖Real.sin (2 * π * a * ↑n)‖ * ‖rexp (-π * ↑n ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 1 0 t n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
n : ℤ
⊢ ‖-I * cexp (↑(2 * π * a * ↑n) * I)‖ / 2 = 1 / 2

Tactic:
norm_mul,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
n : ℤ
⊢ ‖-I‖ * ‖cexp (↑(2 * π * a * ↑n) * I)‖ / 2 = 1 / 2
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
hs : 1 < s.re
x✝ : Primes
⊢ ↑↑x✝ ^ (-s) = 1 * ↑↑x✝ ^ (-s)

Tactic:
one_mul

Goal state after:
s : ℂ
hs : 1 < s.re
x✝ : Primes
⊢ ↑↑x✝ ^ (-s) = ↑↑x✝ ^ (-s)
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inl
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ 0 + b ^ 0 + c ^ 0 = 0
⊢ IsCoprime a b

pp: case inr
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ IsCoprime a b

Tactic:
· simp only [pow_zero, Int.reduceAdd, OfNat.ofNat_ne_zero] at HF

Goal state after:
case inr
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ IsCoprime a b
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ ↑(x.gcd y) ∣ z

pp: case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ ↑(x.gcd y) ∣ z

Tactic:
· obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0
    have hz : z = 0 := by
      simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero,
        or_self_iff] using h
    simp [h0, hz]

Goal state after:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ ↑(x.gcd y) ∣ z
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑(1 * k) ∣ z

Tactic:
one_mul

Goal state after:
case neg
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑k ∣ z
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Primes
⊢ ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1

Tactic:
norm_mul,

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Primes
⊢ ‖χ ↑↑p‖ * ‖↑↑p ^ (-s)‖ < 1
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Primes
⊢ 1 * ↑↑p ^ (-s.re) < 1

Tactic:
one_mul

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Primes
⊢ ↑↑p ^ (-s.re) < 1
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 * ↑k) (y0 * ↑k) (↑(1 * k) * z0)
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑(1 * k)) (y0 * ↑k / ↑(1 * k)) (↑(1 * k) * z0 / ↑(1 * k))

Tactic:
one_mul

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 * ↑k) (y0 * ↑k) (↑k * z0)
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑k) (y0 * ↑k / ↑k) (↑k * z0 / ↑k)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
⊢ v = 2 * q / (1 + q ^ 2)

Tactic:
apply ht4.1

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ ¬w.IsReal ↔ w.IsComplex

Tactic:
isComplex_iff,

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ ¬w.IsReal ↔ ¬ComplexEmbedding.IsReal w.embedding
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ ¬w.IsComplex ↔ w.IsReal

Tactic:
isComplex_iff,

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ ¬¬ComplexEmbedding.IsReal w.embedding ↔ w.IsReal
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∑ w, w.mult = finrank ℚ K

Tactic:
rw [← Embeddings.card K ℂ, Fintype.card, Finset.card_eq_sum_ones, ← Finset.univ.sum_fiberwise
    (fun φ => InfinitePlace.mk φ)]
  exact Finset.sum_congr rfl
    (fun _ _ => by rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq])

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
⊢ 1 ≤ ↑|↑((Algebra.norm ℤ) a)|

Tactic:
← Int.cast_one,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
⊢ ↑1 ≤ ↑|↑((Algebra.norm ℤ) a)|
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
ψ : K →ₐ[ℚ] ℂ
⊢ w.embedding.toRatAlgHom ↑x = ψ ↑x → w.embedding.toRatAlgHom = ψ

Tactic:
hψ

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
⊢ w.embedding.toRatAlgHom = ψ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding ↑x = ψ ↑x
h : 1 ≤ ‖w.embedding ↑x‖
⊢ w = mk ψ.toRingHom

Tactic:
hψ

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding ↑x = ψ ↑x
h : 1 ≤ ‖ψ ↑x‖
⊢ w = mk ψ.toRingHom
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case refine_2
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsMixed k φ
⊢ (mk φ).IsComplex ∧ ((mk φ).comap (algebraMap k K)).IsReal

Tactic:
isComplex_iff,

Goal state after:
case refine_2
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsMixed k φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding ∧ ((mk φ).comap (algebraMap k K)).IsReal
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ convexBodySumFun x = ∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖

Tactic:
convexBodySumFun_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ∑ w, ↑w.mult * (normAtPlace w) x = ∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
x✝ : w ∈ Finset.univ
⊢ (normAtPlace w) x ≤ convexBodySumFun x

Tactic:
convexBodySumFun_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
x✝ : w ∈ Finset.univ
⊢ (normAtPlace w) x ≤ ∑ w, ↑w.mult * (normAtPlace w) x
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
⊢ volume (fundamentalDomain (latticeBasis K)) = 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊)

Tactic:
let M := (mixedEmbedding.stdBasis K).toMatrix ((latticeBasis K).reindex e.symm)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
⊢ volume (fundamentalDomain (latticeBasis K)) = 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊)
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 →+* ℂ
σ : Gal(K/k)
⊢ φ.comp ↑σ.symm = φ ∨ conjugate (φ.comp ↑σ.symm) = φ ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ

Tactic:
rw [← ComplexEmbedding.isConj_symm, ComplexEmbedding.conjugate, star_eq_iff_star_eq]

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
⊢ φ.comp ↑σ.symm = φ ∨ star φ = φ.comp ↑σ.symm ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ.symm
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case e'_3.e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal B ^ finrank ℝ (mixedSpace K)

Tactic:
mixedEmbedding.finrank

Goal state after:
case e'_3.e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ ENNReal.ofReal B ^ finrank ℚ K = ENNReal.ofReal B ^ finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 1 * 1 = 1

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ NullMeasurableSet (Set.univ.pi fun x ↦ Set.Ico 0 1) volume

Tactic:
one_mul

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 1 = 1

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ NullMeasurableSet (Set.univ.pi fun x ↦ Set.Ico 0 1) volume
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
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : (fun x ↦ x.comap (algebraMap k K)) w ∈ {w | IsUnramifiedIn K w}
⊢ #({a ∈ {w | IsUnramified k w} | a.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w}) = Nat.card Gal(K/k)

Tactic:
mem_filter_univ

Goal state after:
k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
⊢ #({a ∈ {w | IsUnramified k w} | a.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w}) = Nat.card Gal(K/k)
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
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : (fun x ↦ x.comap (algebraMap k K)) w ∈ {x | ¬IsUnramifiedIn K x}
⊢ #({a ∉ {w | IsUnramified k w} | a.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w}) =
    Nat.card Gal(K/k) / 2

Tactic:
mem_filter_univ

Goal state after:
k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : ¬IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
⊢ #({a ∉ {w | IsUnramified k w} | a.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w}) =
    Nat.card Gal(K/k) / 2
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
i✝ j✝ : index K
⊢ ofRealHom (((mixedEmbedding.stdBasis K).repr ((latticeBasis K) (e j✝))) i✝) =
    (matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ) i✝ j✝

Tactic:
latticeBasis_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
i✝ j✝ : index K
⊢ ofRealHom (((mixedEmbedding.stdBasis K).repr ((mixedEmbedding K) ((integralBasis K) (e j✝)))) i✝) =
    (matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ) i✝ j✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
h : minkowskiBound K 1 < volume (convexBodyLT K f)
w✝ : K
h_mem : w✝ ∈ ↑1
h_nz : w✝ ≠ 0
h_bd : ∀ (w : InfinitePlace K), w w✝ < ↑(f w)
⊢ ∃ a, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(f w)

Tactic:
obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
h : minkowskiBound K 1 < volume (convexBodyLT K f)
a : 𝓞 K
h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1
h_nz : (algebraMap (𝓞 K) K) a ≠ 0
h_bd : ∀ (w : InfinitePlace K), w ((algebraMap (𝓞 K) K) a) < ↑(f w)
⊢ ∃ a, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(f w)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
h : minkowskiBound K 1 < volume (convexBodyLT' K f w₀)
w✝ : K
h_mem : w✝ ∈ ↑1
h_nz : w✝ ≠ 0
h_bd :
  (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w w✝ < ↑(f w)) ∧
    |((↑w₀).embedding w✝).re| < 1 ∧ |((↑w₀).embedding w✝).im| < ↑(f ↑w₀) ^ 2
⊢ ∃ a,
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w ↑a < ↑(f w)) ∧
        |((↑w₀).embedding ↑a).re| < 1 ∧ |((↑w₀).embedding ↑a).im| < ↑(f ↑w₀) ^ 2

Tactic:
obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
h : minkowskiBound K 1 < volume (convexBodyLT' K f w₀)
a : 𝓞 K
h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1
h_nz : (algebraMap (𝓞 K) K) a ≠ 0
h_bd :
  (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w ((algebraMap (𝓞 K) K) a) < ↑(f w)) ∧
    |((↑w₀).embedding ((algebraMap (𝓞 K) K) a)).re| < 1 ∧ |((↑w₀).embedding ((algebraMap (𝓞 K) K) a)).im| < ↑(f ↑w₀) ^ 2
⊢ ∃ a,
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w ↑a < ↑(f w)) ∧
        |((↑w₀).embedding ↑a).re| < 1 ∧ |((↑w₀).embedding ↑a).im| < ↑(f ↑w₀) ^ 2
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 : v.IsComplex
⊢ w.IsComplex

Tactic:
isComplex_iff,

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 : ¬ComplexEmbedding.IsReal v.embedding
⊢ ¬ComplexEmbedding.IsReal w.embedding
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Injective fun r ↦ r • 1

Tactic:
{ simpa only [Complex.real_smul, mul_one] using Complex.ofReal_injective }

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℝ (mixedSpace K) = finrank ℚ K

Tactic:
mixedEmbedding.finrank

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℚ K = finrank ℚ K