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

Goal state before:
pp: a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (2 * ↑π * I * ↑a * ↑n) * cexp (-(↑π * ↑n ^ 2 * ↑t)) = jacobiTheta₂_term n (↑a) (I * ↑t)

Tactic:
rw [jacobiTheta₂_term, ← Complex.exp_add]

Goal state after:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (2 * ↑π * I * ↑a * ↑n + -(↑π * ↑n ^ 2 * ↑t)) = cexp (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2 * (I * ↑t))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a x : ℝ
⊢ ↑(oddKernel (↑a) x) =
    cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))

Tactic:
oddKernel_def,

Goal state after:
a x : ℝ
⊢ jacobiTheta₂'' (↑a) (I * ↑x) =
    cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
h4 : (↑x).arg ≠ π
⊢ ↑(oddKernel (↑a) x) = ↑(1 / x ^ (3 / 2) * sinKernel (↑a) (1 / x))

Tactic:
oddKernel_def,

Goal state after:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
h4 : (↑x).arg ≠ π
⊢ jacobiTheta₂'' (↑a) (I * ↑x) = ↑(1 / x ^ (3 / 2) * sinKernel (↑a) (1 / x))
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ sinZeta a s = (cosZeta a s + I * sinZeta a s - (cosZeta a s + I * -sinZeta a s)) / (2 * I)

Tactic:
field

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

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < τ.im / normSq τ

Tactic:
exact div_pos hτ (normSq_pos.mpr (fun h ↦ lt_irrefl 0 (zero_im ▸ h ▸ hτ)))

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

Goal state before:
pp: case inr
s : ℂ
hs : s ≠ 0
⊢ (completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)) / (↑π ^ (-s / 2) * Gamma (s / 2)) =
    (s * completedRiemannZeta₀ s - 1 - s / (1 - s)) / (2 * ↑π ^ (-s / 2) * (s / 2 * Gamma (s / 2)))

Tactic:
field

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

Goal state before:
pp: s : ℂ
⊢ LSeriesSummable (fun n ↦ ↑(μ n)) s ↔ 1 < s.re

Tactic:
by
  refine ⟨fun H ↦ ?_, LSeriesSummable_of_bounded_of_one_lt_re (m := 1) fun n _ ↦ ?_⟩
  · by_contra! h
    exact not_LSeriesSummable_moebius_at_one <| LSeriesSummable.of_re_le_re (by simpa) H
  · norm_cast
    exact abs_moebius_le_one

Goal state after:
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:

Tactic:
(2 * N₀ : ℝ)
    _ = ((2 * N₀).smoothNumbersUpTo k).card + ((2 * N₀).roughNumbersUpTo k).card := by
        exact_mod_cast ((2 * N₀).smoothNumbersUpTo_card_add_roughNumbersUpTo_card k).symm
    _ ≤ m * (2 * N₀).sqrt + ((2 * N₀).roughNumbersUpTo k).card := by
        exact_mod_cast Nat.add_le_add_right ((2 * N₀).smoothNumbersUpTo_card_le k) _
    _ ≤ m * (2 * N₀).sqrt + 2 * N₀ * S := by grw [roughNumbersUpTo_card_le']; norm_cast

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
m n : ℕ
hmn : m ∣ n
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
obtain ⟨k, rfl⟩ := hmn

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ a ^ (m * k) + b ^ (m * k) ≠ c ^ (m * k)
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
⊢ [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE

Tactic:
tfae_have 1 → 2
  | h, a, b, c, ha, hb, hc, habc => by
    obtain hn | hn := n.even_or_odd
    · refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [hn.pow_abs, habc]
    obtain ha | ha := ha.lt_or_gt <;> obtain hb | hb := hb.lt_or_gt <;>
      obtain hc | hc := hc.lt_or_gt
    · refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_neg, neg_pow a, neg_pow b, neg_pow c, ← mul_add, *]
    · exact (by positivity : 0 < c ^ n).not_gt <| habc.symm.trans_lt <| add_neg (hn.pow_neg ha) <|
        hn.pow_neg hb
    · refine h b.natAbs c.natAbs a.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, add_neg_eq_iff_eq_add,
        eq_neg_add_iff_add_eq, *]
    · refine h a.natAbs c.natAbs b.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, neg_add_eq_iff_eq_add,
        *]
    · refine h c.natAbs a.natAbs b.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, neg_add_eq_iff_eq_add,
        eq_add_neg_iff_add_eq, *]
    · refine h c.natAbs b.natAbs a.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, add_neg_eq_iff_eq_add,
        *]
    · exact (by positivity : 0 < a ^ n + b ^ n).not_gt <| habc.trans_lt <| hn.pow_neg hc
    · refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, *]
  tfae_have 2 → 3
  | h, a, b, c, ha, hb, hc, habc => by
    rw [← Rat.num_ne_zero] at ha hb hc
    refine h (a.num * b.den * c.den) (a.den * b.num * c.den) (a.den * b.den * c.num)
      (by positivity) (by positivity) (by positivity) ?_
    have : (a.den * b.den * c.den : ℚ) ^ n ≠ 0 := by positivity
    refine Int.cast_injective <| (div_left_inj' this).1 ?_
    push_cast
    simp only [add_div, ← div_pow, mul_div_mul_comm, div_self (by positivity : (a.den : ℚ) ≠ 0),
      div_self (by positivity : (b.den : ℚ) ≠ 0), div_self (by positivity : (c.den : ℚ) ≠ 0),
      one_mul, mul_one, Rat.num_div_den, habc]
  tfae_have 3 → 1
  | h, a, b, c => mod_cast h a b c
  tfae_finish

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ HasProd (fun p ↦ (1 - ↑↑p ^ (-s))⁻¹) (riemannZeta s)

Tactic:
by
  rw [← tsum_riemannZetaSummand hs]
  apply eulerProduct_completely_multiplicative_hasProd <| summable_riemannZetaSummand hs

Goal state after:
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hs : b' ^ 2 = -d ^ 2 * m
hd : r * s = d ^ 2 ∨ r * s = -d ^ 2
h1 : r * s = -d ^ 2
⊢ False

Tactic:
have h2 : b' ^ 2 ≤ 0 := by
      rw [hs, (by ring : -d ^ 2 * m = -(d ^ 2 * m))]
      exact neg_nonpos.mpr ((mul_nonneg_iff_of_pos_right h4).mpr (sq_nonneg d))

Goal state after:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2✝ : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hs : b' ^ 2 = -d ^ 2 * m
hd : r * s = d ^ 2 ∨ r * s = -d ^ 2
h1 : r * s = -d ^ 2
h2 : b' ^ 2 ≤ 0
⊢ False
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case 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
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(m.gcd n)
hp2m : p ∣ (2 * m).natAbs
⊢ False

Tactic:
rw [Int.natAbs_mul] at hp2m
    rcases (Nat.Prime.dvd_mul hp).mp hp2m with hp2 | hpm
    · have hp2' : p = 2 := (Nat.le_of_dvd zero_lt_two hp2).antisymm hp.two_le
      revert hp1
      rw [hp2']
      apply mt Int.emod_eq_zero_of_dvd
      simp only [sq, Nat.cast_ofNat, Int.sub_emod, Int.mul_emod, hm, hn,
        mul_zero, EuclideanDomain.zero_mod, mul_one, zero_sub]
      decide
    apply mt (Int.dvd_coe_gcd (Int.natCast_dvd.mpr hpm)) hnp
    apply or_self_iff.mp
    apply Int.Prime.dvd_mul' hp
    rw [(by ring : n * n = -(m ^ 2 - n ^ 2) + m * m)]
    exact hp1.neg_right.add ((Int.natCast_dvd.2 hpm).mul_right _)

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inr.inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
ha : a ≠ 0
hb : b ≠ 0
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯

Tactic:
rw [Finset.disjUnion_eq_union, primeFactors_mul_eq_union ha hb]

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
⊢ radical a * (a / radical a) = a

Tactic:
← EuclideanDomain.mul_div_assoc _ radical_dvd_self,

Goal state after:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
⊢ radical a * a / radical a = a
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
⊢ (1 - (↑n / ↑m) ^ 2) / (1 + (↑n / ↑m) ^ 2) = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)

Tactic:
field

Goal state after:
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)
⊢ 2 * (↑n / ↑m) / (1 + (↑n / ↑m) ^ 2) = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)

Tactic:
field

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ absNorm (spanSingleton R⁰ x) = |(Algebra.norm ℚ) x|

Tactic:
rw [absNorm_eq' d (Ideal.span {r})]

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ ↑(Ideal.absNorm (Ideal.span {r})) / ↑|(Algebra.norm ℤ) ↑d| = |(Algebra.norm ℚ) x|

R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ d • ↑(spanSingleton R⁰ x) = Submodule.map (Algebra.linearMap R K) (Ideal.span {r})
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ^ torsionOrder K = 1
⊢ ζ ∈ CommGroup.torsion (𝓞 K)ˣ

Tactic:
rw [CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
    exact ⟨torsionOrder K, torsionOrder_pos K, h⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
⊢ Subgroup.map (Units.complexEmbedding φ) (torsion K) = rootsOfUnity (torsionOrder K) ℂ

Tactic:
apply Subgroup.eq_of_le_of_card_ge
  · rw [← rootsOfUnity_eq_torsion]
    exact map_rootsOfUnity _ (torsionOrder K)
  · let e := ((torsion K).equivMapOfInjective (Units.complexEmbedding φ)
      (Units.complexEmbedding_injective φ)).symm.toEquiv
    rw [Complex.card_rootsOfUnity, Nat.card_congr e, torsionOrder]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card (K →+* ℂ) = Fintype.card (ChooseBasisIndex ℤ (𝓞 K))

Tactic:
by
    rw [Embeddings.card, ← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ basisMatrix K =
    Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑(equivReindex K)) (RingHom.equivRatAlgHom K ℂ)

Tactic:
by
  ext; simp [Algebra.embeddingsMatrixReindex]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
⊢ (↑(integerLattice K) ∩ Metric.closedBall 0 r).Finite

Tactic:
by
  obtain hr | _ := lt_or_ge r 0
  · simp [Metric.closedBall_eq_empty.2 hr]
  · have heq : ∀ x, canonicalEmbedding K x ∈ Metric.closedBall 0 r ↔
        ∀ φ : K →+* ℂ, ‖φ x‖ ≤ r := by
      intro x; rw [← norm_le_iff, mem_closedBall_zero_iff]
    convert! (Embeddings.finite_of_norm_le K ℂ r).image (canonicalEmbedding K)
    ext; constructor
    · rintro ⟨⟨_, ⟨x, rfl⟩, rfl⟩, hx⟩
      exact ⟨x, ⟨SetLike.coe_mem x, fun φ => (heq _).mp hx φ⟩, rfl⟩
    · rintro ⟨x, ⟨hx1, hx2⟩, rfl⟩
      exact ⟨⟨x, ⟨⟨x, hx1⟩, rfl⟩, rfl⟩, (heq x).mpr hx2⟩

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

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
this : ((commMap K) x).2 ⟨InfinitePlace.mk φ, ⋯⟩ = 0.2 ⟨InfinitePlace.mk φ, ⋯⟩
⊢ x φ = 0

Tactic:
cases embedding_mk_eq φ with
    | inl h => rwa [← h, ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]
    | inr h =>
        apply RingHom.injective (starRingEnd ℂ)
        rwa [canonicalEmbedding.conj_apply _ h_mem, ← h, map_zero,
          ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]

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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : 0 ≤ ↑(discr K) ↔ Even (nrComplexPlaces K)
h : 0 < discr K
⊢ (discr K).sign = (-1) ^ nrComplexPlaces K

Tactic:
rw [Int.sign_eq_one_of_pos h, Even.neg_one_pow (this.mp <| Int.cast_nonneg h.le)]

Goal state after:
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) = convexBodySumFun x

Tactic:
convexBodySumFun,

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
⊢ convexBodySumFun (x + y) ≤ convexBodySumFun x + convexBodySumFun y

Tactic:
convexBodySumFun,

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : mixedSpace K
⊢ convexBodySumFun (c • x) = |c| * convexBodySumFun x

Tactic:
convexBodySumFun,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : mixedSpace K
⊢ ∑ w, ↑w.mult * (normAtPlace w) (c • x) = |c| * ∑ w, ↑w.mult * (normAtPlace w) x
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 = 0 ↔ ∀ (w : InfinitePlace K), (normAtPlace w) x = 0

Tactic:
convexBodySumFun,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ∑ w, ↑w.mult * (normAtPlace w) x = 0 ↔ ∀ (w : InfinitePlace K), (normAtPlace w) x = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : B ≤ 0
⊢ volume (convexBodySum K B) = 0

Tactic:
obtain hB | hB := lt_or_eq_of_le hB
  · suffices convexBodySum K B = ∅ by rw [this, measure_empty]
    ext x
    refine ⟨fun hx => ?_, fun h => h.elim⟩
    rw [Set.mem_ofPred] at hx
    linarith [convexBodySumFun_nonneg x]
  · suffices convexBodySum K B = { 0 } by rw [this, measure_singleton]
    ext
    rw [convexBodySum, Set.mem_ofPred_eq, Set.mem_singleton_iff, hB, ← convexBodySumFun_eq_zero_iff]
    exact (convexBodySumFun_nonneg _).ge_iff_eq'

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : K
⊢ convexBodySumFun ((mixedEmbedding K) x) ≤ B ↔ ∑ w, ↑w.mult * ↑w x ≤ B

Tactic:
convexBodySumFun,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : K
⊢ ∑ w, ↑w.mult * (normAtPlace w) ((mixedEmbedding K) x) ≤ B ↔ ∑ w, ↑w.mult * ↑w x ≤ B
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (NNReal.pi / 2) ^ nrComplexPlaces K ≠ 0

Tactic:
exact mul_ne_zero (pow_ne_zero _ two_ne_zero)
    (pow_ne_zero _ (div_ne_zero NNReal.pi_ne_zero two_ne_zero))

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 →+* ℂ
σ : Gal(K/k)
⊢ φ.comp ↑σ.symm = φ ∨ star φ = φ.comp ↑σ.symm ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ.symm

Tactic:
refine or_congr ⟨fun H ↦ ?_, fun H ↦ H ▸ rfl⟩ Iff.rfl

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)
H : φ.comp ↑σ.symm = φ
⊢ σ = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ convexBodySum K B = {a | convexBodySumFun (B⁻¹ • a) ≤ 1}

Tactic:
convexBodySumFun,

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ convexBodySum K B = {a | ∑ w, ↑w.mult * (normAtPlace w) (B⁻¹ • a) ≤ 1}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ¬mixedEmbedding.norm x ≠ 0 ↔ ¬∀ (w : InfinitePlace K), (normAtPlace w) x ≠ 0

Tactic:
simp_rw [ne_eq, mixedEmbedding.norm_eq_zero_iff, not_not, not_forall, not_not]

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
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
w' : InfinitePlace K
⊢ IsUnramified k w' ∧ w'.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w ↔ w' ∈ MulAction.orbit Gal(K/k) w

Tactic:
mem_orbit_iff,

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)
w' : InfinitePlace K
⊢ IsUnramified k w' ∧ w'.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w ↔
    w.comap (algebraMap k K) = w'.comap (algebraMap 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 : ¬IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
w' : InfinitePlace K
⊢ ¬IsUnramified k w' ∧ (fun x ↦ x.comap (algebraMap k K)) w = w'.comap (algebraMap k K) ↔
    w' ∈ MulAction.orbit Gal(K/k) w

Tactic:
mem_orbit_iff,

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)
w' : InfinitePlace K
⊢ ¬IsUnramified k w' ∧ (fun x ↦ x.comap (algebraMap k K)) w = w'.comap (algebraMap k K) ↔
    w.comap (algebraMap k K) = w'.comap (algebraMap k K)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
⊢ minkowskiBound K I = volume (convexBodySum K B)

Tactic:
convexBodySum_volume,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
⊢ minkowskiBound K I = ↑(convexBodySumFactor K) * ENNReal.ofReal B ^ finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n : ℕ
⊢ 4 / 9 * (3 * π / 4) ^ 2 = 2 ^ 4 / ((4 / π) ^ 2 * 2 ^ 2)

Tactic:
field

Goal state after: