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

Goal state before:
pp: case refine_2.inl
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term x z τ
hτ✝ : τ.im ≤ 0
hτ : τ.im < 0
⊢ Tendsto (fun n ↦ rexp (-π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im)) atTop atTop

Tactic:
conv =>
        enter [1, n]
        rw [show -π * n ^ 2 * τ.im - 2 * π * n * z.im =
              n * (n * (-π * τ.im) - 2 * π * z.im) by ring]

Goal state after:
case refine_2.inl
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term x z τ
hτ✝ : τ.im ≤ 0
hτ : τ.im < 0
⊢ Tendsto (fun n ↦ rexp (↑n * (↑n * (-π * τ.im) - 2 * π * z.im))) atTop atTop
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case inr.H
x : ℝ
hx : 0 < x
a : ℝ
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x) = ↑(1 / x ^ (1 / 2)) * ↑(cosKernel (↑a) (1 / x))

Tactic:
cosKernel_def,

Goal state after:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x) = ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x : ℝ
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)

Tactic:
rcases le_or_gt x 0 with hx | hx
  · rw [evenKernel_undef _ hx, cosKernel_undef, mul_zero]
    exact div_nonpos_of_nonneg_of_nonpos zero_le_one hx
  induction a using QuotientAddGroup.induction_on with | H a =>
  rw [← ofReal_inj, ofReal_mul, evenKernel_def, cosKernel_def, jacobiTheta₂_functional_equation]
  have h1 : I * ↑(1 / x) = -1 / (I * x) := by
    push_cast
    rw [← div_div, mul_one_div, div_I, neg_one_mul, neg_neg]
  have hx' : I * x ≠ 0 := mul_ne_zero I_ne_zero (ofReal_ne_zero.mpr hx.ne')
  have h2 : a * I * x / (I * x) = a := by
    rw [div_eq_iff hx']
    ring
  have h3 : 1 / (-I * (I * x)) ^ (1 / 2 : ℂ) = 1 / ↑(x ^ (1 / 2 : ℝ)) := by
    rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg, ofReal_cpow hx.le, ofReal_div,
      ofReal_one, ofReal_ofNat]
  have h4 : -π * I * (a * I * x) ^ 2 / (I * x) = - (-π * a ^ 2 * x) := by
    rw [mul_pow, mul_pow, I_sq, div_eq_iff hx']
    ring
  rw [h1, h2, h3, h4, ← mul_assoc, mul_comm (cexp _), mul_assoc _ (cexp _) (cexp _),
    ← Complex.exp_add, neg_add_cancel, Complex.exp_zero, mul_one, ofReal_div, ofReal_one]

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      (cexp (2 * ↑π * I * ↑a * ↑(n + 1)) + cexp (-(2 * ↑π * I * ↑a * ↑(n + 1)))) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t)))
    (↑(cosKernel (↑a) t) - 1)
n : ℕ
⊢ (cexp (2 * ↑π * ↑a * (↑n + 1) * I) + cexp (-(2 * ↑π * ↑a * (↑n + 1)) * I)) * cexp (-↑π * (↑n + 1) ^ 2 * ↑t) =
    (cexp (2 * ↑π * I * ↑a * (↑n + 1)) + cexp (-(2 * ↑π * I * ↑a * (↑n + 1)))) * cexp (-↑π * (↑n + 1) ^ 2 * ↑t)

Tactic:
congr 3 <;> ring

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

Goal state before:
pp: a p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖∑' (b : ℕ), 2 * Real.cos (2 * π * a * (↑b + 1)) * rexp (-π * (↑b + 1) ^ 2 * t)‖ ≤
    2 * ∑' (n : ℕ), HurwitzKernelBounds.f_nat 0 1 t n

Tactic:
apply tsum_of_norm_bounded ((HurwitzKernelBounds.summable_f_nat 0 1 ht).hasSum.mul_left 2)

Goal state after:
a p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ∀ (i : ℕ),
    ‖2 * Real.cos (2 * π * a * (↑i + 1)) * rexp (-π * (↑i + 1) ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 0 1 t i
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaEven a s = (hurwitzZeta a s + hurwitzZeta (-a) s) / 2

Tactic:
by
  simp only [hurwitzZeta, hurwitzZetaEven_neg, hurwitzZetaOdd_neg]
  ring_nf

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaOdd a s = (hurwitzZeta a s - hurwitzZeta (-a) s) / 2

Tactic:
by
  simp only [hurwitzZeta, hurwitzZetaEven_neg, hurwitzZetaOdd_neg]
  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 ≠ π
⊢ jacobiTheta₂'' (↑a) (I * ↑x) =
    ↑(1 / x ^ (3 / 2)) * (-2 * ↑π / (1 / ↑x) ^ (3 / 2) * jacobiTheta₂'' (↑a) (I * ↑x) / (-2 * ↑π))

Tactic:
generalize jacobiTheta₂'' a (I * ↑x) = J

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 ≠ π
J : ℂ
⊢ J = ↑(1 / x ^ (3 / 2)) * (-2 * ↑π / (1 / ↑x) ^ (3 / 2) * J / (-2 * ↑π))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
by
  refine (((hurwitzEvenFEPair a).symm.differentiableAt_Λ (Or.inl ?_) ?_).comp s
      (differentiableAt_id.div_const _)).div_const _
  · exact div_ne_zero_iff.mpr ⟨hs, two_ne_zero⟩
  · change s / 2 ≠ ↑(1 / 2 : ℝ) ∨ (if a = 0 then 1 else 0) = 0
    refine Or.imp (fun h ↦ ?_) (fun ha ↦ ?_) hs'
    · simpa [push_cast] using h ∘ (div_left_inj' two_ne_zero).mp
    · simpa

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

Goal state before:
pp: case pos
a : ℝ
s : ℂ
hs : 1 < s.re
aux : ↑|0| ^ s = 0
hint :
  HasSum
    (fun n ↦
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (completedCosZeta (↑a) s)
n : ℕ
h : n = 0
⊢ 0 =
    s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2

pp: case neg
a : ℝ
s : ℂ
hs : 1 < s.re
aux : ↑|0| ^ s = 0
hint :
  HasSum
    (fun n ↦
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (completedCosZeta (↑a) s)
n : ℕ
h : ¬n = 0
⊢ s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s =
    s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2

Tactic:
· simp only [h, Nat.cast_zero, aux, div_zero, zero_div, neg_zero, zero_add]

Goal state after:
case neg
a : ℝ
s : ℂ
hs : 1 < s.re
aux : ↑|0| ^ s = 0
hint :
  HasSum
    (fun n ↦
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (completedCosZeta (↑a) s)
n : ℕ
h : ¬n = 0
⊢ s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s =
    s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ I * ↑n * cexp (-(2 * ↑π * ↑a * ↑n * I)) - I * ↑n * cexp (2 * ↑π * ↑a * ↑n * I) =
    I * ↑n * cexp (-(2 * ↑π * I * ↑a * ↑n)) - I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n)

Tactic:
congr 3 <;> ring

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s = -deriv (L fun n ↦ χ ↑n) s / L (fun n ↦ χ ↑n) s

Tactic:
rcases eq_or_ne N 0 with rfl | hN
  · simp [modZero_eq_delta, delta_mul_eq_smul_delta, LSeries_delta]
  -- now `N ≠ 0`
  have hχ : LSeriesSummable ↗χ s := (LSeriesSummable_iff hN χ).mpr hs
  have hs' : abscissaOfAbsConv ↗χ < s.re := by
    rwa [absicssaOfAbsConv_eq_one hN, ← EReal.coe_one, EReal.coe_lt_coe_iff]
  have hΛ : LSeriesSummable (↗χ * ↗Λ) s := LSeriesSummable_twist_vonMangoldt χ hs
  rw [eq_div_iff <| LSeries_ne_zero_of_one_lt_re χ hs, ← LSeries_convolution' hΛ hχ,
    convolution_twist_vonMangoldt, LSeries_deriv hs', neg_neg]
  exact LSeries_congr (fun _ ↦ by simp [mul_comm, logMul]) s

Goal state after:
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)
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
S_nhds : {1}ᶜ ∈ 𝓝 0
x : ℂ
⊢ x = 1 / x⁻¹

Tactic:
rw [← one_div, one_div_one_div]

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

Goal state before:
pp: case inr.inl.inr.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : c < 0
⊢ |b| ^ n + |c| ^ n = |a| ^ n

Tactic:
simp only [abs_of_pos, abs_of_neg, hn.neg_pow, add_neg_eq_iff_eq_add,
        eq_neg_add_iff_add_eq, *]

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s

Tactic:
have := differentiableAt_update_of_residue
    (fun t ht ht' ↦ differentiableAt_completedHurwitzZetaEven a (Or.inl ht) ht')
    (completedHurwitzZetaEven_residue_zero a) s hs'
  simp_rw [div_eq_mul_inv, ite_mul, zero_mul, ← div_eq_mul_inv] at this
  exact this

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

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : d ^ n * A ^ n + d ^ n * B ^ n = d ^ n * C ^ n
⊢ False

Tactic:
rw [← mul_add, mul_right_inj' (pow_ne_zero n ha.1)] at habc

Goal state after:
n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
⊢ False
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:
congr 3 <;> ring

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

Goal state before:
pp: case right
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := ⋯
S_nonempty : S.Nonempty
m : ℕ := ⋯
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
⊢ ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → s0.2.2.natAbs ≤ c1.natAbs

Tactic:
intro a1 b1 c1 h1

Goal state after:
case right
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
a1 b1 c1 : ℤ
h1 : Fermat42 a1 b1 c1
⊢ s0.2.2.natAbs ≤ 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 : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hd : r * s = d ^ 2 ∨ r * s = -d ^ 2
h1 : r * s = -d ^ 2
⊢ False

Tactic:
rw [h1] at hs

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 : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hs : b' ^ 2 = -d ^ 2 * m
hd : r * s = d ^ 2 ∨ r * s = -d ^ 2
h1 : r * s = -d ^ 2
⊢ False
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x y : M
hxy : x ≠ y
hx : Irreducible x ∧ normalize x = x ∧ x ∣ a
hy : Irreducible y ∧ normalize y = y ∧ y ∣ a
⊢ ¬x ∣ y

Tactic:
contrapose hxy

Goal state after:
case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x y : M
hx : Irreducible x ∧ normalize x = x ∧ x ∣ a
hy : Irreducible y ∧ normalize y = y ∧ y ∣ a
hxy : x ∣ y
⊢ x = y
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ ↑K

Tactic:
suffices range (ofReal : ℝ → ℂ) ⊆ closure (Set.range ((ofReal : ℝ → ℂ) ∘ ((↑) : ℚ → ℝ))) by
    refine subset_trans this ?_
    rw [← IsClosed.closure_eq hc]
    apply closure_mono
    rintro _ ⟨_, rfl⟩
    simp only [Function.comp_apply, ofReal_ratCast, SetLike.mem_coe, SubfieldClass.ratCast_mem]

Goal state after:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
φ ψ : { φ // ComplexEmbedding.IsReal φ }
h : (fun φ ↦ ⟨mk ↑φ, ⋯⟩) φ = (fun φ ↦ ⟨mk ↑φ, ⋯⟩) ψ
⊢ φ = ψ

Tactic:
Subtype.mk.injEq,

Goal state after:
case refine_2
K : Type u_1
inst✝ : Field K
φ ψ : { φ // ComplexEmbedding.IsReal φ }
h : mk ↑φ = mk ↑ψ
⊢ φ = ψ
Module: Mathlib.NumberTheory.NumberField.Units.Basic

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

Tactic:
by
  simp_rw [(isUnit_map_iff (Rat.ringOfIntegersEquiv : 𝓞 ℚ →+* ℤ) x).symm, Int.isUnit_iff,
    RingEquiv.coe_toRingHom, RingEquiv.map_eq_one_iff, RingEquiv.map_eq_neg_one_iff, ←
    Subtype.coe_injective.eq_iff]; rfl

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

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
⊢ ↑((RingOfIntegers.norm ℚ) x) = 1 ∨ ↑((RingOfIntegers.norm ℚ) x) = -1 ↔ IsUnit ((RingOfIntegers.norm ℚ) x)

Tactic:
← Rat.RingOfIntegers.isUnit_iff

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
⊢ IsUnit ((RingOfIntegers.norm ℚ) x) ↔ IsUnit ((RingOfIntegers.norm ℚ) x)
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
⊢ ∑ w, ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑x)) = 0

Tactic:
by
  simpa [Units.norm, Real.log_prod, Real.log_pow] using
    congr_arg Real.log (prod_eq_abs_norm (x : K))

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
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬ComplexEmbedding.IsConj φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
this : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra
⊢ False

Tactic:
let := φ.toAlgebra

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φ : ¬ComplexEmbedding.IsConj φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
this✝ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra
this : Algebra K ℂ := φ.toAlgebra
⊢ 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
σ : Gal(K/k)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
x✝ : Gal(K/k)
⊢ x✝ = 1 ∨ σ = x✝ ↔ x✝ = 1 ∨ x✝ = σ

Tactic:
eq_comm (a := σ)

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
x✝ : Gal(K/k)
⊢ x✝ = 1 ∨ x✝ = σ ↔ x✝ = 1 ∨ x✝ = σ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsReal }
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) (Sum.inl w)) =
    ∑ x_1,
        fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
            (Sum.inl w) (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Tactic:
stdBasis_apply_isReal,

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsReal }
⊢ ↑(x (↑w).embedding).re =
    ∑ x_1,
        fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
            (Sum.inl w) (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case inr
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
hr : (mk (w.embedding.comp (algebraMap K L))).embedding = conjugate (w.embedding.comp (algebraMap K L))
⊢ w.embedding.comp (algebraMap K L) = v.embedding ∨ (conjugate w.embedding).comp (algebraMap K L) = v.embedding

Tactic:
| inr hr =>

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

Goal state before:
pp: case inr
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : ψ ∈ mixedEmbeddingsOver L v.embedding
hr : (mk ψ).embedding = conjugate ψ
⊢ ψ ∈ Sum.elim embedding (conjugate ∘ embedding) '' Set.sumEquiv.symm (ramifiedPlacesOver L v, ramifiedPlacesOver L v)

Tactic:
| inr hr =>

Goal state after:
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) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K *
            (↑(2 ^ nrRealPlaces K) * ↑((pi / 2) ^ nrComplexPlaces K) / ↑↑(finrank ℚ K).factorial)⁻¹))) =
    ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹)))

Tactic:
NNReal.coe_pow,

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) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * (↑2 ^ nrRealPlaces K * ↑(pi / 2) ^ nrComplexPlaces K / ↑↑(finrank ℚ K).factorial)⁻¹))) =
    ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹)))
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) *
            2 ^ (↑(finrank ℚ K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π⁻¹ ^ nrComplexPlaces K =
    ↑(FractionalIdeal.absNorm ↑I) * 2 ^ (2 * ↑(nrComplexPlaces K)) * √‖discr K‖ * ↑(finrank ℚ K).factorial *
      π⁻¹ ^ nrComplexPlaces K

Tactic:
by
      congr
      rw [← card_add_two_mul_card_eq_rank, Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat]
      ring

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ((stdOrthonormalBasis K).toBasis.map ↑(toMixed K)).addHaar = volume

Tactic:
stdOrthonormalBasis_map_eq,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (stdBasis K).addHaar = volume