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

Goal state before:
pp: case refine_2
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ 2 * ↑π * I * ↑a * ↑n = 2 * ↑π * I * ↑n * ↑a

pp: case refine_3
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -↑π * ↑n ^ 2 * ↑t = ↑π * I * ↑n ^ 2 * (I * ↑t)

Tactic:
· exact mul_right_comm (2 * π * I) a n

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
hs' : ∀ (n : ℕ), s ≠ -↑n
x y z : ℂ
⊢ 2 * x * Complex.Gamma s * ((y + z) / 2) * hurwitzZetaEven a s +
      I * (2 * x * Complex.Gamma s * ((z - y) * I / 2) * hurwitzZetaOdd a s) =
    x * Complex.Gamma s *
      (y * (hurwitzZetaEven a s + hurwitzZetaOdd a s) + z * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))

Tactic:
ring_nf

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
hs' : ∀ (n : ℕ), s ≠ -↑n
x y z : ℂ
⊢ x * Complex.Gamma s * y * hurwitzZetaEven a s - x * Complex.Gamma s * y * I ^ 2 * hurwitzZetaOdd a s +
        x * Complex.Gamma s * z * hurwitzZetaEven a s +
      x * Complex.Gamma s * z * I ^ 2 * hurwitzZetaOdd a s =
    x * Complex.Gamma s * y * hurwitzZetaEven a s + x * Complex.Gamma s * y * hurwitzZetaOdd a s +
        x * Complex.Gamma s * z * hurwitzZetaEven a s -
      x * Complex.Gamma s * z * hurwitzZetaOdd a s
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
hs' : ∀ (n : ℕ), s ≠ -↑n
x y z : ℂ
⊢ x * Complex.Gamma s * y * hurwitzZetaEven a s - x * Complex.Gamma s * y * -1 * hurwitzZetaOdd a s +
        x * Complex.Gamma s * z * hurwitzZetaEven a s +
      x * Complex.Gamma s * z * -1 * hurwitzZetaOdd a s =
    x * Complex.Gamma s * y * hurwitzZetaEven a s + x * Complex.Gamma s * y * hurwitzZetaOdd a s +
        x * Complex.Gamma s * z * hurwitzZetaEven a s -
      x * Complex.Gamma s * z * hurwitzZetaOdd a s

Tactic:
ring_nf

Goal state after:
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: 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 : 2 * (↑2 * ↑(m ^ 2)) - ↑m * (↑2 * ↑m) ≤ 2 * (↑2 * ↑(m ^ 2)) * S
⊢ 1 / 2 ≤ S

Tactic:
cast_pow,

Goal state after:
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 : 2 * (↑2 * ↑m ^ 2) - ↑m * (↑2 * ↑m) ≤ 2 * (↑2 * ↑m ^ 2) * S
⊢ 1 / 2 ≤ S
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
simp_rw [← claim2.limUnder_eq]

Goal state after:
case inr
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
⊢ DifferentiableAt ℂ (Function.update (fun s ↦ Λ s / s.Gammaℝ) 0 ((𝓝[≠] 0).limUnder fun s ↦ Λ s / s.Gammaℝ)) 0
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ a ^ (m * k) + b ^ (m * k) ≠ c ^ (m * k)

Tactic:
simp_rw [pow_mul']

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ (a ^ k) ^ m + (b ^ k) ^ m ≠ (c ^ k) ^ m
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
by
  rw [cosZeta, Function.update_of_ne (ne_zero_of_one_lt_re hs)]
  refine ((hasSum_int_completedCosZeta a hs).div_const (Gammaℝ s)).congr_fun fun n ↦ ?_
  rw [mul_div_assoc _ (cexp _), div_right_comm _ (2 : ℂ),
    mul_div_cancel_left₀ _ (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]

Goal state after:
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 ↦ (cexp (2 * ↑π * ↑a * ↑n * I) + cexp (-(2 * ↑π * ↑a * ↑n) * I)) / 2 / ↑n ^ s) (cosZeta (↑a) s)

Tactic:
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.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
this : hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹
A : ℂ
⊢ completedCosZeta a s * (A * s.Gammaℝ⁻¹) = A * (completedCosZeta a s / s.Gammaℝ)

Tactic:
ring_nf

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ cexp (∑' (p : Primes), -Complex.log (1 - ↑↑p ^ (-s))) = L 1 s

Tactic:
convert!
    modOne_eq_one (R := ℂ) ▸
      DirichletCharacter.LSeries_eulerProduct_exp_log (1 : DirichletCharacter ℂ 1) hs using 7

Goal state after:
s : ℂ
hs : 1 < s.re
x✝ : Primes
⊢ ↑↑x✝ ^ (-s) = 1 ↑↑x✝ * ↑↑x✝ ^ (-s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr.e_a.e_a.e_a
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) +
            (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) /
          ↑n ^ s /
        2)
    (completedSinZeta (↑a) s)
n : ℕ
h : n ≠ 0
⊢ I * (cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) =
    I * (cexp (-(2 * ↑π * I * ↑a * ↑n)) - cexp (2 * ↑π * I * ↑a * ↑n))

Tactic:
neg_mul

Goal state after:
case inr.e_a.e_a.e_a
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) +
            (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) /
          ↑n ^ s /
        2)
    (completedSinZeta (↑a) s)
n : ℕ
h : n ≠ 0
⊢ I * (cexp (-(2 * ↑π * ↑a * ↑n * I)) - cexp (2 * ↑π * ↑a * ↑n * I)) =
    I * (cexp (-(2 * ↑π * I * ↑a * ↑n)) - cexp (2 * ↑π * I * ↑a * ↑n))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
A : ℂ
⊢ completedHurwitzZetaEven a s * (A * s.Gammaℝ⁻¹) = A * (completedHurwitzZetaEven a s / s.Gammaℝ)

Tactic:
ring_nf

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n ↦ ↑n + a
c : ℤ → ℂ := fun n ↦ 1 / 2
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaOdd (↑a) s)

Tactic:
have hF t (ht : 0 < t) : HasSum (fun n ↦ c n * r n * rexp (-π * (r n) ^ 2 * t))
      (oddKernel a t / 2) := by
    refine ((hasSum_ofReal.mpr (hasSum_int_oddKernel a ht)).div_const 2).congr_fun fun n ↦ ?_
    simp [r, c, push_cast, div_mul_eq_mul_div, -one_div]

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n ↦ ↑n + a
c : ℤ → ℂ := fun n ↦ 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑(r n) * ↑(rexp (-π * r n ^ 2 * t))) (↑(oddKernel (↑a) t) / 2)
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaOdd (↑a) s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ -(↑n + 1) + a = -(↑n + 1 - a)

Tactic:
ring_nf

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

Goal state before:
pp: a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ c ^ 2 = (-c) ^ 2

Tactic:
exact (neg_sq c).symm

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ z * z = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2

Tactic:
rw [← h.eq]

Goal state after:
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ (x0 * 2 + 1) * (x0 * 2 + 1) + (y0 * 2 + 1) * (y0 * 2 + 1) = 4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : p = 2
h3 : (m ^ 2 + n ^ 2) % 2 = 1
⊢ 2 ∣ m ^ 2 + n ^ 2

Tactic:
rwa [h2] at hp2

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime b c

Tactic:
rw [add_eq_zero_iff_neg_eq] at heq

Goal state after:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : -(C u * a ^ p + C v * b ^ q) = C w * c ^ r
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime b c
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
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
⊢ w = Rat.divInt ((m ^ 2 - n ^ 2) / 2 * 2) ((m ^ 2 + n ^ 2) / 2 * 2)

Tactic:
Int.ediv_mul_cancel h1.1,

Goal state after:
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
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
⊢ w = Rat.divInt ((m ^ 2 - n ^ 2) / 2 * 2) (m ^ 2 + n ^ 2)
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case inr.hi
k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
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
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
ih_d :
  ∀ m ≤ d,
    ∀ {a b c : k[X]},
      C u * a ^ p + C v * b ^ q + C w * c ^ r = 0 → a ≠ 0 → b ≠ 0 → c ≠ 0 → IsCoprime a b → a.natDegree = m → m = 0
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
⊢ d + 1 = 0

Tactic:
suffices hca : ca.natDegree = 0 by
        rw [← eq_d, eq_deg_a, hca, zero_mul]

Goal state after:
case inr.hi
k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
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
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
ih_d :
  ∀ m ≤ d,
    ∀ {a b c : k[X]},
      C u * a ^ p + C v * b ^ q + C w * c ^ r = 0 → a ≠ 0 → b ≠ 0 → c ≠ 0 → IsCoprime a b → a.natDegree = m → m = 0
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
⊢ ca.natDegree = 0
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
this : Fintype ↥(torsion K) := Fintype.ofFinite ↥(torsion K)
⊢ Nat.card ↥(torsion K) = 2

Tactic:
Nat.card_eq_fintype_card

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
this : Fintype ↥(torsion K) := Fintype.ofFinite ↥(torsion K)
⊢ Fintype.card ↥(torsion K) = 2
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card { φ // ¬ComplexEmbedding.IsReal φ } = 2 * nrComplexPlaces K

Tactic:
suffices ∀ w : { w : InfinitePlace K // IsComplex w },
     #{φ : {φ //¬ ComplexEmbedding.IsReal φ} | mkComplex φ = w} = 2 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:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∀ (w : { w // w.IsComplex }), #{φ | mkComplex φ = w} = 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ∏ w, Function.update f w₁ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) w ^ w.mult = B

Tactic:
rw [← Finset.mul_prod_erase Finset.univ _ (Finset.mem_univ w₁), Function.update_self,
      Finset.prod_congr rfl fun w hw => by rw [Function.update_of_ne (Finset.ne_of_mem_erase hw)],
      ← NNReal.rpow_natCast, ← NNReal.rpow_mul, inv_mul_cancel₀, NNReal.rpow_one, mul_assoc,
      inv_mul_cancel₀, mul_one]
    · rw [Finset.prod_ne_zero_iff]
      exact fun w hw => pow_ne_zero _ (hf w (Finset.ne_of_mem_erase hw))
    · rw [mult]; split_ifs <;> norm_num

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

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

Tactic:
rintro _ ⟨x, rfl⟩
    rw [apply_at, apply_at, ComplexEmbedding.conjugate_coe_eq]

Goal state after:
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 ℂ)
⊢ M = N.transpose

Tactic:
{ ext : 2; 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
F : Type u_3
inst✝² : Field F
inst✝¹ : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ Quotient (MulAction.orbitRel Gal(K/k) (InfinitePlace K)) ≃ InfinitePlace k

Tactic:
by
  refine Equiv.ofBijective (Quotient.lift (comap · (algebraMap k K))
    fun _ _ e ↦ (mem_orbit_iff.mp e).symm) ⟨?_, ?_⟩
  · rintro ⟨w⟩ ⟨w'⟩ e
    exact Quotient.sound (mem_orbit_iff.mpr e.symm)
  · intro w
    obtain ⟨w', hw⟩ := comap_surjective (K := K) w
    exact ⟨⟦w'⟧, hw⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) ≠ 0

Tactic:
classical exact ZSpan.measure_fundamentalDomain_ne_zero _

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

Goal state before:
pp: case inr.«1»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsComplex }
⊢ (x (↑w).embedding - (starRingEnd ℂ) (x (↑w).embedding)) / (2 * I) =
    -(2⁻¹ * I * x (↑w).embedding) + 2⁻¹ * I * (starRingEnd ℂ) (x (↑w).embedding)

Tactic:
ring_nf

Goal state after:
case inr.«1»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsComplex }
⊢ x (↑w).embedding * I⁻¹ * (1 / 2) + (starRingEnd ℂ) (x (↑w).embedding) * I⁻¹ * (-1 / 2) =
    x (↑w).embedding * I * (-1 / 2) + (starRingEnd ℂ) (x (↑w).embedding) * I * (1 / 2)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
this : Algebra K ℂ := v.embedding.toAlgebra
⊢ (unramifiedPlacesOver L v).ncard + 2 * (ramifiedPlacesOver L v).ncard = finrank K L

Tactic:
← AlgHom.card K L ℂ,

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
this : Algebra K ℂ := v.embedding.toAlgebra
⊢ (unramifiedPlacesOver L v).ncard + 2 * (ramifiedPlacesOver L v).ncard = Fintype.card (L →ₐ[K] ℂ)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) * 4 ^ ↑(nrComplexPlaces K) * √|↑(discr K)| * ↑(finrank ℚ K).factorial *
      (1 / π ^ nrComplexPlaces K) =
    ↑(FractionalIdeal.absNorm ↑I) * (4 ^ nrComplexPlaces K / π ^ nrComplexPlaces K) * ↑(finrank ℚ K).factorial *
      √|↑(discr K)|

Tactic:
zpow_natCast

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) * 4 ^ nrComplexPlaces K * √|↑(discr K)| * ↑(finrank ℚ K).factorial *
      (1 / π ^ nrComplexPlaces K) =
    ↑(FractionalIdeal.absNorm ↑I) * (4 ^ nrComplexPlaces K / π ^ nrComplexPlaces K) * ↑(finrank ℚ K).factorial *
      √|↑(discr K)|
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∃ a,
    a ≠ 0 ∧
      ↑|(Algebra.norm ℚ) ↑a| ≤
        (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|

Tactic:
obtain ⟨_, h_mem, h_nz, h_nm⟩ := exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr K ↑1
  obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem
  refine ⟨a, ne_zero_of_map h_nz, ?_⟩
  simp_rw [Units.val_one, FractionalIdeal.absNorm_one, Rat.cast_one, one_mul] at h_nm
  exact h_nm

Goal state after:
Module: Mathlib.RingTheory.Invariant.Galois

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsFractionRing A K
inst✝⁸ : IsFractionRing B L
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
h✝ : IsGalois K L
h : IntermediateField.fixedField ⊤ = ⊥
this : MulSemiringAction Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
a : A
hk : (algebraMap A B) a = b
hb : IsIntegral A ((algebraMap A K) a)
⊢ ∃ a, (algebraMap A B) a = b

Tactic:
exact ⟨a, hk⟩

Goal state after: