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

Goal state before:
pp: α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
⊢ v ∈ {v | f (v ∘ inl) ::ₒ v ∈ {v | v ∘ (some ∘ inl ⊗ none :: some ∘ inr) ∈ S}} ↔
    v ∈ {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}

Tactic:
dsimp

Goal state after:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
⊢ (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) ∈ S ↔ (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i ↦ fl i v) ∈ S}
v : α → ℕ
⊢ v ∈ {v | (v ⊗ f v :: fun i ↦ fl i v) ∈ S} ↔ v ∈ {v | (v ⊗ fun i ↦ (f :: fl) i v) ∈ S}

Tactic:
dsimp

Goal state after:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i ↦ fl i v) ∈ S}
v : α → ℕ
⊢ (v ⊗ f v :: fun i ↦ fl i v) ∈ S ↔ (v ⊗ fun i ↦ (f :: fl) i v) ∈ S
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
v : α → ℕ
⊢ v ∈ {v | f v < g v} ∪ {v | g v < f v} ↔ v ∈ {v | f v ≠ g v}

Tactic:
dsimp

Goal state after:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
v : α → ℕ
⊢ v ∈ {v | f v < g v} ∪ {v | g v < f v} ↔ ¬f v = g v
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedDivisionRing F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
p : ℕ
hp : 1 < p
⊢ Summable fun n ↦ f (p ^ n)

Tactic:
exact hsum.comp_injective <| Nat.pow_right_injective hp

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := max n k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
na : n ≤ a
x : ℕ := xn a1 k
y : ℕ := yn a1 k
z : ℕ
ze : yn w1 w = w * z
t : ℕ
te : ↑t = 2 * ↑a * ↑n - ↑n * ↑n - 1
nt : ↑(n ^ k) < ↑t
⊢ ↑t ∣ ↑(y * (a - n)) + ↑(n ^ k) - ↑x

Tactic:
Int.natCast_mul,

Goal state after:
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := max n k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
na : n ≤ a
x : ℕ := xn a1 k
y : ℕ := yn a1 k
z : ℕ
ze : yn w1 w = w * z
t : ℕ
te : ↑t = 2 * ↑a * ↑n - ↑n * ↑n - 1
nt : ↑(n ^ k) < ↑t
⊢ ↑t ∣ ↑y * ↑(a - n) + ↑(n ^ k) - ↑x
Module: Mathlib.NumberTheory.LSeries.Positivity

Goal state before:
pp: a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n : ℕ
⊢ 0 ≤ ∑' (n_1 : ℕ), term (logMul^[n] a) (↑x) n_1

Tactic:
refine tsum_nonneg fun k ↦ ?_

Goal state after:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
⊢ 0 ≤ term (logMul^[n] a) (↑x) k
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: f : ℕ → ℂ
m : ℕ
⊢ abscissaOfAbsConv (logMul^[m] f) = abscissaOfAbsConv f

Tactic:
induction m with
  | zero => simp
  | succ n ih => simp [ih, Function.iterate_succ', Function.comp_def,
      -Function.comp_apply, -Function.iterate_succ]

Goal state after:
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case refine_3
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑q.den
hq₁ : 0 < ↑q.den * (2 * ↑q.den - 1)
hq₂ : 0 < 2 * (↑q.den * ↑q.den)
⊢ |ξ - ↑q.num / ↑q.den| < (↑q.den * (2 * ↑q.den - 1))⁻¹

Tactic:
rw [(by norm_cast : (q.num / q.den : ℝ) = (q.num / q.den : ℚ)), Rat.num_div_den]

Goal state after:
case refine_3
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑q.den
hq₁ : 0 < ↑q.den * (2 * ↑q.den - 1)
hq₂ : 0 < 2 * (↑q.den * ↑q.den)
⊢ |ξ - ↑q| < (↑q.den * (2 * ↑q.den - 1))⁻¹
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 a t - 1) =O[atTop] fun t ↦ rexp (-p * t)

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

Tactic:
· rw [h]
    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
    refine ⟨_, pi_pos, this.trans ?_⟩
    simpa using! (isBigO_refl (fun t ↦ rexp (-π * t)) _).mul isBigO_one_aux

Goal state after:
case neg
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
⊢ ∃ p, 0 < p ∧ (fun t ↦ F_nat 0 a t - 0) =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
hP : IsStrongFEPair P
r : ℝ
⊢ P.f =O[atTop] fun x ↦ x ^ r

Tactic:
by
  simpa [hP.hf₀] using P.hf_top r

Goal state after:
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_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x

Tactic:
rw [f_modif, Pi.add_apply, indicator_of_mem (mem_Ioi.mpr this),
      indicator_of_notMem (notMem_Ioo_of_ge this.le), g_modif, Pi.add_apply,
      indicator_of_notMem (notMem_Ioi.mpr hx'.le),
      indicator_of_mem (mem_Ioo.mpr ⟨hx, hx'⟩), P.h_feq _ hx]

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.ε * ↑(x ^ P.k)) • P.g x - P.f₀ + 0 = (P.ε * ↑(x ^ P.k)) • (0 + (P.g x - (P.ε⁻¹ * ↑(x ^ (-P.k))) • P.f₀))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : 0 ≤ a
t : ℝ
n : ℕ
⊢ |↑n + a| ^ k * rexp (-π * (↑n + a) ^ 2 * t) = (↑n + a) ^ k * rexp (-π * (↑n + a) ^ 2 * t)

Tactic:
abs_of_nonneg (by positivity)

Goal state after:
k : ℕ
a : ℝ
ha : 0 ≤ a
t : ℝ
n : ℕ
⊢ (↑n + a) ^ k * rexp (-π * (↑n + a) ^ 2 * t) = (↑n + a) ^ k * rexp (-π * (↑n + a) ^ 2 * t)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
⊢ 1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / (-I * τ) * (↑n + I * (I * z)) ^ 2) =
    1 / (-I * τ) ^ (1 / 2) * cexp (↑π * I * (-1 / τ) * z ^ 2) *
      ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))

Tactic:
simp_rw [mul_assoc _ (cexp _), ← tsum_mul_left (a := cexp _), ← Complex.exp_add]
    congr 2 with n : 1; congr 1
    field_simp
    ring_nf
    simp_rw [I_sq, I_pow_four]
    ring_nf

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

Goal state before:
pp: case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
h4 : (↑x).arg ≠ π
⊢ oddKernel (↑a) x = 1 / x ^ (3 / 2) * sinKernel (↑a) (1 / x)

Tactic:
rw [← ofReal_inj, oddKernel_def, ofReal_mul, sinKernel_def, jacobiTheta₂'_functional_equation',
    h1, h2]

Goal state after:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
h4 : (↑x).arg ≠ π
⊢ jacobiTheta₂'' (↑a) (I * ↑x) =
    ↑(1 / x ^ (3 / 2)) * (-2 * ↑π / (1 / ↑x) ^ (3 / 2) * jacobiTheta₂'' (↑a) (I * ↑x) / (-2 * ↑π))
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: ⊢ cosZeta 0 = riemannZeta

Tactic:
simp_rw [cosZeta, riemannZeta, hurwitzZetaEven, if_true, completedHurwitzZetaEven_zero,
    completedCosZeta_zero]

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

Goal state before:
pp: n : ℕ
⊢ ∀ (a b c : ℕ), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n

Tactic:
simp only [Nat.isUnit_iff]

Goal state after:
n : ℕ
⊢ ∀ (a b c : ℕ), a = 1 → b = 1 → c = 1 → a ^ n + b ^ n ≠ c ^ n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
simp_rw [push_cast, Complex.cos, neg_mul]

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

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

Tactic:
refine (hasSum_int_hurwitzZetaOdd a hs).nat_add_neg_add_one.congr_fun fun n ↦ ?_

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(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 : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
this : ∀ (b : ℝ), 0 ≤ b → ↑(SignType.sign (↑n + b)) / ↑|↑n + b| ^ s = 1 / (↑n + ↑b) ^ s
⊢ (1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2 =
    (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2

Tactic:
simp only [add_sub_assoc, this a ha.1, this (1 - a) (sub_nonneg.mpr ha.2), push_cast]

Goal state after:
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
⊢ a.gcd n = 1

Tactic:
apply Int.isCoprime_iff_gcd_eq_one.mp

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
⊢ IsCoprime a n
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 (x0 * ↑k) (y0 * ↑k) (↑((x0 * ↑k).gcd (y0 * ↑k)) * z0)
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑((x0 * ↑k).gcd (y0 * ↑k))) (y0 * ↑k / ↑((x0 * ↑k).gcd (y0 * ↑k)))
    (↑((x0 * ↑k).gcd (y0 * ↑k)) * z0 / ↑((x0 * ↑k).gcd (y0 * ↑k)))

Tactic:
rw [Int.gcd_mul_right, h2, Int.natAbs_natCast, one_mul] at h ⊢

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 (x0 * ↑k) (y0 * ↑k) (↑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
hxy : (x, y).1 ^ 2 + (x, y).2 ^ 2 = 1
hy : (x, 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:
change x ^ 2 + y ^ 2 = 1 at hxy

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
⊢ (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.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: case h
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := ⋯
⊢ ∀ᶠ (i : ℕ) in atTop, ‖f i‖ ≤ ↑i ^ (-s.re)

Tactic:
filter_upwards [eventually_gt_atTop 1] with n hn
          simp only [f, norm_mul, norm_div, norm_real, norm_eq_abs]
          grw [norm_le_one, vonMangoldt_le_log]
          have := log_pos (x := n) (mod_cast hn)
          field_simp
          rw [← ofReal_natCast n, norm_cpow_eq_rpow_re_of_nonneg (by simp) (by simp; grind)]
          simp

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

Goal state before:

Tactic:
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.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₀
⊢ { toFun := fun I ↦ ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den|, map_zero' := ⋯ } I =
    ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den|

Tactic:
ZeroHom.coe_mk

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 ℤ) ↑I.den| = ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den|
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: x : 𝓞 ℚ
⊢ IsUnit (↑ringOfIntegersEquiv x) ↔ ↑x = 1 ∨ ↑x = -1

Tactic:
Int.isUnit_iff,

Goal state after:
x : 𝓞 ℚ
⊢ ↑ringOfIntegersEquiv x = 1 ∨ ↑ringOfIntegersEquiv x = -1 ↔ ↑x = 1 ∨ ↑x = -1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
a✝ b✝ : K
hx : a✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
hy : b✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
x✝ : K →+* ℂ
⊢ star (x✝ (a✝ * b✝)) = x✝ (a✝ * b✝)

Tactic:
rw [map_mul, star_mul, hx, hy, mul_comm]

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
w : InfinitePlace K
h : IsUnramified k w
hw : (w.comap (algebraMap k K)).IsReal
⊢ ComplexEmbedding.IsReal (conjugate w.embedding)

Tactic:
simpa using isReal_iff.1 <| (isUnramified_iff.1 h).resolve_right (not_isComplex_iff_isReal.2 hw)

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ 0 ≤ { toFun := fun x ↦ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖, map_zero' := ⋯ } x

Tactic:
ZeroHom.coe_mk

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ 0 ≤ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ { toFun := fun x ↦ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖, map_zero' := ⋯ } (-x) =
    { toFun := fun x ↦ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖, map_zero' := ⋯ } x

Tactic:
ZeroHom.coe_mk

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ (if hw : w.IsReal then ‖(-x).1 ⟨w, hw⟩‖ else ‖(-x).2 ⟨w, ⋯⟩‖) = if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
⊢ { toFun := fun x ↦ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖, map_zero' := ⋯ } (x + y) ≤
    { toFun := fun x ↦ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖, map_zero' := ⋯ } x +
      { toFun := fun x ↦ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖, map_zero' := ⋯ } y

Tactic:
ZeroHom.coe_mk

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
⊢ (if hw : w.IsReal then ‖(x + y).1 ⟨w, hw⟩‖ else ‖(x + y).2 ⟨w, ⋯⟩‖) ≤
    (if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖) + if hw : w.IsReal then ‖y.1 ⟨w, hw⟩‖ else ‖y.2 ⟨w, ⋯⟩‖
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
⊢ volume (convexBodyLT' K f w₀) = ↑(convexBodyLT'Factor K) * ↑(∏ w, f w ^ w.mult)

Tactic:
by
  have vol_box : ∀ B : ℝ≥0, volume {x : ℂ | |x.re| < 1 ∧ |x.im| < B ^ 2} = 4 * B ^ 2 := by
    intro B
    rw [← (Complex.volume_preserving_equiv_real_prod.symm).measure_preimage]
    · simp_rw [Set.preimage_ofPred_eq, Complex.measurableEquivRealProd_symm_apply]
      rw [show {a : ℝ × ℝ | |a.1| < 1 ∧ |a.2| < B ^ 2} =
        Set.Ioo (-1 : ℝ) (1 : ℝ) ×ˢ Set.Ioo (-(B : ℝ) ^ 2) ((B : ℝ) ^ 2) by
          ext; simp_rw [Set.mem_ofPred_eq, Set.mem_prod, Set.mem_Ioo, abs_lt]]
      simp_rw [volume_eq_prod, prod_prod, Real.volume_Ioo, sub_neg_eq_add, one_add_one_eq_two,
        ← two_mul, ofReal_mul zero_le_two, ofReal_pow (coe_nonneg B), ofReal_ofNat,
        ofReal_coe_nnreal, ← mul_assoc, show (2 : ℝ≥0∞) * 2 = 4 by norm_num]
    · refine (MeasurableSet.inter ?_ ?_).nullMeasurableSet
      · exact measurableSet_lt (measurable_norm.comp Complex.measurable_re) measurable_const
      · exact measurableSet_lt (measurable_norm.comp Complex.measurable_im) measurable_const
  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.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
⊢ { toFun := fun x ↦ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖, map_zero' := ⋯ } (c • x) =
    |c| * { toFun := fun x ↦ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖, map_zero' := ⋯ } x

Tactic:
ZeroHom.coe_mk

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
⊢ (if hw : w.IsReal then ‖(c • x).1 ⟨w, hw⟩‖ else ‖(c • x).2 ⟨w, ⋯⟩‖) =
    |c| * if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
⊢ ∑ w, ↑w.mult * (normAtPlace w) (x + y) ≤ ∑ w, ↑w.mult * (normAtPlace w) x + ∑ w, ↑w.mult * (normAtPlace w) y

Tactic:
← Finset.sum_add_distrib,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
⊢ ∑ w, ↑w.mult * (normAtPlace w) (x + y) ≤ ∑ x_1, (↑x_1.mult * (normAtPlace x_1) x + ↑x_1.mult * (normAtPlace x_1) y)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ Continuous ⇑{ toFun := fun x ↦ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖, map_zero' := ⋯ }

Tactic:
ZeroHom.coe_mk

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ Continuous fun x ↦ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨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✝ : IsGalois k K
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
⊢ IsUnramified k (mk φ)

Tactic:
by_contra hφ

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
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬IsUnramified k (mk φ)
⊢ False
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
φ : K →+* ℂ
⊢ IsUnramified k (mk φ) ↔ ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1

Tactic:
refine ⟨fun H σ hσ ↦ hσ.isUnramified_mk_iff.mp H,
    fun H ↦ ?_⟩
  by_contra hφ
  rw [not_isUnramified_iff] at hφ
  rw [comap_mk, isReal_mk_iff, ← not_isReal_iff_isComplex, isReal_mk_iff,
    ← ComplexEmbedding.isConj_one_iff (k := k)] at hφ
  let := (φ.comp (algebraMap k K)).toAlgebra
  let := φ.toAlgebra
  have : IsScalarTower k K ℂ := IsScalarTower.of_algebraMap_eq' rfl
  let φ' : K →ₐ[k] ℂ := { star φ with
    commutes' := fun r ↦ by simpa using! RingHom.congr_fun hφ.2 r }
  have : ComplexEmbedding.IsConj φ (AlgHom.restrictNormal' φ' K) :=
    (RingHom.ext <| AlgHom.restrictNormal_commutes φ' K).symm
  exact hφ.1 (H _ this ▸ this)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ Set.range ⇑(mixedEmbedding K)
⊢ mixedEmbedding.norm x = 0 ↔ x = 0

Tactic:
by
  obtain ⟨a, rfl⟩ := hx
  rw [norm_eq_norm, Rat.cast_abs, abs_eq_zero, Rat.cast_eq_zero, Algebra.norm_eq_zero_iff,
    map_eq_zero]

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✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : (fun x ↦ x.comap (algebraMap k K)) w ∈ {w | IsUnramifiedIn K w}
⊢ #({a ∈ {w | IsUnramified k w} | a.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w}) = Nat.card Gal(K/k)

Tactic:
rw [mem_filter_univ] at hw

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)
⊢ #({a ∈ {w | IsUnramified k w} | a.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w}) = Nat.card Gal(K/k)