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

Goal state before:
pp: case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ Integrable (fun x ↦ ↑x ^ (s - 1) • P.f₀) (volume.restrict (Ioc 0 1))

Tactic:
apply Integrable.smul_const

Goal state after:
case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ Integrable (fun x ↦ ↑x ^ (s - 1)) (volume.restrict (Ioc 0 1))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (1 / s) • P.f₀) s

pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (P.ε / (↑P.k - s)) • P.g₀) s

Tactic:
· rcases hs with hs | hs
    · fun_prop
    · simp [hs]

Goal state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (P.ε / (↑P.k - s)) • P.g₀) s
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ s • (1 / s) • P.f₀) (𝓝[≠] 0) (𝓝 P.f₀)

pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ s • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] 0) (𝓝 0)

Tactic:
· refine (tendsto_const_nhds.mono_left nhdsWithin_le_nhds).congr' ?_
    filter_upwards [self_mem_nhdsWithin] with s (hs : s ≠ 0)
    match_scalars
    grind

Goal state after:
case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ s • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] 0) (𝓝 0)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ I *
      (cexp (-(↑π * I * z ^ 2) / τ) *
        -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)))) =
    I *
      (cexp (-(↑π * I * z ^ 2) / τ) *
        (-jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * ↑π * I)))

Tactic:
neg_div

Goal state after:
case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ I *
      (cexp (-(↑π * I * z ^ 2 / τ)) *
        -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)))) =
    I *
      (cexp (-(↑π * I * z ^ 2 / τ)) *
        (-jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * ↑π * I)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case hf
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / s
⊢ DifferentiableAt ℂ (completedHurwitzZetaEven₀ a) 1

Tactic:
apply differentiable_completedHurwitzZetaEven₀

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

Goal state before:
pp: case hg
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / s
⊢ DifferentiableAt ℂ (completedHurwitzZetaEven₀ b) 1

Tactic:
apply differentiable_completedHurwitzZetaEven₀

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

Goal state before:
pp: N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
⊢ ¬LSeriesSummable (fun n ↦ χ ↑n) 1

Tactic:
refine fun h ↦ (Real.not_summable_indicator_one_div_natCast hN 1) ?_

Goal state after:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
⊢ Summable ({n | ↑n = 1}.indicator fun n ↦ 1 / ↑n)
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ 1 < (↑x).re

Tactic:
simpa using hx

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

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

Tactic:
suffices deriv (L 1) s = deriv riemannZeta s by
    rw [LSeries_vonMangoldt_eq hs, ← LSeries_one_eq_riemannZeta hs, this]
  refine Filter.EventuallyEq.deriv_eq <| Filter.eventuallyEq_iff_exists_mem.mpr ?_
  exact ⟨{z | 1 < z.re}, (isOpen_lt continuous_const continuous_re).mem_nhds hs,
    fun _ ↦ LSeries_one_eq_riemannZeta⟩

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ -completedHurwitzZetaOdd a s / (s + 1).Gammaℝ = -(completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)

Tactic:
neg_div

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ -completedSinZeta a s / (s + 1).Gammaℝ = -(completedSinZeta a s / (s + 1).Gammaℝ)

Tactic:
neg_div

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

Goal state before:
pp: a b c : ℤ
h : Fermat42 a b c
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0

Tactic:
let S : Set ℕ := { n | ∃ s : ℤ × ℤ × ℤ, Fermat42 s.1 s.2.1 s.2.2 ∧ n = Int.natAbs s.2.2 }
  have S_nonempty : S.Nonempty := by
    use Int.natAbs c
    rw [Set.mem_ofPred_eq]
    use ⟨a, ⟨b, c⟩⟩
  let m : ℕ := Nat.find S_nonempty
  have m_mem : m ∈ S := Nat.find_spec S_nonempty
  rcases m_mem with ⟨s0, hs0, hs1⟩
  use s0.1, s0.2.1, s0.2.2, hs0
  intro a1 b1 c1 h1
  rw [← hs1]
  apply Nat.find_min'
  use ⟨a1, ⟨b1, c1⟩⟩

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2 =
    ↑(SignType.sign (↑↑n + a)) / ↑|↑↑n + a| ^ s / 2 + ↑(SignType.sign (-(↑↑n + 1) + a)) / ↑|-(↑↑n + 1) + a| ^ s / 2

Tactic:
sub_eq_add_neg,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -(↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2) =
    ↑(SignType.sign (↑↑n + a)) / ↑|↑↑n + a| ^ s / 2 + ↑(SignType.sign (-(↑↑n + 1) + a)) / ↑|-(↑↑n + 1) + a| ^ s / 2
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
this : -(↑n + 1) + a = -(↑n + 1 - a)
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -(↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2) =
    ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -(↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2

Tactic:
neg_div

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
this : -(↑n + 1) + a = -(↑n + 1 - a)
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -(↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2) =
    ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -(↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (sinZeta (↑a) s)

Tactic:
by
  rw [sinZeta]
  refine ((hasSum_int_completedSinZeta a hs).div_const (Gammaℝ (s + 1))).congr_fun fun n ↦ ?_
  have : 0 < re (s + 1) := by rw [add_re, one_re]; positivity
  simp only [mul_assoc, div_right_comm _ _ (Gammaℝ _),
    mul_div_cancel_left₀ _ (Gammaℝ_ne_zero_of_re_pos this)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
⊢ (a.wronskian b).natDegree < a.natDegree + b.natDegree

Tactic:
have ha : a ≠ 0 := by intro h; subst h; rw [wronskian_zero_left] at hw; exact hw rfl
  have hb : b ≠ 0 := by intro h; subst h; rw [wronskian_zero_right] at hw; exact hw rfl
  rw [← WithBot.coe_lt_coe, WithBot.coe_add]
  convert! ← degree_wronskian_lt_add ha hb
  · exact Polynomial.degree_eq_natDegree hw
  · exact Polynomial.degree_eq_natDegree ha
  · exact Polynomial.degree_eq_natDegree hb

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inr
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 ∣ ↑(n.gcd m)
hpn : p ∣ n.natAbs
⊢ False

Tactic:
apply mt (Int.dvd_coe_gcd (Int.natCast_dvd.mpr hpn)) hnp

Goal state after:
case inr
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 ∣ ↑(n.gcd m)
hpn : p ∣ n.natAbs
⊢ ↑p ∣ m
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a : k[X]
⊢ divRadical a ∣ derivative a

Tactic:
induction a using induction_on_coprime
  · case h0 =>
    rw [derivative_zero]
    apply dvd_zero
  · case h1 a ha =>
    exact (divRadical_isUnit ha).dvd
  · case hpr p i hp =>
    cases i
    · rw [pow_zero, derivative_one]
      apply dvd_zero
    · case succ i =>
      rw [← mul_dvd_mul_iff_left radical_ne_zero, radical_mul_divRadical,
        radical_pow_of_prime hp i.succ_ne_zero, derivative_pow_succ, ← mul_assoc]
      apply dvd_mul_of_dvd_left
      rw [mul_comm, mul_assoc]
      apply dvd_mul_of_dvd_right
      rw [pow_succ, mul_dvd_mul_iff_left (pow_ne_zero i hp.ne_zero), dvd_normalize_iff]
  · -- If it holds for coprime pair a and b, then it also holds for a * b.
    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.RingTheory.Radical.Basic

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

Tactic:
rw [dvd_iff_normalizedFactors_le_normalizedFactors ha₀ hb₀] at h

Goal state after:
case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : normalizedFactors a ≤ normalizedFactors b
hb₀ : b ≠ 0
ha₀ : a ≠ 0
⊢ radical a ∣ radical b
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < m ^ 2 + n ^ 2
hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
h2 : y = m ^ 2 - n ^ 2 ∧ z = m ^ 2 + n ^ 2
⊢ x = 2 * m * n

Tactic:
rw [← Rat.intCast_inj, ← div_left_inj' (mt Rat.intCast_inj.mp hz), hv2, h2.right]

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < m ^ 2 + n ^ 2
hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
h2 : y = m ^ 2 - n ^ 2 ∧ z = m ^ 2 + n ^ 2
⊢ 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2) = ↑(2 * m * n) / ↑(m ^ 2 + n ^ 2)
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✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ ¬↑I.den = 0

Tactic:
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
⊢ ¬↑d = 0

Tactic:
exact nonZeroDivisors.coe_ne_zero _

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
⊢ #{φ | mk φ = w} = w.mult

Tactic:
conv_lhs =>
    congr; congr; ext
    rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]
  simp_rw [Finset.filter_or, Finset.filter_eq' _ (embedding w),
    Finset.filter_eq' _ (ComplexEmbedding.conjugate (embedding w)),
    Finset.mem_univ, ite_true, mult]
  split_ifs with hw
  · rw [ComplexEmbedding.isReal_iff.mp (isReal_iff.mp hw), Finset.union_idempotent,
      Finset.card_singleton]
  · refine Finset.card_pair ?_
    rwa [Ne, eq_comm, ← ComplexEmbedding.isReal_iff, ← isReal_iff]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (finrank ℚ K)
hc : nrRealPlaces K = 0
⊢ Even (finrank ℚ K)

Tactic:
rw [← card_add_two_mul_card_eq_rank, hc, zero_add]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (finrank ℚ K)
hc : nrRealPlaces K = 0
⊢ Even (2 * nrComplexPlaces K)
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
heq : 1 * a ^ n + 1 * b ^ n - 1 * c ^ n = 0
hn' : 0 < n
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0

Tactic:
sub_eq_add_neg,

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
heq : 1 * a ^ n + 1 * b ^ n + -(1 * c ^ n) = 0
hn' : 0 < n
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
h : maximalRealSubfield K = ⊤
⊢ IsTotallyReal K

Tactic:
have : Algebra.IsIntegral (⊤ : Subfield K) K := Algebra.IsIntegral.tower_top ℚ

Goal state after:
K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
h : maximalRealSubfield K = ⊤
this : Algebra.IsIntegral (↥⊤) K
⊢ IsTotallyReal K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬‖(canonicalEmbedding K) x‖ ≤ r

pp: case inl.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
· exact (hr.trans_le (norm_nonneg _)).not_ge

Goal state after:
case inl.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case pos
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h₁ : ¬(w.comap f).IsReal
h₂ : w.IsReal
⊢ 2 ≤ 1

pp: case pos
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h₁ : (w.comap f).IsReal
h₂ : w.IsReal
⊢ 1 ≤ 1

pp: case neg
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h₁ : (w.comap f).IsReal
h₂ : ¬w.IsReal
⊢ 1 ≤ 2

pp: case neg
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h₁ : ¬(w.comap f).IsReal
h₂ : ¬w.IsReal
⊢ 2 ≤ 2

Tactic:
· exact (h₁ (h₂.comap _)).elim

Goal state after:
case pos
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h₁ : (w.comap f).IsReal
h₂ : w.IsReal
⊢ 1 ≤ 1

case neg
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h₁ : (w.comap f).IsReal
h₂ : ¬w.IsReal
⊢ 1 ≤ 2

case neg
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h₁ : ¬(w.comap f).IsReal
h₂ : ¬w.IsReal
⊢ 2 ≤ 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 ℂ)
this : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
⊢ volume (fundamentalDomain (latticeBasis K)) =
    ↑‖((mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)).det‖₊

Tactic:
← fundamentalDomain_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)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
this : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
⊢ volume (fundamentalDomain ((latticeBasis K).reindex e.symm)) =
    ↑‖((mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)).det‖₊
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_natCast

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.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume (fundamentalDomain (stdBasis K)) = 1

Tactic:
rw [fundamentalDomain_stdBasis, volume_eq_prod, prod_prod, volume_pi, volume_pi, pi_pi, pi_pi,
    Complex.volume_preserving_equiv_pi.measure_preimage ?_, volume_pi, pi_pi, Real.volume_Ico,
    sub_zero, ENNReal.ofReal_one, prod_const_one, prod_const_one, prod_const_one, one_mul]

Goal state after:
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✝ : IsGalois k K
w : InfinitePlace K
⊢ IsUnramifiedIn K (w.comap (algebraMap k K)) ↔ IsUnramified k w

Tactic:
refine ⟨fun H ↦ H _ rfl, fun H v hv ↦ ?_⟩

Goal state after:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace K
H : IsUnramified k w
v : InfinitePlace K
hv : v.comap (algebraMap k K) = w.comap (algebraMap k K)
⊢ IsUnramified k v
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]).det = ∏ _k, (2⁻¹ • !![1, 1; -I, I]).det

Tactic:
det_blockDiagonal

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∏ k, (2⁻¹ • !![1, 1; -I, I]).det = ∏ _k, (2⁻¹ • !![1, 1; -I, I]).det
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ finrank ℤ ↥↑↑I = finrank ℤ (𝓞 K)

Tactic:
fractionalIdeal_rank

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ finrank ℤ (𝓞 K) = finrank ℤ (𝓞 K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ finrank ℤ (𝓞 K) = finrank ℤ ↥↑↑I

Tactic:
fractionalIdeal_rank

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ finrank ℤ (𝓞 K) = finrank ℤ (𝓞 K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I := Fintype.equivOfCardEq ⋯
this : IsUnit ((latticeBasis K).det (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e))
⊢ Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)

Tactic:
rw [← Basis.is_basis_iff_det] at this
    exact Basis.mk this.1 (by rw [this.2])

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
⊢ ↑(FractionalIdeal.absNorm ↑I) * 2 ^ (-↑(nrComplexPlaces K)) * √‖discr K‖ * 2 ^ ↑(finrank ℚ K) *
      (↑(finrank ℚ K).factorial *
        (2 ^ (-↑(nrRealPlaces K)) * (π ^ (-↑(nrComplexPlaces K)) * 2 ^ ↑(nrComplexPlaces K)))) =
    ↑(FractionalIdeal.absNorm ↑I) *
            2 ^ (↑(finrank ℚ K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π ^ (-↑(nrComplexPlaces K))

Tactic:
sub_eq_add_neg,

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) * 2 ^ (-↑(nrComplexPlaces K)) * √‖discr K‖ * 2 ^ ↑(finrank ℚ K) *
      (↑(finrank ℚ K).factorial *
        (2 ^ (-↑(nrRealPlaces K)) * (π ^ (-↑(nrComplexPlaces K)) * 2 ^ ↑(nrComplexPlaces K)))) =
    ↑(FractionalIdeal.absNorm ↑I) *
            2 ^ (↑(finrank ℚ K) + -↑(nrComplexPlaces K) + -↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π ^ (-↑(nrComplexPlaces K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∉ s
⊢ ((negAt s) x).1 w = x.1 w

Tactic:
simp_rw [negAt, prodCongr_apply, piCongrRight_apply, if_neg hw,
    ContinuousLinearEquiv.refl_apply]

Goal state after: