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

Goal state before:
pp: case inr.e_a.e_a.e_a
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) +
            (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) /
          ↑n ^ s /
        2)
    (completedSinZeta (↑a) s)
n : ℕ
h : n ≠ 0
⊢ I * (cexp (-(2 * ↑π * ↑a * ↑n * I)) - cexp (2 * ↑π * ↑a * ↑n * I)) =
    I * (cexp (-(2 * ↑π * I * ↑a * ↑n)) - cexp (2 * ↑π * I * ↑a * ↑n))

Tactic:
congr 3

Goal state after:
case inr.e_a.e_a.e_a.e_a.e_a
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) +
            (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) /
          ↑n ^ s /
        2)
    (completedSinZeta (↑a) s)
n : ℕ
h : n ≠ 0
⊢ -(2 * ↑π * ↑a * ↑n * I) = -(2 * ↑π * I * ↑a * ↑n)

case inr.e_a.e_a.e_a.e_a.e_a
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) +
            (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) /
          ↑n ^ s /
        2)
    (completedSinZeta (↑a) s)
n : ℕ
h : n ≠ 0
⊢ 2 * ↑π * ↑a * ↑n * I = 2 * ↑π * I * ↑a * ↑n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n ↦ ↑n + a
c : ℤ → ℂ := fun n ↦ 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑(r n) * ↑(rexp (-π * r n ^ 2 * t))) (↑(oddKernel (↑a) t) / 2)
h_sum : Summable fun i ↦ ‖c i‖ / |r i| ^ s.re
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaOdd (↑a) s)

Tactic:
completedHurwitzZetaOdd,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n ↦ ↑n + a
c : ℤ → ℂ := fun n ↦ 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑(r n) * ↑(rexp (-π * r n ^ 2 * t))) (↑(oddKernel (↑a) t) / 2)
h_sum : Summable fun i ↦ ‖c i‖ / |r i| ^ s.re
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2)
    ((hurwitzOddFEPair ↑a).Λ ((s + 1) / 2) / 2)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
x0 : ℤ
hx2 : x - 1 = x0 * 2
y0 : ℤ
hy2 : y - 1 = y0 * 2
⊢ ∃ x0 y0, x = x0 * 2 + 1 ∧ y = y0 * 2 + 1

Tactic:
rw [sub_eq_iff_eq_add] at hx2 hy2

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
x0 : ℤ
hx2 : x = x0 * 2 + 1
y0 : ℤ
hy2 : y = y0 * 2 + 1
⊢ ∃ x0 y0, x = x0 * 2 + 1 ∧ y = y0 * 2 + 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 (↑k * x0) (y0 * ↑k) (↑k * z0)
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑k) (y0 * ↑k / ↑k) (↑k * z0 / ↑k)

Tactic:
mul_comm y0,

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x✝ : { p // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : x ^ 2 + y ^ 2 = 1
⊢ (fun x ↦ ⟨(2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2)), ⋯⟩) ((fun p ↦ (↑p).1 / ((↑p).2 + 1)) ⟨(x, y), ⋯⟩) =
    ⟨(x, y), ⋯⟩

Tactic:
have h2 : y + 1 ≠ 0 := mt eq_neg_of_add_eq_zero_left hy

Goal state after:
K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x✝ : { p // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : x ^ 2 + y ^ 2 = 1
h2 : y + 1 ≠ 0
⊢ (fun x ↦ ⟨(2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2)), ⋯⟩) ((fun p ↦ (↑p).1 / ((↑p).2 + 1)) ⟨(x, y), ⋯⟩) =
    ⟨(x, y), ⋯⟩
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a.degree ≠ ⊥
hb : b ≠ 0
⊢ a.degree + (derivative b).degree < a.degree + b.degree

Tactic:
WithBot.add_lt_add_iff_left ha

Goal state after:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a.degree ≠ ⊥
hb : b ≠ 0
⊢ (derivative b).degree < b.degree
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: case hcp
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x✝ y✝ : k[X]
a✝² : IsRelPrime x✝ y✝
a✝¹ : divRadical x✝ ∣ derivative x✝
a✝ : divRadical y✝ ∣ derivative y✝
⊢ divRadical (x✝ * y✝) ∣ derivative (x✝ * y✝)

Tactic:
case hcp x y hpxy hx hy =>
    have hc : IsCoprime x y :=
      EuclideanDomain.isCoprime_of_dvd
        (fun ⟨hx, hy⟩ => not_isUnit_zero (hpxy (zero_dvd_iff.mpr hx) (zero_dvd_iff.mpr hy)))
        fun p hp _ hpx hpy => hp (hpxy hpx hpy)
    rw [divRadical_mul hc, derivative_mul]
    exact dvd_add (mul_dvd_mul hx (divRadical_dvd_self y)) (mul_dvd_mul (divRadical_dvd_self x) hy)

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

Goal state before:
pp: hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
⊢ FermatLastTheorem

Tactic:
by
  intro n h
  obtain hdvd | ⟨p, hpprime, hdvd, hpodd⟩ := Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt h
    <;> apply FermatLastTheoremWith.mono hdvd
  · exact fermatLastTheoremFour
  · exact hprimes p hpprime hpodd

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

Goal state before:
pp: case inr.refine_1
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
x✝ : ∃ n, a ∣ b ^ n
n : ℕ
hdvd : a ∣ b ^ n
⊢ radical a ∣ b

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)
    · simp [radical_of_isUnit <| isUnit_of_dvd_one <| pow_zero b ▸ hdvd]
    grw [radical_dvd_radical hdvd <| pow_ne_zero _ hb, radical_pow b hn, radical_dvd_self]

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

Goal state before:
pp: case inr.refine_1
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
x✝ : ∃ n, a ∣ b ^ n
n : ℕ
hdvd : a ∣ b ^ n
⊢ radical a ∣ b

pp: case inr.refine_2
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
h : radical a ∣ b
⊢ a ∣ b ^ (normalizedFactors a).card

Tactic:
· rcases eq_or_ne n 0 with (rfl | hn)
    · simp [radical_of_isUnit <| isUnit_of_dvd_one <| pow_zero b ▸ hdvd]
    grw [radical_dvd_radical hdvd <| pow_ne_zero _ hb, radical_pow b hn, radical_dvd_self]

Goal state after:
case inr.refine_2
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
h : radical a ∣ b
⊢ a ∣ b ^ (normalizedFactors a).card
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: case neg.refine_1
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
rw [mul_rotate] at abc_dr_dvd_w ⊢
      apply abc_subcall wbc <;> assumption

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

Goal state before:
pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ ↑ℤ⁰
h : x * (algebraMap (𝓞 K) K) ((algebraMap ℤ (𝓞 K)) d) = (algebraMap (𝓞 K) K) a
⊢ ⟨d * ↑(Ideal.absNorm (↑I).num), ⋯⟩ • x = (↑↑I).subtype ⟨↑(Ideal.absNorm (↑I).num) * (algebraMap (𝓞 K) K) a, ⋯⟩

Tactic:
Submodule.coe_subtype

Goal state after:
case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ ↑ℤ⁰
h : x * (algebraMap (𝓞 K) K) ((algebraMap ℤ (𝓞 K)) d) = (algebraMap (𝓞 K) K) a
⊢ ⟨d * ↑(Ideal.absNorm (↑I).num), ⋯⟩ • x = ↑(Ideal.absNorm (↑I).num) * (algebraMap (𝓞 K) K) a
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 ℤ) r)| / |↑((Algebra.norm ℤ) ↑d)| = |(Algebra.norm ℚ) x|

Tactic:
show ((Algebra.norm ℤ _) : ℚ) = algebraMap ℤ ℚ
      (Algebra.norm ℤ _) by rfl,

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
⊢ |(algebraMap ℤ ℚ) ((Algebra.norm ℤ) r)| / |(algebraMap ℤ ℚ) ((Algebra.norm ℤ) ↑d)| = |(Algebra.norm ℚ) x|
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:
intro ψ 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.TotallyRealComplex

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
K : Type u_2
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst✝ : ∀ (i : ι), IsTotallyReal ↥(k i)
⊢ IsTotallyReal ↥(⨆ i, k i)

Tactic:
obtain hι | ⟨⟨i⟩⟩ := isEmpty_or_nonempty ι
  · rw [iSup_of_empty]
    infer_instance
  · rw [isTotallyReal_iff_le_maximalRealSubfield, iSup_le_iff]
    exact fun i ↦ IsTotallyReal.le_maximalRealSubfield (k i)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i✝ : Free.ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) :=
  LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (canonicalEmbedding K).toRatAlgHom.toLinearMap
    ⋯
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ (↑(Basis.restrictScalars ℚ (latticeBasis K)).repr ∘ₗ f) ((integralBasis K) i) =
    ↑(integralBasis K).repr ((integralBasis K) i)

Tactic:
have : f (integralBasis K i) = ((latticeBasis K).restrictScalars ℚ) i := by
    apply Subtype.val_injective
    rw [LinearMap.codRestrict_apply, AlgHom.toLinearMap_apply, Basis.restrictScalars_apply,
      latticeBasis_apply]
    rfl

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i✝ : Free.ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) :=
  LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (canonicalEmbedding K).toRatAlgHom.toLinearMap
    ⋯
i : Free.ChooseBasisIndex ℤ (𝓞 K)
this : f ((integralBasis K) i) = (Basis.restrictScalars ℚ (latticeBasis K)) i
⊢ (↑(Basis.restrictScalars ℚ (latticeBasis K)).repr ∘ₗ f) ((integralBasis K) i) =
    ↑(integralBasis K).repr ((integralBasis K) i)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ volume (convexBodyLT' K f w₀) = ↑(convexBodyLT'Factor K) * ↑(∏ w, f w ^ w.mult)

Tactic:
calc
    _ = (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (2 * (f x.val))) *
          ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal (f x.val) ^ 2 * pi) *
          (4 * (f w₀) ^ 2)) := by
      simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball]
      rw [← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]
      congr 2
      · refine Finset.prod_congr rfl (fun w' hw' ↦ ?_)
        rw [if_neg (Finset.ne_of_mem_erase hw'), Complex.volume_ball]
      · simpa only [ite_true] using vol_box (f w₀)
    _ = ((2 : ℝ≥0) ^ nrRealPlaces K *
          (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val))) *
            ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal (f x.val) ^ 2) *
              ↑pi ^ (nrComplexPlaces K - 1) * (4 * (f w₀) ^ 2)) := by
      simp_rw [ofReal_mul (by simp : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
        Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ, ofReal_ofNat,
        ofReal_coe_nnreal, coe_ofNat]
    _ = convexBodyLT'Factor K * (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val))
        * (∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2) := by
      rw [show (4 : ℝ≥0∞) = (2 : ℝ≥0) ^ 2 by norm_num, convexBodyLT'Factor, pow_add,
        ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀), ofReal_coe_nnreal]
      simp_rw [coe_mul, ENNReal.coe_pow]
      ring
    _ = convexBodyLT'Factor 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, mul_assoc]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : ∫ (x : mixedSpace K), rexp (-convexBodySumFun x) = 2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K
⊢ ENNReal.ofReal (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K) / ↑(finrank ℚ K).factorial =
    ↑(convexBodySumFactor K)

Tactic:
convexBodySumFactor,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : ∫ (x : mixedSpace K), rexp (-convexBodySumFun x) = 2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K
⊢ ENNReal.ofReal (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K) / ↑(finrank ℚ K).factorial =
    ↑(2 ^ nrRealPlaces K * (NNReal.pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : ∫ (x : mixedSpace K), rexp (-convexBodySumFun x) = 2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K
⊢ 2 ^ nrRealPlaces K * (↑NNReal.pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial =
    ↑(2 ^ nrRealPlaces K * (NNReal.pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)

Tactic:
coe_div (Nat.cast_ne_zero.mpr
        (Nat.factorial_ne_zero _)),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : ∫ (x : mixedSpace K), rexp (-convexBodySumFun x) = 2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K
⊢ 2 ^ nrRealPlaces K * (↑NNReal.pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial =
    ↑(2 ^ nrRealPlaces K * (NNReal.pi / 2) ^ nrComplexPlaces K) / ↑↑(finrank ℚ K).factorial
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)
⊢ #(MulAction.orbit Gal(K/k) w).toFinset = Fintype.card ↑(MulAction.orbit Gal(K/k) w) * Fintype.card ↥(Stab w)

Tactic:
← Nat.card_eq_fintype_card (α := Stab w),

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)
⊢ #(MulAction.orbit Gal(K/k) w).toFinset = Fintype.card ↑(MulAction.orbit Gal(K/k) w) * Nat.card ↥(Stab w)
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)
⊢ #(MulAction.orbit Gal(K/k) w).toFinset = Fintype.card ↑(MulAction.orbit Gal(K/k) w) * Fintype.card ↥(Stab w) / 2

Tactic:
← Nat.card_eq_fintype_card (α := Stab w),

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)
⊢ #(MulAction.orbit Gal(K/k) w).toFinset = Fintype.card ↑(MulAction.orbit Gal(K/k) w) * Nat.card ↥(Stab w) / 2
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))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)| =
    B ^ finrank ℚ K / ↑(finrank ℚ K) ^ finrank ℚ K

Tactic:
← Real.rpow_natCast B,

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))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)| =
    B ^ ↑(finrank ℚ K) / ↑(finrank ℚ K) ^ finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ ∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(max B 1)

Tactic:
classical
  have : minkowskiBound K ↑1 < volume (convexBodyLT K (fun w ↦ if w = w₀ then B else 1)) := by
    rw [convexBodyLT_volume, ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]
    simp_rw [ite_pow, one_pow]
    rw [Finset.prod_ite_eq']
    simp_rw [Finset.notMem_erase, ite_false, mult, hw₀, ite_true, one_mul, pow_one]
    exact hB
  obtain ⟨a, h_nz, h_le⟩ := exists_ne_zero_mem_ringOfIntegers_lt K this
  refine ⟨a, ?_, fun w ↦ lt_of_lt_of_le (h_le w) ?_⟩
  · exact is_primitive_element_of_infinitePlace_lt h_nz
      (fun w h_ne ↦ by convert! (if_neg h_ne) ▸ h_le w) (Or.inl hw₀)
  · split_ifs <;> simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ DiscreteTopology ↥(mixedEmbedding.integerLattice K)

Tactic:
classical
  rw [← span_latticeBasis]
  infer_instance

Goal state after:
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))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ (volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) * 2 ^ finrank ℝ (mixedSpace K) *
        ↑(convexBodySumFactor K)⁻¹).toReal =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹

Tactic:
convexBodySumFactor,

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))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ (volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) * 2 ^ finrank ℝ (mixedSpace K) *
        ↑(2 ^ nrRealPlaces K * (pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹).toReal =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasureTheory.IsAddFundamentalDomain (↥(mixedEmbedding.integerLattice K)) (ZSpan.fundamentalDomain (latticeBasis K))
    MeasureTheory.volume

Tactic:
by
  rw [← span_latticeBasis]
  exact ZSpan.isAddFundamentalDomain (latticeBasis K) _

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i✝ : ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) :=
  LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (mixedEmbedding K).toRatAlgHom.toLinearMap ⋯
i : ChooseBasisIndex ℤ (𝓞 K)
⊢ (↑(Basis.restrictScalars ℚ (latticeBasis K)).repr ∘ₗ f) ((integralBasis K) i) =
    ↑(integralBasis K).repr ((integralBasis K) i)

Tactic:
have : f (integralBasis K i) = ((latticeBasis K).restrictScalars ℚ) i := by
    apply Subtype.val_injective
    rw [LinearMap.codRestrict_apply, AlgHom.toLinearMap_apply, Basis.restrictScalars_apply,
      latticeBasis_apply]
    rfl

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i✝ : ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) :=
  LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (mixedEmbedding K).toRatAlgHom.toLinearMap ⋯
i : ChooseBasisIndex ℤ (𝓞 K)
this : f ((integralBasis K) i) = (Basis.restrictScalars ℚ (latticeBasis K)) i
⊢ (↑(Basis.restrictScalars ℚ (latticeBasis K)).repr ∘ₗ f) ((integralBasis K) i) =
    ↑(integralBasis K).repr ((integralBasis K) i)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: 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
⊢ ∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < √(1 + ↑B ^ 2)

Tactic:
classical
  have : minkowskiBound K ↑1 <
      volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩) := by
    rw [convexBodyLT'_volume, ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]
    simp_rw [ite_pow, one_pow]
    rw [Finset.prod_ite_eq']
    simp_rw [Finset.notMem_erase, ite_false, mult, not_isReal_iff_isComplex.mpr hw₀,
      ite_true, ite_false, one_mul, NNReal.sq_sqrt]
    exact hB
  obtain ⟨a, h_nz, h_le, h_le₀⟩ := exists_ne_zero_mem_ringOfIntegers_lt' K ⟨w₀, hw₀⟩ this
  refine ⟨a, ?_, fun w ↦ ?_⟩
  · exact is_primitive_element_of_infinitePlace_lt h_nz
      (fun w h_ne ↦ by convert! if_neg h_ne ▸ h_le w h_ne) (Or.inr h_le₀.1)
  · by_cases h_eq : w = w₀
    · rw [if_pos rfl] at h_le₀
      dsimp only at h_le₀
      rw [h_eq, ← norm_embedding_eq, Real.lt_sqrt (norm_nonneg _), ← Complex.re_add_im
        (embedding w₀ _), Complex.norm_add_mul_I, Real.sq_sqrt (by positivity)]
      refine add_lt_add ?_ ?_
      · rw [← sq_abs, sq_lt_one_iff₀ (abs_nonneg _)]
        exact h_le₀.1
      · rw [sq_lt_sq, NNReal.abs_eq, ← NNReal.sq_sqrt B]
        exact h_le₀.2
    · refine lt_of_lt_of_le (if_neg h_eq ▸ h_le w h_eq) ?_
      rw [NNReal.coe_one, Real.le_sqrt' zero_lt_one, one_pow]
      norm_num

Goal state after: