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

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
this :
  ∃ p,
    0 < p ∧
      (fun t ↦
          rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t ↦ rexp (-p * t)
p : ℝ
hp : 0 < p
hp' :
  (fun t ↦
      rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
    fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖F_nat 1 a t‖ ≤
    rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))

Tactic:
exact F_nat_one_le ha ht

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

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

Tactic:
h4,

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

Goal state before:
pp: case H
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)
⊢ ∃ p, 0 < p ∧ (fun x ↦ cosKernel (↑a) x - 1) =O[atTop] fun x ↦ rexp (-p * x)

Tactic:
refine ⟨p, hp, (Eventually.isBigO ?_).trans (hp'.const_mul_left 2)⟩

Goal state after:
case H
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)
⊢ ∀ᶠ (x : ℝ) in atTop, ‖cosKernel (↑a) x - 1‖ ≤ 2 * (HurwitzKernelBounds.F_nat 0 1 x - if 1 = 0 then 1 else 0)
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a b : UnitAddCircle
⊢ Differentiable ℂ fun s ↦ hurwitzZeta a s - hurwitzZeta b s

Tactic:
simp only [hurwitzZeta, add_sub_add_comm]
  refine (differentiable_hurwitzZetaEven_sub_hurwitzZetaEven a b).add (.sub ?_ ?_)
  all_goals apply differentiable_hurwitzZetaOdd

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
x y : ℂ
⊢ 2 * x * Complex.Gamma s * ((y + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * x * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - y) * I / 2) * sinZeta a s =
    x * Complex.Gamma s *
      (cexp (-(↑π * s / 2) * I) * (cosZeta a s + I * sinZeta a s) + y * (cosZeta a s + I * -sinZeta a s))

Tactic:
generalize (-(↑π * s / 2) * I).exp = z

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
x y z : ℂ
⊢ 2 * x * Complex.Gamma s * ((y + z) / 2) * cosZeta a s + 2 * x * Complex.Gamma s * ((z - y) * I / 2) * sinZeta a s =
    x * Complex.Gamma s * (z * (cosZeta a s + I * sinZeta a s) + y * (cosZeta a s + I * -sinZeta 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 : ℂ
⊢ 2 * x * Complex.Gamma s * ((y + cexp (-(↑π * s / 2) * I)) / 2) * hurwitzZetaEven a s +
      I * (2 * x * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - y) * I / 2) * hurwitzZetaOdd a s) =
    x * Complex.Gamma s *
      (y * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-(↑π * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))

Tactic:
generalize (-(↑π * s / 2) * I).exp = z

Goal state after:
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))
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: k : ℕ
⊢ 1 / 2 ≤ ∑ p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow, 1 / ↑p

Tactic:
set m : ℕ := 2 ^ k.primesBelow.card
  set N₀ : ℕ := 2 * m ^ 2 with hN₀
  let S : ℝ := ((2 * N₀).succ.primesBelow \ k.primesBelow).sum (fun p ↦ (1 / p : ℝ))
  suffices 1 / 2 ≤ S by
    convert! this using 5
    rw [show 4 = 2 ^ 2 by simp, pow_right_comm]
    ring
  suffices 2 * N₀ ≤ m * (2 * N₀).sqrt + 2 * N₀ * S by
    rwa [hN₀, ← mul_assoc, ← pow_two 2, ← mul_pow, sqrt_eq', ← sub_le_iff_le_add',
      cast_mul, cast_mul, cast_pow, cast_two,
      show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,
      mul_le_mul_iff_right₀ <| by positivity] at this
  calc (2 * N₀ : ℝ)
    _ = ((2 * N₀).smoothNumbersUpTo k).card + ((2 * N₀).roughNumbersUpTo k).card := by
        exact_mod_cast ((2 * N₀).smoothNumbersUpTo_card_add_roughNumbersUpTo_card k).symm
    _ ≤ m * (2 * N₀).sqrt + ((2 * N₀).roughNumbersUpTo k).card := by
        exact_mod_cast Nat.add_le_add_right ((2 * N₀).smoothNumbersUpTo_card_le k) _
    _ ≤ m * (2 * N₀).sqrt + 2 * N₀ * S := by grw [roughNumbersUpTo_card_le']; norm_cast

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

Goal state before:
pp: case H
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
⊢ ∃ p, 0 < p ∧ sinKernel ↑a =O[atTop] fun x ↦ rexp (-p * x)

Tactic:
refine ⟨p, hp, (Eventually.isBigO ?_).trans (hp'.const_mul_left 2)⟩

Goal state after:
case H
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop, ‖sinKernel (↑a) x‖ ≤ 2 * HurwitzKernelBounds.F_nat 1 0 x
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: z : ZMod 4
⊢ z * z ≠ 2

Tactic:
change Fin 4 at z

Goal state after:
z : Fin 4
⊢ z * z ≠ 2
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (r ^ 2 + s ^ 2) (r * s)

Tactic:
apply IsCoprime.mul_right (Int.isCoprime_of_sq_sum (isCoprime_comm.mp h))

Goal state after:
r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (r ^ 2 + s ^ 2) s
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
⊢ False

Tactic:
have ha22 : a ^ 2 % 2 = 1 := by
    rw [sq, Int.mul_emod, ha2]
    decide

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
⊢ False
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ n.gcd m = 1

Tactic:
rwa [Int.gcd_comm]

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
⊢ divRadical 0 ∣ derivative 0

Tactic:
rw [derivative_zero]

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
⊢ divRadical 0 ∣ 0
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 : s.gcd r = 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
hd : s * r = d ^ 2
j : ℤ
hj : r = j ^ 2 ∨ r = -j ^ 2
hj0 : j ≠ 0
k : ℤ
hk : s = k ^ 2 ∨ s = -k ^ 2
hk0 : k ≠ 0
hj2 : r ^ 2 = j ^ 4
hk2 : s ^ 2 = k ^ 4
hh : i ^ 2 = j ^ 4 + k ^ 4
hn : n ≠ 0
⊢ ↑i.natAbs < ↑c.natAbs

Tactic:
← Int.eq_natAbs_of_nonneg (le_of_lt hc)

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 : s.gcd r = 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
hd : s * r = d ^ 2
j : ℤ
hj : r = j ^ 2 ∨ r = -j ^ 2
hj0 : j ≠ 0
k : ℤ
hk : s = k ^ 2 ∨ s = -k ^ 2
hk0 : k ≠ 0
hj2 : r ^ 2 = j ^ 4
hk2 : s ^ 2 = k ^ 4
hh : i ^ 2 = j ^ 4 + k ^ 4
hn : n ≠ 0
⊢ ↑i.natAbs < c
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : NormalizationMonoid M
inst✝¹ : UniqueFactorizationMonoid M
a : M
inst✝ : Nontrivial M
⊢ radical a ≠ 0

Tactic:
rw [radical, ← Finset.prod_val]

Goal state after:
M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : NormalizationMonoid M
inst✝¹ : UniqueFactorizationMonoid M
a : M
inst✝ : Nontrivial M
⊢ (primeFactors a).val.prod ≠ 0
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
⊢ abc_dr.natDegree + abc_r.natDegree < a.natDegree + b.natDegree + abc_r.natDegree

Tactic:
exact Nat.add_lt_add_right abc_dr_ndeg_lt _

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
⊢ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
have ab_nz := mul_ne_zero ha hb
  have abc_nz := mul_ne_zero ab_nz hc
  -- bound the degree of `divRadical (a * b * c)` using Wronskian `w`
  set abc_dr := divRadical (a * b * c)
  have abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree := by
    calc
      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
  -- add the degree of `radical (a * b * c)` to both sides and rearrange
  set abc_r := radical (a * b * c)
  apply Nat.lt_of_add_lt_add_left
  calc
    a.natDegree + b.natDegree + c.natDegree = (a * b * c).natDegree := by
      rw [Polynomial.natDegree_mul ab_nz hc, Polynomial.natDegree_mul ha hb]
    _ = ((divRadical (a * b * c)) * (radical (a * b * c))).natDegree := by
      rw [mul_comm _ (radical _), radical_mul_divRadical]
    _ = abc_dr.natDegree + abc_r.natDegree := by
      rw [← Polynomial.natDegree_mul (divRadical_ne_zero abc_nz) radical_ne_zero]
    _ < a.natDegree + b.natDegree + abc_r.natDegree := by
      exact Nat.add_lt_add_right abc_dr_ndeg_lt _

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

Goal state before:
pp: hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
⊢ FermatLastTheoremFor n

Tactic:
obtain hdvd | ⟨p, hpprime, hdvd, hpodd⟩ := Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt h

Goal state after:
case inl
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
hdvd : 4 ∣ n
⊢ FermatLastTheoremFor n

case inr
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
p : ℕ
hpprime : Nat.Prime p
hdvd : p ∣ n
hpodd : Odd p
⊢ FermatLastTheoremFor n
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
⊢ h.IsPrimitiveClassified

Tactic:
by
  rcases h.even_odd_of_coprime hc with h1 | h2
  · exact h.isPrimitiveClassified_of_coprime_of_odd_of_pos hc h1.right hzpos
  rw [Int.gcd_comm] at hc
  obtain ⟨m, n, H⟩ := h.symm.isPrimitiveClassified_of_coprime_of_odd_of_pos hc h2.left hzpos
  use m, n; tauto

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

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

Tactic:
rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
⊢ x ∈ torsion K ↔ ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1

Tactic:
torsion,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
⊢ x ∈ CommGroup.torsion (𝓞 K)ˣ ↔ ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ ζ ∈ torsion K

Tactic:
torsion,

Goal state after:
K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ ζ ∈ CommGroup.torsion (𝓞 K)ˣ
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
⊢ ζ ∈ rootsOfUnity (torsionOrder K) (𝓞 K) ↔ ζ ∈ torsion K

Tactic:
torsion,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
⊢ ζ ∈ rootsOfUnity (torsionOrder K) (𝓞 K) ↔ ζ ∈ CommGroup.torsion (𝓞 K)ˣ
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 }
x : K
⊢ ((∀ (i : { w // w.IsReal }), ↑i x < ↑(f ↑i)) ∧
      ∀ (i : { w // w.IsComplex }),
        (↑i).embedding x ∈ if i = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑i) ^ 2} else ball 0 ↑(f ↑i)) ↔
    (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
      |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2

Tactic:
Subtype.forall

Goal state after:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
⊢ ((∀ (a : InfinitePlace K), a.IsReal → a x < ↑(f a)) ∧
      ∀ (a : InfinitePlace K) (b : a.IsComplex),
        a.embedding x ∈ if ⟨a, b⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f a) ^ 2} else ball 0 ↑(f a)) ↔
    (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
      |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case convert_6
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ b' * d ≠ 0

Tactic:
exact mul_ne_zero hb.right hb.left

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
⊢ FermatLastTheoremWith' k[X] n

Tactic:
rw [FermatLastTheoremWith']
  intro a b c ha hb hc heq
  obtain ⟨a', eq_a⟩ := gcd_dvd_left a b
  obtain ⟨b', eq_b⟩ := gcd_dvd_right a b
  set d := gcd a b
  have hd : d ≠ 0 := gcd_ne_zero_of_left ha
  rw [eq_a, eq_b, mul_pow, mul_pow, ← mul_add] at heq
  obtain ⟨c', eq_c⟩ : ∃ c', c = d * c' :=
    (IsIntegrallyClosed.pow_dvd_pow_iff (by lia)).mp ⟨_, heq.symm⟩
  rw [eq_a, mul_ne_zero_iff] at ha
  rw [eq_b, mul_ne_zero_iff] at hb
  rw [eq_c, mul_ne_zero_iff] at hc
  rw [mul_comm] at eq_a eq_b eq_c
  refine ⟨d, a', b', c', ⟨eq_a, eq_b, eq_c⟩, ?_⟩
  rw [eq_c, mul_pow, mul_comm, mul_left_inj' (pow_ne_zero n hd)] at heq
  suffices goal : a'.natDegree = 0 ∧ b'.natDegree = 0 ∧ c'.natDegree = 0 by
    simp only [natDegree_eq_zero] at goal
    obtain ⟨⟨ca', ha'⟩, ⟨cb', hb'⟩, ⟨cc', hc'⟩⟩ := goal
    rw [← ha', ← hb', ← hc']
    rw [← ha', C_ne_zero] at ha
    rw [← hb', C_ne_zero] at hb
    rw [← hc', C_ne_zero] at hc
    exact ⟨ha.right.isUnit_C, hb.right.isUnit_C, hc.right.isUnit_C⟩
  apply flt hn chn ha.right hb.right hc.right _ heq
  convert! isCoprime_div_gcd_div_gcd _
  · exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_a.symm
  · exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_b.symm
  · rw [eq_b]
    exact mul_ne_zero hb.right hb.left

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

Goal state before:
pp: case mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), (canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
x✝ : (K →+* ℂ) → ℂ
⊢ x✝ ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r →
    x✝ ∈ ⇑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r}

Tactic:
rintro ⟨⟨_, ⟨x, rfl⟩, rfl⟩, hx⟩

Goal state after:
case mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), (canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
x : 𝓞 K
hx : (canonicalEmbedding K) ((algebraMap (𝓞 K) K) x) ∈ Metric.closedBall 0 r
⊢ (canonicalEmbedding K) ((algebraMap (𝓞 K) K) x) ∈
    ⇑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ ((latticeBasis K).repr ((canonicalEmbedding K) x)) i = ↑(((integralBasis K).repr x) i)

Tactic:
rw [← Basis.restrictScalars_repr_apply ℚ _ ⟨_, mem_rat_span_latticeBasis K x⟩, eq_ratCast,
    Rat.cast_inj]
  let f := (canonicalEmbedding K).toRatAlgHom.toLinearMap.codRestrict _
    (fun x ↦ mem_rat_span_latticeBasis K x)
  suffices ((latticeBasis K).restrictScalars ℚ).repr.toLinearMap ∘ₗ f =
    (integralBasis K).repr.toLinearMap from DFunLike.congr_fun (LinearMap.congr_fun this x) i
  refine Basis.ext (integralBasis K) (fun i ↦ ?_)
  have : f (integralBasis K i) = ((latticeBasis K).restrictScalars ℚ) i := by
    apply Subtype.val_injective
    rw [LinearMap.codRestrict_apply, AlgHom.toLinearMap_apply, Basis.restrictScalars_apply,
      latticeBasis_apply]
    rfl
  simp_rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, this, Basis.repr_self]

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
σ : Gal(K/k)
w : InfinitePlace K
⊢ ¬(σ • w).IsReal ↔ ¬w.IsReal

Tactic:
isReal_smul_iff

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
⊢ ¬w.IsReal ↔ ¬w.IsReal
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ x φ = 0

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
⊢ x φ = 0

Tactic:
· 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φ]

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
⊢ x φ = 0
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case pos
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∃ σ, ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2

Tactic:
obtain ⟨σ, hσ⟩ := h

Goal state after:
case pos
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
σ : Gal(K/k)
hσ : ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:

Tactic:
_ = (∫ x : {w : InfinitePlace K // IsReal w} → ℝ, ∏ w, exp (-‖x w‖)) *
              (∫ x : {w : InfinitePlace K // IsComplex w} → ℂ, ∏ w, exp (-2 * ‖x w‖)) := by
        simp_rw [convexBodySumFun_apply', neg_add, ← neg_mul, Finset.mul_sum,
          ← Finset.sum_neg_distrib, exp_add, exp_sum, ← integral_prod_mul, volume_eq_prod]
      _ = (∫ x : ℝ, exp (-|x|)) ^ nrRealPlaces K *
              (∫ x : ℂ, Real.exp (-2 * ‖x‖)) ^ nrComplexPlaces K := by
        rw [integral_fintype_prod_volume_eq_pow (fun x => exp (-‖x‖)),
          integral_fintype_prod_volume_eq_pow (fun x => exp (-2 * ‖x‖))]
        simp_rw [norm_eq_abs]
      _ = (2 * Gamma (1 / 1 + 1)) ^ nrRealPlaces K *
              (π * (2 : ℝ) ^ (-(2 : ℝ) / 1) * Gamma (2 / 1 + 1)) ^ nrComplexPlaces K := by
        rw [integral_comp_abs (f := fun x => exp (-x)), ← integral_exp_neg_rpow zero_lt_one,
          ← Complex.integral_exp_neg_mul_rpow le_rfl zero_lt_two]
        simp_rw [Real.rpow_one]
      _ = (2 : ℝ) ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K := by
        simp_rw [div_one, one_add_one_eq_two, Gamma_add_one two_ne_zero, Gamma_two, mul_one,
          mul_assoc, ← Real.rpow_add_one two_ne_zero, show (-2 : ℝ) + 1 = -1 by norm_num,
          Real.rpow_neg_one, div_eq_mul_inv]

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))
⊢ minkowskiBound K I ≤ volume (convexBodySum K B)

Tactic:
refine le_of_eq ?_

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))
⊢ minkowskiBound K I = volume (convexBodySum K B)
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))
⊢ minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹ ≠ ∞

Tactic:
exact mul_ne_top (ne_of_lt (minkowskiBound_lt_top K I)) coe_ne_top

Goal state after:
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
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
hw : ¬w.IsComplex
⊢ ¬v.IsComplex

Tactic:
exact mt (isComplex_of_isComplex_under w) hw

Goal state after: