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

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
this :
  ∃ p,
    0 < p ∧
      (fun t ↦
          rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t ↦ rexp (-p * t)
⊢ ∃ p, 0 < p ∧ F_nat 1 a =O[atTop] fun t ↦ rexp (-p * t)

Tactic:
let ⟨p, hp, hp'⟩ := this

Goal state after:
a : ℝ
ha : 0 ≤ a
this :
  ∃ p,
    0 < p ∧
      (fun t ↦
          rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t ↦ rexp (-p * t)
p : ℝ
hp : 0 < p
hp' :
  (fun t ↦
      rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
    fun t ↦ rexp (-p * t)
⊢ ∃ p, 0 < p ∧ F_nat 1 a =O[atTop] fun t ↦ rexp (-p * t)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - if ↑a = 0 then 1 else 0)

Tactic:
simp_rw [AddCircle.coe_eq_zero_iff, zsmul_one]

Goal state after:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t))
    (evenKernel (↑a) t - if ∃ n, ↑n = a then 1 else 0)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ ∑' (c : ℤ), jacobiTheta₂'_term ((Equiv.neg ℤ) c) (-z) τ = ∑' (b : ℤ), -jacobiTheta₂'_term b z τ

Tactic:
congr 1 with n

Goal state after:
case e_f
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂'_term ((Equiv.neg ℤ) n) (-z) τ = -jacobiTheta₂'_term n z τ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ ∑' (b : ℤ), -(starRingEnd ℂ) (jacobiTheta₂'_term b z τ) =
    ∑' (n : ℤ), jacobiTheta₂'_term n (-(starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
congr 1 with n

Goal state after:
case e_f
z τ : ℂ
n : ℤ
⊢ -(starRingEnd ℂ) (jacobiTheta₂'_term n z τ) = jacobiTheta₂'_term n (-(starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
Complex.cos,

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.cos (↑π * s / 2) * cosZeta a s +
      2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.sin (↑π * s / 2) * sinZeta a s =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (-↑π * I * s / 2) * (cosZeta a s + I * sinZeta a s) +
        cexp (↑π * I * s / 2) * (cosZeta (-a) s + I * sinZeta (-a) s))

Tactic:
Complex.cos,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.sin (↑π * s / 2) * sinZeta a s =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (-↑π * I * s / 2) * (cosZeta a s + I * sinZeta a s) +
        cexp (↑π * I * s / 2) * (cosZeta (-a) s + I * sinZeta (-a) s))
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
hs' : ∀ (n : ℕ), s ≠ -↑n
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.cos (↑π * s / 2) * hurwitzZetaEven a s +
      I * (2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.sin (↑π * s / 2) * hurwitzZetaOdd a s) =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (↑π * I * s / 2) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-↑π * I * s / 2) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))

Tactic:
Complex.cos,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
hs' : ∀ (n : ℕ), s ≠ -↑n
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) *
        hurwitzZetaEven a s +
      I * (2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.sin (↑π * s / 2) * hurwitzZetaOdd a s) =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (↑π * I * s / 2) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-↑π * I * s / 2) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
⊢ (∑' (b : ℕ), if b = 0 then 0 else ↑π ^ (-s / 2) * Gamma (s / 2) / ↑b ^ s) =
    ∑' (x : ℕ), ↑π ^ (-s / 2) * Gamma (s / 2) / ↑x ^ s

Tactic:
congr 1 with n

Goal state after:
case e_f
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
n : ℕ
⊢ (if n = 0 then 0 else ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s) = ↑π ^ (-s / 2) * Gamma (s / 2) / ↑n ^ s
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: N k : ℕ
⊢ ↑(N.roughNumbersUpTo k).card ≤ ↑N * ∑ p ∈ N.succ.primesBelow \ k.primesBelow, 1 / ↑p

Tactic:
simp_rw [Finset.mul_sum, mul_one_div]
  exact (Nat.cast_le.mpr <| roughNumbersUpTo_card_le N k).trans <|
    cast_sum (R := ℝ) .. ▸ Finset.sum_le_sum fun n _ ↦ cast_div_le

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

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.HurwitzZetaOdd

Goal state before:
pp: case hg
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ 2 * HurwitzKernelBounds.f_nat 1 0 t n) (2 * ∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n)

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
⊢ ∀ (i : ℕ), ‖2 * ↑i * Real.sin (2 * π * a * ↑i) * rexp (-π * ↑i ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 1 0 t i

Tactic:
· exact (HurwitzKernelBounds.summable_f_nat 1 0 ht).hasSum.mul_left _

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
⊢ ∀ (i : ℕ), ‖2 * ↑i * Real.sin (2 * π * a * ↑i) * rexp (-π * ↑i ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 1 0 t i
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun n ↦ (cexp (2 * ↑π * I * ↑a * ↑n) + cexp (-(2 * ↑π * I * ↑a * ↑n))) / 2 / ↑n ^ s) (cosZeta (↑a) s)
⊢ HasSum (fun n ↦ Complex.cos (2 * ↑π * ↑a * ↑n) / ↑n ^ s) (cosZeta (↑a) s)

Tactic:
Complex.cos,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun n ↦ (cexp (2 * ↑π * I * ↑a * ↑n) + cexp (-(2 * ↑π * I * ↑a * ↑n))) / 2 / ↑n ^ s) (cosZeta (↑a) s)
⊢ HasSum (fun n ↦ (cexp (2 * ↑π * ↑a * ↑n * I) + cexp (-(2 * ↑π * ↑a * ↑n) * I)) / 2 / ↑n ^ s) (cosZeta (↑a) s)
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
⊢ FermatLastTheoremWith R n

Tactic:
intro a b c ha hb hc habc

Goal state after:
n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ False
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
⊢ a * a % 2 = 1

Tactic:
Int.mul_emod,

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
⊢ a % 2 * (a % 2) % 2 = 1
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)
⊢ ∑' (b : Primes) (b_1 : ℕ), (χ ↑↑b * ↑↑b ^ (-s)) ^ (b_1 + 1) / (↑b_1 + 1) =
    ∑' (n : ℕ), χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) / ↑n ^ s

Tactic:
calc
    _ = ∑' (p : Primes) (k : ℕ), (χ (p ^ (k + 1)) * ((p ^ (k + 1) : ℕ) : ℂ) ^ (-s)) *
          Λ (p ^ (k + 1)) / Real.log (p ^ (k + 1)) := by
      refine tsum_congr fun p ↦ tsum_congr fun k ↦ ?_
      have : Complex.log p ≠ 0 := mod_cast p.prop.log_ne_zero
      simp [mul_pow, ← cpow_nat_mul, ← natCast_cpow_natCast_mul, vonMangoldt_apply_pow,
        vonMangoldt_apply_prime p.2, field]
    _ = ∑' n : {n : ℕ // IsPrimePow n}, f n := by
      rw [← tsum_primes_pow_eq]
      · exact tsum_congr fun p ↦ tsum_congr fun k ↦ (by unfold f; simp; ring)
      · apply comp_injective _ Subtype.coe_injective (f := f)
        apply of_norm_bounded_eventually_nat (g := (↑· ^ (-s.re)))
        · simp [hs]
        · filter_upwards [eventually_gt_atTop 1] with n hn
          simp only [f, norm_mul, norm_div, norm_real, norm_eq_abs]
          grw [norm_le_one, vonMangoldt_le_log]
          have := log_pos (x := n) (mod_cast hn)
          field_simp
          rw [← ofReal_natCast n, norm_cpow_eq_rpow_re_of_nonneg (by simp) (by simp; grind)]
          simp
    _ = _ := by
      simp only [div_eq_mul_inv _ (_ ^ _), ← cpow_neg]
      suffices (Function.support f) ⊆ {n | IsPrimePow n} from
        tsum_subtype_eq_of_support_subset this
      intro n hn
      contrapose! hn
      simp [f, vonMangoldt_eq_zero_iff.mpr hn]

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : NormalizationMonoid M
inst✝¹ : UniqueFactorizationMonoid M
a : M
inst✝ : DecidableEq M
⊢ (normalizedFactors a).toFinset = primeFactors a

Tactic:
by
  unfold primeFactors
  convert rfl

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

Goal state before:
pp: case mpr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : Irreducible a
hb : b ≠ 0
ha' : a ∣ b
c : M
hc : c ∈ normalizedFactors b
hc' : Associated a c
⊢ a ∣ radical b

Tactic:
exact hc'.dvd.trans (Finset.dvd_prod_of_mem _ (by simpa [mem_primeFactors] using hc))

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : a ∣ b
hb₀ : b ≠ 0
⊢ radical a ∣ radical b

Tactic:
by
  obtain rfl | ha₀ := eq_or_ne a 0
  · simp
  rw [dvd_iff_normalizedFactors_le_normalizedFactors ha₀ hb₀] at h
  rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors]
  exact Multiset.subset_of_le h

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg.inl.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ⋯
w : ℚ := ⋯
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 : ℚ := ⋯
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ⋯
n : ℤ := ⋯
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)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 1
⊢ m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0

Tactic:
apply Or.intro_left
      exact And.intro hm2 hn2

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
⊢ |(Algebra.norm ℚ) ((algebraMap R K) r)| / |(Algebra.norm ℚ) ((algebraMap R K) ↑d)| = |(Algebra.norm ℚ) x|

Tactic:
rw [hr, Algebra.smul_def, map_mul, abs_mul, mul_div_assoc, mul_div_cancel₀ _ (by
      rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]
      exact nonZeroDivisors.coe_ne_zero _)]

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
⊢ ↑(Ideal.absNorm (Ideal.span {r})) / ↑|(Algebra.norm ℤ) ↑d| = |(Algebra.norm ℚ) x|

Tactic:
rw [Ideal.absNorm_span_singleton]
    simp_rw [Nat.cast_natAbs, Int.cast_abs, show ((Algebra.norm ℤ _) : ℚ) = algebraMap ℤ ℚ
      (Algebra.norm ℤ _) by rfl, ← Algebra.norm_localization ℤ ℤ⁰ (Sₘ := K) _]
    rw [hr, Algebra.smul_def, map_mul, abs_mul, mul_div_assoc, mul_div_cancel₀ _ (by
      rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]
      exact nonZeroDivisors.coe_ne_zero _)]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ #({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}) = 1

Tactic:
rw [ComplexEmbedding.isReal_iff.mp (isReal_iff.mp hw), Finset.union_idempotent,
      Finset.card_singleton]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v w : InfinitePlace K
h✝ : (↑w).IsEquiv ↑v
t : ℝ
left✝ : 0 < t
h : (fun x ↦ ↑w x ^ t) = ⇑↑v
⊢ w = v

Tactic:
exact ext _ _ fun k ↦ by simpa [eq_one_of_rpow_eq h, ext, coe_apply] using funext_iff.1 h k

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ volume (convexBodyLT K f) = ↑(convexBodyLTFactor K) * ↑(∏ w, f w ^ w.mult)

Tactic:
calc
    _ = (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (2 * (f x.val))) *
          ∏ x : {w // InfinitePlace.IsComplex w}, ENNReal.ofReal (f x.val) ^ 2 * NNReal.pi := by
      simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball, Complex.volume_ball]
    _ = ((2 : ℝ≥0) ^ nrRealPlaces K
          * (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val)))
          * ((∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2) *
            NNReal.pi ^ nrComplexPlaces K) := by
      simp_rw [ofReal_mul (by simp : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
        Finset.card_univ, ofReal_ofNat, ofReal_coe_nnreal, coe_ofNat]
    _ = (convexBodyLTFactor K) * ((∏ x : {w // InfinitePlace.IsReal w}, .ofReal (f x.val)) *
        (∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2)) := by
      simp_rw [convexBodyLTFactor, coe_mul, ENNReal.coe_pow]
      ring
    _ = (convexBodyLTFactor K) * ∏ w, (f w) ^ (mult w) := by
      simp_rw [prod_eq_prod_mul_prod, coe_mul, ofNNReal_finsetProd, mult_isReal, mult_isComplex,
        pow_one, ENNReal.coe_pow, ofReal_coe_nnreal]

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

Goal state before:
pp: case convert_6
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ b ≠ 0

Tactic:
rw [eq_b]
    exact mul_ne_zero hb.right hb.left

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

Goal state before:
pp: case refine_1.inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
wj : { w // w.IsComplex } × Fin 2
⊢ K →+* ℂ

Tactic:
rcases wj with ⟨w, j⟩

Goal state after:
case refine_1.inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : { w // w.IsComplex }
j : Fin 2
⊢ K →+* ℂ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ ↥↑↑I ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
⊢ ENNReal.ofReal |(Basis.det ?b₀) (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e.symm)| *
      volume (fundamentalDomain ?b₀) =
    ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * volume (fundamentalDomain (latticeBasis K))

Tactic:
mixedEmbedding.det_basisOfFractionalIdeal_eq_norm

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ ↥↑↑I ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
⊢ ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * volume (fundamentalDomain (latticeBasis K)) =
    ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * volume (fundamentalDomain (latticeBasis K))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume.real (fundamentalDomain (latticeBasis K)) = 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|

Tactic:
measureReal_def,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (volume (fundamentalDomain (latticeBasis K))).toReal = 2⁻¹ ^ nrComplexPlaces K * √|↑(discr 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)ˣ
⊢ volume.real (fundamentalDomain (fractionalIdealLatticeBasis K I)) =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|

Tactic:
measureReal_def,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ (volume (fundamentalDomain (fractionalIdealLatticeBasis K I))).toReal =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr 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)ˣ
⊢ (volume (fundamentalDomain (fractionalIdealLatticeBasis K I))).toReal =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|

Tactic:
volume_fundamentalDomain_fractionalIdealLatticeBasis,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ (ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * volume (fundamentalDomain (latticeBasis K))).toReal =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
w₀ : { w // w.IsComplex }
h : minkowskiBound K I < volume (convexBodyLT' K f w₀)
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 ∧
      (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧
        |((↑w₀).embedding a).re| < 1 ∧ |((↑w₀).embedding a).im| < ↑(f ↑w₀) ^ 2

Tactic:
obtain ⟨⟨x, hx⟩, h_nz, h_mem⟩ := exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure
    h_fund (convexBodyLT'_neg_mem K f w₀) (convexBodyLT'_convex K f w₀) h

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
w₀ : { w // w.IsComplex }
h : minkowskiBound K I < volume (convexBodyLT' K f w₀)
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⟩ ∈ convexBodyLT' K f w₀
⊢ ∃ a ∈ ↑I,
    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.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr ((commMap K) x)) c) = (matrixToStdBasis K *ᵥ x ∘ ⇑(indexEquiv K)) c

Tactic:
simp_rw [commMap, matrixToStdBasis, LinearMap.coe_mk, AddHom.coe_mk,
    mulVec, dotProduct, Function.comp_apply, index, Fintype.sum_sum_type,
    diagonal_one, reindex_apply, ← univ_product_univ, sum_product,
    indexEquiv_apply_isReal, Fin.sum_univ_two, indexEquiv_apply_isComplex_fst,
    indexEquiv_apply_isComplex_snd, smul_of, smul_cons, smul_eq_mul,
    mul_one, Matrix.smul_empty, Equiv.prodComm_symm, Equiv.coe_prodComm]
  cases c with
  | inl w =>
      simp_rw [stdBasis_apply_isReal, fromBlocks_apply₁₁, fromBlocks_apply₁₂,
        one_apply, Matrix.zero_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_univ, ite_true,
        add_zero, sum_const_zero, add_zero, ← conj_eq_iff_re, hx (embedding w.val),
        conjugate_embedding_eq_of_isReal w.prop]
  | inr c =>
    rcases c with ⟨w, j⟩
    fin_cases j
    · simp only [Fin.zero_eta, Fin.isValue, stdBasis_apply_isComplex_fst, re_eq_add_conj,
        mul_neg, fromBlocks_apply₂₁, Matrix.zero_apply, zero_mul, sum_const_zero,
        fromBlocks_apply₂₂, submatrix_apply, Prod.swap_prod_mk, blockDiagonal_apply, of_apply,
        cons_val', cons_val_zero, empty_val', cons_val_fin_one, ite_mul, cons_val_one,
        sum_add_distrib, sum_ite_eq, mem_univ, ↓reduceIte, ← hx (embedding w), zero_add]
      ring
    · simp only [Fin.mk_one, Fin.isValue, stdBasis_apply_isComplex_snd, im_eq_sub_conj,
        mul_neg, fromBlocks_apply₂₁, Matrix.zero_apply, zero_mul, sum_const_zero,
        fromBlocks_apply₂₂, submatrix_apply, Prod.swap_prod_mk, blockDiagonal_apply, of_apply,
        cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_one, ite_mul, neg_mul,
        sum_add_distrib, sum_ite_eq, mem_univ, ↓reduceIte, ← hx (embedding w), zero_add]
      ring_nf; simp [field]

Goal state after: