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

Goal state before:
pp: case mpr.inr.inr
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : ↑(n ^ k) < ↑t
na : n ≤ xn hw1 j
te : ↑t = 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
this✝ : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]
this : n ^ k = m % t
⊢ n ^ k = m

Tactic:
Nat.mod_eq_of_lt mt

Goal state after:
case mpr.inr.inr
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : ↑(n ^ k) < ↑t
na : n ≤ xn hw1 j
te : ↑t = 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
this✝ : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]
this : n ^ k = m
⊢ n ^ k = m
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
⊢ ∏' (n : ℕ), f n = (∏' (p : Primes), f ↑p) * ∏' (p : Primes) (k : ℕ), f (↑p ^ (k + 2))

Tactic:
rw [tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers hfm hf]

Goal state after:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
⊢ ∏' (p : Primes) (k : ℕ), f (↑p ^ (k + 1)) = (∏' (p : Primes), f ↑p) * ∏' (p : Primes) (k : ℕ), f (↑p ^ (k + 2))
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
n : ℕ
hn : max 1 ⌈Real.exp 1⌉₊ ≤ n
⊢ ‖term f (↑s) n‖ ≤ ‖term (logMul f) (↑s) n‖

Tactic:
simp only [term_of_ne_zero (show n ≠ 0 by omega), logMul, norm_mul, mul_div_assoc,
      ← natCast_log, norm_real]

Goal state after:
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
n : ℕ
hn : max 1 ⌈Real.exp 1⌉₊ ≤ n
⊢ ‖f n / ↑n ^ ↑s‖ ≤ ‖Real.log ↑n‖ * ‖f n / ↑n ^ ↑s‖
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
step1 : mellin (fun t ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t ↦ ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t ↦ P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (↑P.k - s - 1) • P.f t = ↑t ^ (↑P.k - s - 1) • (fun t ↦ P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) t

Tactic:
simp_rw [P.h_feq' t ht, ← mul_smul]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
step1 : mellin (fun t ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t ↦ ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t ↦ P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (↑P.k - s - 1) • P.f t = (↑t ^ (↑P.k - s - 1) * (P.ε * (↑t ^ (-↑P.k) * (P.ε⁻¹ * ↑(t ^ P.k))))) • P.f t
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
this : 1 / x < 1
⊢ (((Ioi 1).indicator fun x ↦ P.f x - P.f₀) + (Ioo 0 1).indicator fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀)
      (1 / x) =
    (P.ε * ↑(x ^ P.k)) • P.g_modif x

Tactic:
Pi.add_apply,

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
this : 1 / x < 1
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) (1 / x) +
      (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) (1 / x) =
    (P.ε * ↑(x ^ P.k)) • P.g_modif x
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
this : 1 / x < 1
⊢ P.f (1 / x) - (P.ε * ↑((1 / x) ^ (-P.k))) • P.g₀ =
    (P.ε * ↑(x ^ P.k)) •
      (((Ioi 1).indicator fun x ↦ P.g x - P.g₀) + (Ioo 0 1).indicator fun x ↦ P.g x - (P.ε⁻¹ * ↑(x ^ (-P.k))) • P.f₀) x

Tactic:
Pi.add_apply,

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
this : 1 / x < 1
⊢ P.f (1 / x) - (P.ε * ↑((1 / x) ^ (-P.k))) • P.g₀ =
    (P.ε * ↑(x ^ P.k)) •
      ((Ioi 1).indicator (fun x ↦ P.g x - P.g₀) x +
        (Ioo 0 1).indicator (fun x ↦ P.g x - (P.ε⁻¹ * ↑(x ^ (-P.k))) • P.f₀) x)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / x
⊢ (((Ioi 1).indicator fun x ↦ P.f x - P.f₀) + (Ioo 0 1).indicator fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀)
      (1 / x) =
    (P.ε * ↑(x ^ P.k)) • P.g_modif x

Tactic:
Pi.add_apply,

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / x
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) (1 / x) +
      (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) (1 / x) =
    (P.ε * ↑(x ^ P.k)) • P.g_modif x
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / x
⊢ P.f (1 / x) - P.f₀ + 0 =
    (P.ε * ↑(x ^ P.k)) •
      (((Ioi 1).indicator fun x ↦ P.g x - P.g₀) + (Ioo 0 1).indicator fun x ↦ P.g x - (P.ε⁻¹ * ↑(x ^ (-P.k))) • P.f₀) x

Tactic:
Pi.add_apply,

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / x
⊢ P.f (1 / x) - P.f₀ + 0 =
    (P.ε * ↑(x ^ P.k)) •
      ((Ioi 1).indicator (fun x ↦ P.g x - P.g₀) x +
        (Ioo 0 1).indicator (fun x ↦ P.g x - (P.ε⁻¹ * ↑(x ^ (-P.k))) • P.f₀) x)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x : ℝ
⊢ evenKernel (-a) x = evenKernel a x

Tactic:
by
  induction a using QuotientAddGroup.induction_on with
  | H => simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, evenKernel_def, jacobiTheta₂_neg_left]

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : t < 1
⊢ ↑t ^ (s - 1) • (((Ioo 0 1).indicator fun x ↦ P.f x) + (Ioi 1).indicator fun x ↦ P.f x) t = ↑t ^ (s - 1) • P.f t

Tactic:
Pi.add_apply,

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : t < 1
⊢ ↑t ^ (s - 1) • ((Ioo 0 1).indicator (fun x ↦ P.f x) t + (Ioi 1).indicator (fun x ↦ P.f x) t) = ↑t ^ (s - 1) • P.f t
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : ¬t < 1
⊢ ↑t ^ (s - 1) • (((Ioi 1).indicator fun x ↦ P.f x) + (Ioo 0 1).indicator fun x ↦ P.f x) t = ↑t ^ (s - 1) • P.f t

Tactic:
Pi.add_apply,

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : ¬t < 1
⊢ ↑t ^ (s - 1) • ((Ioi 1).indicator (fun x ↦ P.f x) t + (Ioo 0 1).indicator (fun x ↦ P.f x) t) = ↑t ^ (s - 1) • P.f t
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s ↦ hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) 1

Tactic:
simp only [hurwitzZeta, add_sub_right_comm]
  exact (differentiableAt_hurwitzZetaEven_sub_one_div a).add (differentiable_hurwitzZetaOdd a 1)

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

Goal state before:
pp: case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
n : ℕ
hn : n ≠ 0
⊢ term (fun n ↦ χ ↑n) s n = f n

Tactic:
simp only [ne_eq, hn, not_false_eq_true, term_of_ne_zero, div_eq_mul_inv,
        dirichletSummandHom, cpow_neg, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, f]

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

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

Tactic:
by
  rw [← Gammaℂ]
  have : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (Gammaℝ (1 - s))⁻¹ := by
    rw [cosZeta, Function.update_of_ne, div_eq_mul_inv]
    simpa [sub_eq_zero] using (hs 0).symm
  rw [this, completedCosZeta_one_sub, inv_Gammaℝ_one_sub (fun n ↦ by simpa using hs (n + 1)),
    hurwitzZetaEven_def_of_ne_or_ne (Or.inr (by simpa using hs 1))]
  generalize Gammaℂ s * cos (π * s / 2) = A -- speeds up ring_nf call
  ring_nf

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (hurwitzZetaOdd (↑a) s)

Tactic:
by
  refine ((hasSum_int_completedHurwitzZetaOdd a hs).div_const (Gammaℝ _)).congr_fun fun n ↦ ?_
  have : 0 < re (s + 1) := by rw [add_re, one_re]; positivity
  simp [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 : R[X]
⊢ a.wronskian a = 0

Tactic:
rw [wronskian, mul_comm, sub_self]

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
⊢ abc_dr.natDegree < a.natDegree + b.natDegree

Tactic:
calc
      abc_dr.natDegree ≤ w.natDegree := Polynomial.natDegree_le_of_dvd abc_dr_dvd_w hw
      _ < a.natDegree + b.natDegree := by rw [wab] at hw ⊢; exact natDegree_wronskian_lt_add hw

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

Goal state before:
pp: hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
⊢ FermatLastTheoremFor n

Tactic:
obtain hdvd | ⟨p, hpprime, hdvd, hpodd⟩ := Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt h
    <;> apply FermatLastTheoremWith.mono hdvd

Goal state after:
case inl
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
hdvd : 4 ∣ n
⊢ FermatLastTheoremWith ℕ 4

case inr
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
p : ℕ
hpprime : Nat.Prime p
hdvd : p ∣ n
hpodd : Odd p
⊢ FermatLastTheoremWith ℕ p
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ p * a * (q * r) + q * b * (r * p) + r * c * (p * q) + 1 ≤
    (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q)

Tactic:
Nat.succ_le_iff

Goal state after:
p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ p * a * (q * r) + q * b * (r * p) + r * c * (p * q) <
    (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q)
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

Goal state before:
pp: case refine_2
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) ↑(a, ⟨(algebraMap ℤ (𝓞 K)) d, ⋯⟩).2 = (algebraMap (𝓞 K) K) (a, ⟨(algebraMap ℤ (𝓞 K)) d, ⋯⟩).1
⊢ d * ↑(Ideal.absNorm (↑I).num) ∈ ℤ⁰

Tactic:
refine Submonoid.mul_mem _ hd (mem_nonZeroDivisors_of_ne_zero ?_)
      rw [Nat.cast_ne_zero, ne_eq, Ideal.absNorm_eq_zero_iff]
      exact FractionalIdeal.num_eq_zero_iff.not.mpr <| Units.ne_zero I

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✝² : 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 ⋯))
⊢ |(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| =
    ↑(b.det (Subtype.val ∘ ⇑bI.num)).natAbs / ↑|(Algebra.norm ℤ) ↑I.den|

Tactic:
Nat.cast_natAbs,

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✝² : 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 ⋯))
⊢ |(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| =
    ↑|b.det (Subtype.val ∘ ⇑bI.num)| / ↑|(Algebra.norm ℤ) ↑I.den|
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).natAbs / ↑|(Algebra.norm ℤ) ↑d| = |(Algebra.norm ℚ) x|

Tactic:
Nat.cast_natAbs,

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
⊢ ↑|(Algebra.norm ℤ) r| / ↑|(Algebra.norm ℤ) ↑d| = |(Algebra.norm ℚ) x|
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ 0 < w.mult

Tactic:
rw [mult]
  split_ifs <;> norm_num

Goal state after:
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
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
h : 1 ≤ w ↑x
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |(w.embedding ↑x).re| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
⊢ (starRingEnd ℂ) (w.embedding ↑x) = w.embedding ↑x

Tactic:
have := RingHom.congr_fun h' x

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
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
h : 1 ≤ w ↑x
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |(w.embedding ↑x).re| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this : (ComplexEmbedding.conjugate w.embedding) ↑x = ψ.toRingHom ↑x
⊢ (starRingEnd ℂ) (w.embedding ↑x) = w.embedding ↑x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝³ x✝² : (K →+* ℂ) → ℂ
x✝¹ : x✝³ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝ : x✝² ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝³ φ) = x✝³ (ComplexEmbedding.conjugate φ)
hy : (starRingEnd ℂ) (x✝² φ) = x✝² (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((x✝³ + x✝²) φ) = (x✝³ + x✝²) (ComplexEmbedding.conjugate φ)

Tactic:
Pi.add_apply,

Goal state after:
case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝³ x✝² : (K →+* ℂ) → ℂ
x✝¹ : x✝³ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝ : x✝² ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝³ φ) = x✝³ (ComplexEmbedding.conjugate φ)
hy : (starRingEnd ℂ) (x✝² φ) = x✝² (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) (x✝³ φ + x✝² φ) = (x✝³ + x✝²) (ComplexEmbedding.conjugate φ)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝³ x✝² : (K →+* ℂ) → ℂ
x✝¹ : x✝³ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝ : x✝² ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝³ φ) = x✝³ (ComplexEmbedding.conjugate φ)
hy : (starRingEnd ℂ) (x✝² φ) = x✝² (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) (x✝³ φ + x✝² φ) = (x✝³ + x✝²) (ComplexEmbedding.conjugate φ)

Tactic:
Pi.add_apply,

Goal state after:
case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝³ x✝² : (K →+* ℂ) → ℂ
x✝¹ : x✝³ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝ : x✝² ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝³ φ) = x✝³ (ComplexEmbedding.conjugate φ)
hy : (starRingEnd ℂ) (x✝² φ) = x✝² (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) (x✝³ φ + x✝² φ) = x✝³ (ComplexEmbedding.conjugate φ) + x✝² (ComplexEmbedding.conjugate φ)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

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

pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : 0 ≤ r
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
· obtain ⟨φ⟩ := (inferInstance : Nonempty (K →+* ℂ))
    refine iff_of_false ?_ ?_
    · exact (hr.trans_le (norm_nonneg _)).not_ge
    · exact fun h => hr.not_ge (le_trans (norm_nonneg _) (h φ))

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

Goal state before:
pp: case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : w₁.embedding = conjugate w₂.embedding
⊢ mk w₁.embedding = w₂

Tactic:
h_eq,

Goal state after:
case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : w₁.embedding = conjugate w₂.embedding
⊢ mk (conjugate w₂.embedding) = w₂
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: 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

Tactic:
normAtPlace_apply

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
⊢ ↑((Algebra.norm ℚ) a) = 0 ↔ (mixedEmbedding K) a = 0

Tactic:
Rat.cast_eq_zero,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
⊢ (Algebra.norm ℚ) a = 0 ↔ (mixedEmbedding K) a = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ∫ (x : mixedSpace K), (∏ x_1, rexp (-‖x.1 x_1‖)) * ∏ x_1, rexp (-2 * ‖x.2 x_1‖) =
    ∫ (z : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)),
      (∏ w, rexp (-‖z.1 w‖)) * ∏ w, rexp (-2 * ‖z.2 w‖) ∂volume.prod volume

Tactic:
volume_eq_prod

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

Goal state before:
pp: case pos
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
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ : |(w₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ w ↑a < √(1 + ↑B ^ 2)

Tactic:
h_eq,

Goal state after:
case pos
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
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ : |(w₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ w₀ ↑a < √(1 + ↑B ^ 2)
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 ⋯
⊢ ¬↑(FractionalIdeal.absNorm ↑I) = 0

Tactic:
Rat.cast_eq_zero,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I := Fintype.equivOfCardEq ⋯
⊢ ¬FractionalIdeal.absNorm ↑I = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w // w.IsReal }), x.1 w ≠ 0
⊢ x ∈ ⇑(negAt s) '' plusPart A ↔ (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0

Tactic:
refine ⟨fun hx ↦ ⟨fun _ hw ↦ neg_of_mem_negA_plusPart A hx hw,
      fun _ hw ↦ pos_of_notMem_negAt_plusPart A hx hw⟩,
      fun ⟨h₁, h₂⟩ ↦
        ⟨(fun w ↦ ‖x.1 w‖, x.2), ⟨(hA x).mp hx₁, fun w ↦ norm_pos_iff.mpr (hx₂ w)⟩, ?_⟩⟩

Goal state after:
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w // w.IsReal }), x.1 w ≠ 0
x✝ : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
⊢ (negAt s) (fun w ↦ ‖x.1 w‖, x.2) = x