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

Goal state before:
pp: ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
m : ℕ
hm : 1 / |ξ - ↑q| < ↑m
m_pos : 0 < ↑m
q' : ℚ
hbd : |ξ - ↑q'| ≤ 1 / ((↑m + 1) * ↑q'.den)
hden : q'.den ≤ m
den_pos : 0 < ↑q'.den
md_pos : 0 < (↑m + 1) * ↑q'.den
⊢ 1 / ((↑m + 1) * ↑q'.den) < 1 / (↑q'.den * ↑q'.den)

Tactic:
one_div_lt_one_div md_pos (mul_pos den_pos den_pos),

Goal state after:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
m : ℕ
hm : 1 / |ξ - ↑q| < ↑m
m_pos : 0 < ↑m
q' : ℚ
hbd : |ξ - ↑q'| ≤ 1 / ((↑m + 1) * ↑q'.den)
hden : q'.den ≤ m
den_pos : 0 < ↑q'.den
md_pos : 0 < (↑m + 1) * ↑q'.den
⊢ ↑q'.den * ↑q'.den < (↑m + 1) * ↑q'.den
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: n : ℕ
⊢ convergent 0 n = 0

Tactic:
induction n with
  | zero => simp only [convergent_zero, floor_zero, cast_zero]
  | succ n ih =>
    simp only [ih, convergent_succ, floor_zero, cast_zero, fract_zero, add_zero, inv_zero]

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |ξ * ↑v * (2 * ↑v - 1) - ↑u * (2 * ↑v - 1)| < 1
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v

Tactic:
abs_sub_comm,

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑u * (2 * ↑v - 1) - ξ * ↑v * (2 * ↑v - 1)| < 1
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
Module: Mathlib.NumberTheory.LSeries.Convergence

Goal state before:
pp: f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun x ↦ ↑(f x)) < ↑x
⊢ Summable fun n ↦ f n / ↑n ^ x

Tactic:
by
  have aux : term (f ·) x = fun n ↦ ↑(if n = 0 then 0 else f n / (n : ℝ) ^ x) := by
    ext n
    simp [term_def, apply_ite ((↑) : ℝ → ℂ), ofReal_cpow n.cast_nonneg]
  have := LSeriesSummable_of_abscissaOfAbsConv_lt_re (ofReal_re x ▸ h)
  simp only [LSeriesSummable, aux, summable_ofReal] at this
  refine this.congr_cofinite ?_
  filter_upwards [(Set.finite_singleton 0).compl_mem_cofinite] with n hn
    using if_neg (by simpa using hn)

Goal state after:
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) < 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
⊢ n ^ k = m

Tactic:
have na : n ≤ xn hw1 j := (Nat.le_self_pow hk0.ne' _).trans hnka.le

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) < 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
na : n ≤ xn hw1 j
⊢ n ^ k = m
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: case succ
f : ℕ → ℂ
m : ℕ
ih : ∀ {s : ℂ}, abscissaOfAbsConv f < ↑s.re → iteratedDeriv m (LSeries f) s = (-1) ^ m * LSeries (logMul^[m] f) s
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
ih' : Set.EqOn (iteratedDeriv m (LSeries f)) ((-1) ^ m * LSeries (logMul^[m] f)) {s | abscissaOfAbsConv f < ↑s.re}
this : deriv (iteratedDeriv m (LSeries f)) s = deriv ((-1) ^ m * LSeries (logMul^[m] f)) s
⊢ iteratedDeriv (m + 1) (LSeries f) s = (-1) ^ (m + 1) * LSeries (logMul^[m + 1] f) s

Tactic:
iteratedDeriv_succ,

Goal state after:
case succ
f : ℕ → ℂ
m : ℕ
ih : ∀ {s : ℂ}, abscissaOfAbsConv f < ↑s.re → iteratedDeriv m (LSeries f) s = (-1) ^ m * LSeries (logMul^[m] f) s
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
ih' : Set.EqOn (iteratedDeriv m (LSeries f)) ((-1) ^ m * LSeries (logMul^[m] f)) {s | abscissaOfAbsConv f < ↑s.re}
this : deriv (iteratedDeriv m (LSeries f)) s = deriv ((-1) ^ m * LSeries (logMul^[m] f)) s
⊢ deriv (iteratedDeriv m (LSeries f)) s = (-1) ^ (m + 1) * LSeries (logMul^[m + 1] f) s
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_6
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 =
    rexp (-π * a ^ 2 * t) * (rexp (-π * t) / (1 - rexp (-π * t)) ^ 2)

Tactic:
rw [mul_add, add_mul, mul_one, exp_add, mul_div_assoc]

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

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ a i / (↑π ^ s * ↑(q i) ^ s) = ↑π ^ (-s) * a i / ↑(q i) ^ s

Tactic:
← div_div,

Goal state after:
case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ a i / ↑π ^ s / ↑(q i) ^ s = ↑π ^ (-s) * a i / ↑(q i) ^ s
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ ‖a i‖ / (π ^ s.re * q i ^ s.re) = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

Tactic:
← div_div,

Goal state after:
case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ ‖a i‖ / π ^ s.re / q i ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: x : ℝ
hx : 0 < x
a : ℝ
⊢ I * (1 / ↑x) = -1 / (I * ↑x)

Tactic:
← div_div,

Goal state after:
x : ℝ
hx : 0 < x
a : ℝ
⊢ I * (1 / ↑x) = -1 / I / ↑x
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ 1 / τ = -I / (-I * τ)

Tactic:
← div_div,

Goal state after:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ 1 / τ = -I / -I / τ
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i ≠ 0
⊢ ‖a i‖ * |r i| / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re

Tactic:
← div_div,

Goal state after:
case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i ≠ 0
⊢ ‖a i‖ * |r i| / |r i| ^ s.re / |r i| = ‖a i‖ / |r i| ^ s.re
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: x : ℝ
hx : 0 < x
a : ℝ
⊢ -1 / ((↑x)⁻¹ * I) = I * ↑x

Tactic:
← div_div,

Goal state after:
x : ℝ
hx : 0 < x
a : ℝ
⊢ -1 / (↑x)⁻¹ / I = I * ↑x
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (expZeta a) s

Tactic:
apply DifferentiableAt.add

Goal state after:
case hf
a : UnitAddCircle
s : ℂ
hs : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (cosZeta a) s

case hg
a : UnitAddCircle
s : ℂ
hs : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (fun s ↦ I * sinZeta a s) s
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: case h
k : ℕ
m : ℕ := 2 ^ k.primesBelow.card
N₀ : ℕ := 2 * m ^ 2
hN₀ : N₀ = 2 * m ^ 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p
this : 1 / 2 ≤ S
⊢ 4 ^ (k.primesBelow.card + 1) = 2 * N₀

Tactic:
rw [show 4 = 2 ^ 2 by simp, pow_right_comm]

Goal state after:
case h
k : ℕ
m : ℕ := 2 ^ k.primesBelow.card
N₀ : ℕ := 2 * m ^ 2
hN₀ : N₀ = 2 * m ^ 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p
this : 1 / 2 ≤ S
⊢ (2 ^ (k.primesBelow.card + 1)) ^ 2 = 2 * N₀
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ abscissaOfAbsConv 1 < ↑s.re

Tactic:
rw [abscissaOfAbsConv_one]

Goal state after:
s : ℂ
hs : 1 < s.re
⊢ 1 < ↑s.re
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s✝ : ℂ
hs' : s✝ ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
s : ℂ
hs : s ≠ 0
⊢ s * Λ s / (s * s.Gammaℝ) = Λ s / s.Gammaℝ

Tactic:
← div_div,

Goal state after:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s✝ : ℂ
hs' : s✝ ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
s : ℂ
hs : s ≠ 0
⊢ s * Λ s / s / s.Gammaℝ = Λ s / s.Gammaℝ
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ HasProd (fun p ↦ (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) (L (fun n ↦ χ ↑n) s)

Tactic:
← tsum_dirichletSummand χ hs

Goal state after:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ HasProd (fun p ↦ (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) (∑' (n : ℕ), (dirichletSummandHom χ ⋯) n)
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) atTop (𝓝 (L (fun n ↦ χ ↑n) s))

Tactic:
← tsum_dirichletSummand χ hs

Goal state after:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) atTop (𝓝 (∑' (n : ℕ), (dirichletSummandHom χ ⋯) n))
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 * c1).natAbs

Tactic:
Int.natAbs_mul,

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
⊢ c1.natAbs < (↑p ^ 2).natAbs * c1.natAbs
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hdab : derivative a = 0 ∧ derivative b = 0
⊢ a.wronskian b = 0

Tactic:
obtain ⟨hda, hdb⟩ := hdab
    rw [wronskian]
    rw [hda, hdb]; simp only [mul_zero, zero_mul, sub_self]

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
⊢ (normalizedFactors a).Nodup

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0
  · simp
  rwa [← squarefree_iff_nodup_normalizedFactors ha₀, ← isRadical_iff_squarefree_of_ne_zero ha₀]

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

Goal state before:
pp: case inl
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
⊢ (∃ n, a ∣ 0 ^ n) ↔ radical a ∣ 0

pp: case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
⊢ (∃ n, a ∣ b ^ n) ↔ radical a ∣ b

Tactic:
· exact ⟨by simp, fun _ ↦ ⟨1, by simp⟩⟩

Goal state after:
case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
⊢ (∃ n, a ∣ b ^ n) ↔ radical a ∣ b
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
⊢ mk (ComplexEmbedding.conjugate φ) = mk φ

Tactic:
refine DFunLike.ext _ _ (fun x => ?_)

Goal state after:
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
x : K
⊢ (mk (ComplexEmbedding.conjugate φ)) x = (mk φ) x
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ ↑1 ≤ ↑w.mult

Tactic:
Nat.cast_le

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ 1 ≤ w.mult
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : ∀ (w : { w // w.IsComplex }), #{φ | mkComplex φ = w} = 2
⊢ card { φ // ¬ComplexEmbedding.IsReal φ } = 2 * nrComplexPlaces K

Tactic:
by
    rw [Fintype.card, Finset.card_eq_sum_ones, ← Finset.sum_fiberwise _ (fun φ => mkComplex φ)]
    simp_rw [Finset.sum_const, this, smul_eq_mul, mul_one, Fintype.card, Finset.card_eq_sum_ones,
      Finset.mul_sum, Finset.sum_const, smul_eq_mul, mul_one]

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
⊢ (Measure.pi fun x ↦ volume) (Set.univ.pi fun w ↦ ball 0 ↑(f ↑w)) *
      (Measure.pi fun x ↦ volume) (Set.univ.pi fun w ↦ ball 0 ↑(f ↑w)) =
    (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) * ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi

Tactic:
pi_pi,

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ (∏ i, volume (ball 0 ↑(f ↑i))) * ∏ i, volume (ball 0 ↑(f ↑i)) =
    (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) * ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi
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
⊢ (Measure.pi fun x ↦ volume) (Set.univ.pi fun w ↦ ball 0 ↑(f ↑w)) *
      (Measure.pi fun x ↦ volume)
        (Set.univ.pi fun w ↦ if w = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑w) ^ 2} else ball 0 ↑(f ↑w)) =
    (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))

Tactic:
pi_pi,

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
⊢ (∏ i, volume (ball 0 ↑(f ↑i))) *
      ∏ i, volume (if i = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑i) ^ 2} else ball 0 ↑(f ↑i)) =
    (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈ Submodule.span ℤ (Set.range ⇑(latticeBasis K)) ↔ x ∈ ((canonicalEmbedding K).comp (algebraMap (𝓞 K) K)).range

Tactic:
by
  rw [show Set.range (latticeBasis K) =
      (canonicalEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (integralBasis K)) by
    rw [← Set.range_comp]; exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))]
  rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe]
  rw [← RingHom.map_range, Subring.mem_map, Set.mem_image]
  simp only [SetLike.mem_coe, mem_span_integralBasis K]
  rfl

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
w w' : InfinitePlace K
h : (mk w.embedding).comap (algebraMap k K) = w'.comap (algebraMap k K)
⊢ ∃ σ, σ • w = w'

Tactic:
← mk_embedding w',

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 w' : InfinitePlace K
h : (mk w.embedding).comap (algebraMap k K) = (mk w'.embedding).comap (algebraMap k K)
⊢ ∃ σ, σ • w = w'
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case h
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)
σ : Gal(K/k)
hσ : w.embedding.comp ↑σ.symm = w'.embedding
⊢ σ • mk w.embedding = w'

Tactic:
← mk_embedding w',

Goal state after:
case h
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)
σ : Gal(K/k)
hσ : w.embedding.comp ↑σ.symm = w'.embedding
⊢ σ • mk w.embedding = mk w'.embedding
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case h
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 : conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)
σ : Gal(K/k)
hσ : ((starRingEnd ℂ).comp w.embedding).comp ↑σ.symm = w'.embedding
⊢ σ • mk w.embedding = w'

Tactic:
← mk_embedding w',

Goal state after:
case h
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 : conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)
σ : Gal(K/k)
hσ : ((starRingEnd ℂ).comp w.embedding).comp ↑σ.symm = w'.embedding
⊢ σ • mk w.embedding = mk w'.embedding
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case h
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 : conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)
σ : Gal(K/k)
hσ : ((starRingEnd ℂ).comp w.embedding).comp ↑σ.symm = w'.embedding
⊢ σ • w = w'

Tactic:
rw [← mk_embedding w, ← mk_embedding w', smul_mk, mk_eq_iff]

Goal state after:
case h
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 : conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)
σ : Gal(K/k)
hσ : ((starRingEnd ℂ).comp w.embedding).comp ↑σ.symm = w'.embedding
⊢ w.embedding.comp ↑σ.symm = w'.embedding ∨ conjugate (w.embedding.comp ↑σ.symm) = w'.embedding
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Disjoint (Submodule.span ℝ (Set.range ⇑(canonicalEmbedding.latticeBasis K))) (commMap K).ker

Tactic:
refine LinearMap.disjoint_ker.mpr (fun x h_mem h_zero => ?_)
  replace h_mem : x ∈ Submodule.span ℝ (Set.range (canonicalEmbedding K)) := by
    refine (Submodule.span_mono ?_) h_mem
    rintro _ ⟨i, rfl⟩
    exact ⟨integralBasis K i, (canonicalEmbedding.latticeBasis_apply K i).symm⟩
  ext1 φ
  rw [Pi.zero_apply]
  by_cases hφ : ComplexEmbedding.IsReal φ
  · apply Complex.ext
    · rw [← embedding_mk_eq_of_isReal hφ, ← commMap_apply_of_isReal K x ⟨φ, hφ, rfl⟩]
      exact congrFun (congrArg (fun x => x.1) h_zero) ⟨InfinitePlace.mk φ, _⟩
    · rw [Complex.zero_im, ← Complex.conj_eq_iff_im, canonicalEmbedding.conj_apply _ h_mem,
        ComplexEmbedding.isReal_iff.mp hφ]
  · have := congrFun (congrArg (fun x => x.2) h_zero) ⟨InfinitePlace.mk φ, ⟨φ, hφ, rfl⟩⟩
    cases embedding_mk_eq φ with
    | inl h => rwa [← h, ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]
    | inr h =>
        apply RingHom.injective (starRingEnd ℂ)
        rwa [canonicalEmbedding.conj_apply _ h_mem, ← h, map_zero,
          ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Measure.pi fun x ↦ volume) (Set.univ.pi fun x ↦ Set.Ico 0 1) *
      (Measure.pi fun x ↦ volume) (Set.univ.pi fun x ↦ ⇑measurableEquivPi ⁻¹' Set.univ.pi fun x ↦ Set.Ico 0 1) =
    1

Tactic:
pi_pi,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (∏ i, volume (Set.Ico 0 1)) *
      (Measure.pi fun x ↦ volume) (Set.univ.pi fun x ↦ ⇑measurableEquivPi ⁻¹' Set.univ.pi fun x ↦ Set.Ico 0 1) =
    1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (∏ i, volume (Set.Ico 0 1)) *
      (Measure.pi fun x ↦ volume) (Set.univ.pi fun x ↦ ⇑measurableEquivPi ⁻¹' Set.univ.pi fun x ↦ Set.Ico 0 1) =
    1

Tactic:
pi_pi,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (∏ i, volume (Set.Ico 0 1)) * ∏ i, volume (⇑measurableEquivPi ⁻¹' Set.univ.pi fun x ↦ Set.Ico 0 1) = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (∏ i, volume (Set.Ico 0 1)) * ∏ i, (Measure.pi fun x ↦ volume) (Set.univ.pi fun x ↦ Set.Ico 0 1) = 1

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ NullMeasurableSet (Set.univ.pi fun x ↦ Set.Ico 0 1) volume

Tactic:
pi_pi,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (∏ i, volume (Set.Ico 0 1)) * ∏ i, ∏ i, volume (Set.Ico 0 1) = 1

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

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

Tactic:
negAt_apply_isReal_and_mem _ hw,

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∈ s
⊢ ((negAt s).symm x).1 w = -x.1 w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsReal }
hw : x.1 w ≤ 0
⊢ ((negAt (signSet x)) x).1 w = ‖x.1 w‖

Tactic:
negAt_apply_isReal_and_mem _ hw,

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsReal }
hw : x.1 w ≤ 0
⊢ -x.1 w = ‖x.1 w‖