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

Goal state before:
pp: case pos
a : ℝ
ha : 0 ≤ a
h : a = 0
⊢ ∃ p, 0 < p ∧ (fun t ↦ F_nat 0 0 t - 1) =O[atTop] fun t ↦ rexp (-p * t)

Tactic:
have : (fun t ↦ F_nat 0 0 t - 1) =O[atTop] fun t ↦ rexp (-π * t) / (1 - rexp (-π * t)) := by
      apply Eventually.isBigO
      filter_upwards [eventually_gt_atTop 0] with t ht
      exact F_nat_zero_zero_sub_le ht

Goal state after:
case pos
a : ℝ
ha : 0 ≤ a
h : a = 0
this : (fun t ↦ F_nat 0 0 t - 1) =O[atTop] fun t ↦ rexp (-π * t) / (1 - rexp (-π * t))
⊢ ∃ p, 0 < p ∧ (fun t ↦ F_nat 0 0 t - 1) =O[atTop] fun t ↦ rexp (-p * t)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: 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
x : ℝ
x✝ : x ∈ Ioc 0 1
hx : 0 < x
right✝ : x ≤ 1
⊢ ↑x ^ (s - 1) • P.f₀ - (P.ε * (↑x ^ (-↑P.k) * ↑x ^ (s - 1))) • P.g₀ =
    ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀

Tactic:
mul_smul,

Goal state after:
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
x : ℝ
x✝ : x ∈ Ioc 0 1
hx : 0 < x
right✝ : x ≤ 1
⊢ ↑x ^ (s - 1) • P.f₀ - P.ε • (↑x ^ (-↑P.k) * ↑x ^ (s - 1)) • P.g₀ =
    ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_1
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := ⋯
hVo : IsOpen V
u : ℤ → ℝ := ⋯
hu : Summable u
n : ℤ
⊢ Continuous fun p ↦ jacobiTheta₂'_term n p.1 p.2

Tactic:
unfold jacobiTheta₂'_term jacobiTheta₂_term

Goal state after:
case refine_1
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n ↦ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : Summable u
n : ℤ
⊢ Continuous fun p ↦ 2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * p.1 + ↑π * I * ↑n ^ 2 * p.2)
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
⊢ Tendsto (fun s ↦ s • P.Λ₀ s) (𝓝 0) (𝓝 (0 • P.Λ₀ 0))

Tactic:
exact (continuous_id.smul P.differentiable_Λ₀.continuous).tendsto _

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

Goal state before:
pp: z τ : ℂ
⊢ (starRingEnd ℂ) (jacobiTheta₂ z τ) = jacobiTheta₂ ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
rw [← jacobiTheta₂_neg_left, jacobiTheta₂, conj_tsum]

Goal state after:
z τ : ℂ
⊢ ∑' (a : ℤ), (starRingEnd ℂ) (jacobiTheta₂_term a (-z) τ) = jacobiTheta₂ ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

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

Tactic:
(by rw [cpow_one, ← div_div, div_self (neg_ne_zero.mpr I_ne_zero)] :
      1 / τ = -I / (-I * τ) ^ (1 : ℂ)),

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

Goal state before:
pp: case H.refine_2
a x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x ↦ jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
    x

Tactic:
· have hf : Continuous fun u : ℝ ↦ (a * I * u, I * u) := by fun_prop
    apply ContinuousAt.add
    · exact ((continuousAt_jacobiTheta₂' (a * I * x) (by rwa [I_mul_im, ofReal_re])).comp
        (f := fun u : ℝ ↦ (a * I * u, I * u)) hf.continuousAt).div_const _
    · exact continuousAt_const.mul <| (continuousAt_jacobiTheta₂ (a * I * x)
        (by rwa [I_mul_im, ofReal_re])).comp (f := fun u : ℝ ↦ (a * I * u, I * u)) hf.continuousAt

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

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

Tactic:
ofReal_intCast,

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

Goal state before:
pp: case refine_2
s : ℂ
n : ℕ
x✝ : n ≠ 0
⊢ ‖↑(μ n)‖ ≤ 1

Tactic:
· norm_cast
    exact abs_moebius_le_one

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
t : ℝ
ht : 0 < t
n : ℤ
⊢ (if n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) =
    (if n = 0 then 0 else cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) / 2

Tactic:
split_ifs <;> simp [c, div_mul_eq_mul_div]

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

Goal state before:
pp: a : UnitAddCircle
⊢ Tendsto (fun s ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) (𝓝 1) (𝓝 (hurwitzZetaEven a 1))

Tactic:
simpa using (differentiableAt_hurwitzZetaEven_sub_one_div a).continuousAt.tendsto

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ Summable fun n ↦ ‖(riemannZetaSummandHom ⋯) n‖

Tactic:
simp only [riemannZetaSummandHom, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
  convert! Real.summable_nat_rpow_inv.mpr hs with n
  rw [← ofReal_natCast,
    norm_cpow_eq_rpow_re_of_nonneg (Nat.cast_nonneg n) <| re_neg_ne_zero_of_one_lt_re hs,
    neg_re, Real.rpow_neg <| Nat.cast_nonneg n]

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

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ c1.natAbs < (↑p ^ 2).natAbs * c1.natAbs

Tactic:
lt_mul_iff_one_lt_left,

Goal state after:
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 1 < (↑p ^ 2).natAbs

p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 0 < c1.natAbs
Module: Mathlib.NumberTheory.FLT.Four

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

Tactic:
have hs : b' ^ 2 = m * (r * s) := by
    apply (mul_right_inj' (by simp : (4 : ℤ) ≠ 0)).mp
    linear_combination (-b - 2 * b') * hb2' + ht2 + 2 * m * htt2

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

Goal state before:
pp: case e'_2
s : ℝ
hs : 1 < s
p : ℕ
⊢ ↑(Λ p) / Complex.log ↑p / ↑p ^ ↑s = ↑(Λ p) / (↑(↑p ^ s) * Complex.log ↑p)

Tactic:
rw [ofReal_cpow (by positivity)]

Goal state after:
case e'_2
s : ℝ
hs : 1 < s
p : ℕ
⊢ ↑(Λ p) / Complex.log ↑p / ↑p ^ ↑s = ↑(Λ p) / (↑↑p ^ ↑s * Complex.log ↑p)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inl.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 ∣ ↑(m.gcd n)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hpm : p ∣ m.natAbs
⊢ False

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

Goal state after:
case inl.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 ∣ ↑(m.gcd n)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hpm : p ∣ m.natAbs
⊢ ↑p ∣ n
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:
← div_left_inj' (mt Rat.intCast_inj.mp hz),

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
⊢ ↑x / ↑z = ↑(2 * m * n) / ↑z
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
⊢ w = (1 - q ^ 2) / (1 + q ^ 2)

Tactic:
apply ht4.2

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
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀
⊢ ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den| = ↑(Ideal.absNorm I₀) / ↑|(Algebra.norm ℤ) ↑a|

Tactic:
div_eq_div_iff

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
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀
⊢ ↑(Ideal.absNorm I.num) * ↑|(Algebra.norm ℤ) ↑a| = ↑(Ideal.absNorm I₀) * ↑|(Algebra.norm ℤ) ↑I.den|

case hb
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
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀
⊢ ↑|(Algebra.norm ℤ) ↑I.den| ≠ 0

case hd
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
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀
⊢ ↑|(Algebra.norm ℤ) ↑a| ≠ 0
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
⊢ 1 • ↑1 = Submodule.map (Algebra.linearMap R K) ⊤

Tactic:
by simp [Submodule.one_eq_range]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : NumberField K
f : InfinitePlace K → α
⊢ ∏ w, f w = (∏ w, f ↑w) * ∏ w, f ↑w

Tactic:
← Equiv.prod_comp (Equiv.subtypeEquivRight (fun _ ↦ not_isReal_iff_isComplex))

Goal state after:
K : Type u_1
inst✝² : Field K
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : NumberField K
f : InfinitePlace K → α
⊢ ∏ w, f w = (∏ w, f ↑w) * ∏ i, f ↑((Equiv.subtypeEquivRight ⋯) i)
Module: Mathlib.NumberTheory.NumberField.Units.Basic

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

Tactic:
· let e := ((torsion K).equivMapOfInjective (Units.complexEmbedding φ)
      (Units.complexEmbedding_injective φ)).symm.toEquiv
    rw [Complex.card_rootsOfUnity, Nat.card_congr e, torsionOrder]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ ↑(2 ^ nrRealPlaces K) * ↑(pi ^ nrComplexPlaces K) *
      ((∏ x, ENNReal.ofReal ↑(f ↑x)) * ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2) =
    ↑(2 ^ nrRealPlaces K) * ↑(pi ^ nrComplexPlaces K) * ((∏ x, ↑(f ↑x)) * ∏ x, ↑(f ↑x ^ 2))

Tactic:
ENNReal.coe_pow,

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ ↑2 ^ nrRealPlaces K * ↑pi ^ nrComplexPlaces K * ((∏ x, ENNReal.ofReal ↑(f ↑x)) * ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2) =
    ↑2 ^ nrRealPlaces K * ↑pi ^ nrComplexPlaces K * ((∏ x, ↑(f ↑x)) * ∏ x, ↑(f ↑x) ^ 2)
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case refine_3
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
heq' : C v * b ^ q + C w * c ^ r + C u * a ^ p = 0
hca : IsCoprime c a
⊢ c.natDegree = 0

Tactic:
← add_rotate

Goal state after:
case refine_3
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : p * q + q * r + r * p ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C w * c ^ r + C u * a ^ p + C v * b ^ q = 0
hbc : IsCoprime b c
heq' : C v * b ^ q + C w * c ^ r + C u * a ^ p = 0
hca : IsCoprime c a
⊢ c.natDegree = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := B.toMatrix fun i ↦ (canonicalEmbedding K) ((integralBasis K) (e i))
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i ↦ (integralBasis K) (e i)) (RingHom.equivRatAlgHom K ℂ)
⊢ N.det ^ 2 ≠ 0

Tactic:
convert!
      (map_ne_zero_iff _ (algebraMap ℚ ℂ).injective).mpr
        (Algebra.discr_not_zero_of_basis ℚ (integralBasis K))

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := B.toMatrix fun i ↦ (canonicalEmbedding K) ((integralBasis K) (e i))
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i ↦ (integralBasis K) (e i)) (RingHom.equivRatAlgHom K ℂ)
⊢ N.det ^ 2 = (algebraMap ℚ ℂ) (Algebra.discr ℚ ⇑(integralBasis K))
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)
⊢ (canonicalEmbedding K).toRatAlgHom ((integralBasis K) i) = (latticeBasis K) i

Tactic:
latticeBasis_apply

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)
⊢ (canonicalEmbedding K).toRatAlgHom ((integralBasis K) i) = (canonicalEmbedding K) ((integralBasis K) i)
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 w' : InfinitePlace K
h :
  w.embedding.comp (algebraMap k K) = w'.embedding.comp (algebraMap k K) ∨
    conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)
⊢ ∃ σ, σ • w = w'

Tactic:
cases h with
  | inl h =>
    obtain ⟨σ, hσ⟩ := ComplexEmbedding.exists_comp_symm_eq_of_comp_eq w.embedding w'.embedding h
    use σ
    rw [← mk_embedding w, ← mk_embedding w', smul_mk, hσ]
  | inr h =>
    obtain ⟨σ, hσ⟩ := ComplexEmbedding.exists_comp_symm_eq_of_comp_eq
      ((starRingEnd ℂ).comp (embedding w)) w'.embedding h
    use σ
    rw [← mk_embedding w, ← mk_embedding w', smul_mk, mk_eq_iff]
    exact Or.inr hσ

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Injective ⇑(mixedEmbedding K)

Tactic:
exact RingHom.injective _

Goal state after:
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
⊢ (↑(2 ^ (nrRealPlaces K + 2)) * ↑(pi ^ (nrComplexPlaces K - 1)) * ∏ x, ENNReal.ofReal ↑(f ↑x)) *
      ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2 =
    ↑(2 ^ (nrRealPlaces K + 2)) * ↑(pi ^ (nrComplexPlaces K - 1)) * ((∏ x, ↑(f ↑x)) * ∏ x, ↑(f ↑x ^ 2))

Tactic:
ENNReal.coe_pow,

Goal state after:
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
⊢ (↑2 ^ (nrRealPlaces K + 2) * ↑pi ^ (nrComplexPlaces K - 1) * ∏ x, ENNReal.ofReal ↑(f ↑x)) *
      ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2 =
    ↑2 ^ (nrRealPlaces K + 2) * ↑pi ^ (nrComplexPlaces K - 1) * ((∏ x, ↑(f ↑x)) * ∏ x, ↑(f ↑x) ^ 2)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
hw : w.IsComplex
x : mixedSpace K
⊢ (normAtPlace w) x = ‖x.2 ⟨w, hw⟩‖

Tactic:
rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk,
    dif_neg (not_isReal_iff_isComplex.mpr hw)]

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

Goal state before:
pp: k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
v : InfinitePlace K
σ : Gal(K/k)
H : IsUnramified k (σ • v)
hv : v.comap (algebraMap k K) = (σ • v).comap (algebraMap k K)
⊢ IsUnramified k v

Tactic:
rwa [isUnramified_smul_iff] at H

Goal state after:
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)ᵀ
this : ‖I‖₊ = 1
⊢ ↑(‖2‖₊⁻¹ ^ nrComplexPlaces K) * ↑‖N.det‖₊ = 2⁻¹ ^ Fintype.card { w // w.IsComplex } * ↑(sqrt ‖N.det ^ 2‖₊)

Tactic:
ENNReal.coe_pow,

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)ᵀ
this : ‖I‖₊ = 1
⊢ ↑‖2‖₊⁻¹ ^ nrComplexPlaces K * ↑‖N.det‖₊ = 2⁻¹ ^ Fintype.card { w // w.IsComplex } * ↑(sqrt ‖N.det ^ 2‖₊)
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)ˣ
h : minkowskiBound K I < volume (convexBodyLT K f)
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
hx : x ∈ span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))
h_nz : ⟨x, hx✝⟩ ≠ 0
h_mem : ↑⟨x, hx✝⟩ ∈ convexBodyLT K f
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w a < ↑(f w)

Tactic:
mem_span_fractionalIdealLatticeBasis

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
h : minkowskiBound K I < volume (convexBodyLT K f)
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
hx : x ∈ ⇑(mixedEmbedding K) '' ↑↑I
h_nz : ⟨x, hx✝⟩ ≠ 0
h_mem : ↑⟨x, hx✝⟩ ∈ convexBodyLT K f
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w a < ↑(f w)