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

Goal state before:
pp: case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num| < ↑ξ.den / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ 1 ≤ |ξ.num * ↑q.den - ↑ξ.den * q.num|

Tactic:
mul_comm _ q.num

Goal state after:
case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num| < ↑ξ.den / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ 1 ≤ |ξ.num * ↑q.den - q.num * ↑ξ.den|
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
⊢ i = k

Tactic:
have yd : 4 * yn a1 i ∣ 4 * n := by gcongr; exact dvd_of_ysq_dvd a1 yv

Goal state after:
a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
⊢ i = k
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

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

Tactic:
rw [hf] at huv_cop
      simp only [isCoprime_zero_left, isCoprime_self, isUnit_iff] at huv_cop
      rcases huv_cop with huv_cop | huv_cop <;> linarith only [hv, huv_cop]

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

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

Tactic:
rw [hf] at huv_cop
      simp only [isCoprime_zero_left, isCoprime_self, isUnit_iff] at huv_cop
      rcases huv_cop with huv_cop | huv_cop <;> linarith only [hv, huv_cop]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
jk : j ≡ k [MOD 4 * yn a1 i]
ki : k + i < 4 * yn a1 i
ji : j ≡ i [MOD 4 * n]
this : i % (4 * yn a1 i) = k % (4 * yn a1 i)
⊢ i = k

Tactic:
rwa [Nat.mod_eq_of_lt (lt_of_le_of_lt (Nat.le_add_left _ _) ki),
              Nat.mod_eq_of_lt (lt_of_le_of_lt (Nat.le_add_right _ _) ki)] at this

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

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
N : ℕ
⊢ ∏ p ∈ range N with Nat.Prime p, (1 - f p)⁻¹ = ∑' (m : ↑(factoredNumbers (range N))), f ↑m

Tactic:
exact prod_filter_prime_geometric_eq_tsum_factoredNumbers hsum _

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n ↦ ‖term f (↑x) n‖
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
have h₁ (n) : DifferentiableOn ℂ (term f · n) S :=
    fun z _ ↦ (hasDerivAt_term f n _).differentiableAt.differentiableWithinAt

Goal state after:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n ↦ ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x ↦ term f x n) S
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: c d : ℝ
hcd : c ≤ d
⊢ (fun t ↦ rexp (-d * t)) =O[atTop] fun t ↦ rexp (-c * t)

Tactic:
by
  apply Eventually.isBigO
  filter_upwards [eventually_gt_atTop 0] with t ht
  rw [norm_of_nonneg (exp_pos _).le]
  gcongr

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: t : ℝ
ht : 0 < t
⊢ rexp (-π * t) < 1

Tactic:
simpa only [exp_lt_one_iff, neg_mul, neg_lt_zero] using mul_pos pi_pos ht

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ‖jacobiTheta₂'_term n z τ‖ ≤ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))

Tactic:
by
  rw [jacobiTheta₂'_term, norm_mul]
  refine mul_le_mul (le_of_eq ?_) (norm_jacobiTheta₂_term_le hT hz hτ n)
    (norm_nonneg _) (by positivity)
  simp only [norm_mul, Complex.norm_two, norm_I, Complex.norm_of_nonneg pi_pos.le,
    norm_intCast, mul_one, Int.cast_abs]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
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:
refine tsum_of_norm_bounded ?_ (f_le_g_nat 1 ha ht)

Goal state after:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (g_nat 1 a t)
    (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ (2 * π)⁻¹ * (2 * π) * ↑|n|

Tactic:
inv_mul_cancel₀ (mul_pos two_pos pi_pos).ne',

Goal state after:
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ 1 * ↑|n|
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case H
x : ℝ
hx : x ≤ 0
z✝ : ℝ
⊢ cosKernel (↑z✝) x = 0

Tactic:
| H =>

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

Goal state before:
pp: case H
x z✝ : ℝ
⊢ evenKernel (-↑z✝) x = evenKernel (↑z✝) x

Tactic:
| H =>

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

Goal state before:
pp: case H
x z✝ : ℝ
⊢ cosKernel (-↑z✝) x = cosKernel (↑z✝) x

Tactic:
| H =>

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

Goal state before:
pp: case inl
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ 0 = 1 / x ^ (1 / 2) * cosKernel a (1 / x)

Tactic:
cosKernel_undef,

Goal state after:
case inl
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ 0 = 1 / x ^ (1 / 2) * 0

case inl.hx
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ 1 / x ≤ 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: 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))
⊢ -↑π * I * (↑a ^ 2 * I ^ 2 * ↑x ^ 2) / (I * ↑x) = -(-↑π * ↑a ^ 2 * ↑x)

Tactic:
I_sq,

Goal state after:
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))
⊢ -↑π * I * (↑a ^ 2 * -1 * ↑x ^ 2) / (I * ↑x) = -(-↑π * ↑a ^ 2 * ↑x)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ 𝓝 0 = 𝓝 (0 • (P.ε / (↑P.k - 0)) • P.g₀)

Tactic:
zero_smul

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ 𝓝 0 = 𝓝 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a x : ℝ
⊢ cexp (I ^ 2 * ↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)) =
    cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))

Tactic:
I_sq,

Goal state after:
a x : ℝ
⊢ cexp (-1 * ↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)) =
    cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case e_a.e_f
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
⊢ ↑n * I ^ 2 * z * τ⁻¹ * 2 + ↑n ^ 2 * τ⁻¹ + I ^ 4 * z ^ 2 * τ⁻¹ =
    ↑n * I ^ 2 * z * τ⁻¹ * 2 - ↑n ^ 2 * I ^ 2 * τ⁻¹ - I ^ 2 * z ^ 2 * τ⁻¹

Tactic:
I_sq,

Goal state after:
case e_a.e_f
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
⊢ ↑n * -1 * z * τ⁻¹ * 2 + ↑n ^ 2 * τ⁻¹ + I ^ 4 * z ^ 2 * τ⁻¹ =
    ↑n * -1 * z * τ⁻¹ * 2 - ↑n ^ 2 * -1 * τ⁻¹ - -1 * z ^ 2 * τ⁻¹
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a x : ℝ
hx : 0 < x
⊢ HasSum (fun n ↦ (↑n + a) * rexp (-π * (↑n + a) ^ 2 * x)) (oddKernel (↑a) x)

Tactic:
by
  rw [← hasSum_ofReal, oddKernel_def' a x]
  have h1 := hasSum_jacobiTheta₂_term (a * I * x) (by rwa [I_mul_im, ofReal_re])
  have h2 := hasSum_jacobiTheta₂'_term (a * I * x) (by rwa [I_mul_im, ofReal_re])
  refine (((h2.div_const (2 * π * I)).add (h1.mul_left ↑a)).mul_left
    (cexp (-π * a ^ 2 * x))).congr_fun (fun n ↦ ?_)
  rw [jacobiTheta₂'_term, mul_assoc (2 * π * I), mul_div_cancel_left₀ _ two_pi_I_ne_zero, ← add_mul,
    mul_left_comm, jacobiTheta₂_term, ← Complex.exp_add]
  push_cast
  simp only [← mul_assoc, ← add_mul]
  congrm _ * cexp (?_ * x)
  simp only [mul_right_comm _ I, add_mul, mul_assoc _ I, I_mul_I]
  ring_nf

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

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ (completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)) / s.Gammaℝ =
    (completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)) / (↑π ^ (-s / 2) * Gamma (s / 2))

Tactic:
Gammaℝ

Goal state after:
s : ℂ
hs : s ≠ 0
⊢ (completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)) / (↑π ^ (-s / 2) * Gamma (s / 2)) =
    (completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)) / (↑π ^ (-s / 2) * Gamma (s / 2))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: 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)
⊢ HasSum (fun n ↦ if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (completedCosZeta (↑a) s)

Tactic:
refine hint.congr_fun fun n ↦ ?_

Goal state after:
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 : ℕ
⊢ (if n = 0 then 0 else 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.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s - 1 / (s - 1)) 1

Tactic:
simp_rw [completedHurwitzZetaEven_eq, sub_sub, add_assoc]

Goal state after:
a : UnitAddCircle
⊢ DifferentiableAt ℂ
    (fun s ↦ completedHurwitzZetaEven₀ a s - ((if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1)))) 1
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
⊢ FermatLastTheoremWith R n

Tactic:
intro a b c ha hb hc habc
  let s : Finset R := {a, b, c}; let d := s.gcd id
  obtain ⟨A, hA⟩ : d ∣ a := gcd_dvd (by simp [s])
  obtain ⟨B, hB⟩ : d ∣ b := gcd_dvd (by simp [s])
  obtain ⟨C, hC⟩ : d ∣ c := gcd_dvd (by simp [s])
  simp only [hA, hB, hC, mul_ne_zero_iff, mul_pow] at ha hb hc habc
  rw [← mul_add, mul_right_inj' (pow_ne_zero n ha.1)] at habc
  refine hn A B C ha.2 hb.2 hc.2 ?_ habc
  rw [← Finset.normalize_gcd, normalize_eq_one]
  refine isUnit_of_associated_mul ?_ ha.1
  grw [← Finset.gcd_mul_left', gcd_eq_gcd_image]
  refine .of_eq ?_; congr; simp [s, hA, hB, hC]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x : K
h2 : 1 + 1 = 2
⊢ (fun p ↦ (↑p).1 / ((↑p).2 + 1)) ((fun x ↦ ⟨(2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2)), ⋯⟩) x) = x

Tactic:
have h3 : (2 : K) ≠ 0 := by
      convert! hk 1
      rw [one_pow 2, h2]

Goal state after:
K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x : K
h2 : 1 + 1 = 2
h3 : 2 ≠ 0
⊢ (fun p ↦ (↑p).1 / ((↑p).2 + 1)) ((fun x ↦ ⟨(2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2)), ⋯⟩) x) = x
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 = 0
hw1 : w = -1
⊢ v = 0

Tactic:
exact eq_zero_of_pow_eq_zero hq

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

Goal state before:
pp: case s.p
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
x✝ : K →+* ℂ
| x✝ = w.embedding ∨ star x✝ = w.embedding

pp: case s.s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.univ

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ DecidablePred ?m.24

Tactic:
star_involutive.eq_iff

Goal state after:
case s.p
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
x✝ : K →+* ℂ
| x✝ = w.embedding ∨ x✝ = star w.embedding

case s.s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.univ

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ DecidablePred ?m.24
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
h : 1 ≤ w ↑x
⊢ w = mk ψ.toRingHom

Tactic:
simp only [RingHom.toRatAlgHom_apply] at hψ

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding ↑x = ψ ↑x
h : 1 ≤ w ↑x
⊢ w = mk ψ.toRingHom
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ∈ CommGroup.torsion (𝓞 K)ˣ
⊢ ζ ^ torsionOrder K = 1

Tactic:
exact Subtype.ext_iff.mp (@pow_card_eq_one' (torsion K) _ ⟨ζ, h⟩)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : finrank ℚ K = 1
⊢ nrRealPlaces K = 1

Tactic:
have := card_add_two_mul_card_eq_rank K

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : finrank ℚ K = 1
this : nrRealPlaces K + 2 * nrComplexPlaces K = finrank ℚ K
⊢ nrRealPlaces K = 1
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
chn0 : ringChar k ≠ 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
⊢ d + 1 = 0

Tactic:
| hi d ih_d =>

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
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
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
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
⊢ a.natDegree = 0

Tactic:
by
  rcases eq_or_ne (ringChar k) 0 with ch0 | chn0
  -- characteristic zero
  · obtain ⟨da, -, -⟩ := flt_catalan_deriv
      hp hq hr hineq chp chq chr ha hb hc hab hu hv hw heq
    have czk : CharZero k := by
      apply charZero_of_inj_zero
      intro n
      rw [ringChar.spec, ch0]
      exact zero_dvd_iff.mp
    rw [eq_C_of_derivative_eq_zero da]
    exact natDegree_C _
  -- characteristic p > 0
  · generalize eq_d : a.natDegree = d
    -- set up infinite descent
    -- strong induct on `d := a.natDegree`
    induction d
      using Nat.case_strong_induction_on
      generalizing a b c ha hb hc hab heq with
    | hz => rfl
    | hi d ih_d => -- have derivatives of `a, b, c` zero
      obtain ⟨ad, bd, cd⟩ := flt_catalan_deriv
        hp hq hr hineq chp chq chr ha hb hc hab hu hv hw heq
      -- find contracts `ca, cb, cc` so that `a(k) = ca(k^ch)`
      obtain ⟨ca, ca_nz, eq_a, eq_deg_a⟩ := find_contract ha ad chn0
      obtain ⟨cb, cb_nz, eq_b, eq_deg_b⟩ := find_contract hb bd chn0
      obtain ⟨cc, cc_nz, eq_c, eq_deg_c⟩ := find_contract hc cd chn0
      set ch := ringChar k
      suffices hca : ca.natDegree = 0 by
        rw [← eq_d, eq_deg_a, hca, zero_mul]
      by_contra hnca; apply hnca
      apply ih_d _ _ _ ca_nz cb_nz cc_nz <;> clear ih_d <;> try rfl
      · apply (isCoprime_expand chn0).mp
        rwa [← eq_a, ← eq_b]
      · have _ : ch ≠ 1 := CharP.ringChar_ne_one
        have hch2 : 2 ≤ ch := by lia
        rw [← add_le_add_iff_right 1, ← eq_d, eq_deg_a]
        grw [← hch2]
        lia
      · rw [eq_a, eq_b, eq_c, ← expand_C ch u, ← expand_C ch v, ← expand_C ch w] at heq
        simp_rw [← map_pow, ← map_mul, ← map_add] at heq
        rwa [Polynomial.expand_eq_zero (zero_lt_iff.mpr chn0)] at heq

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

Goal state before:
pp: case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : ¬w₁ = w₂
⊢ w₁.embedding ≠ conjugate w₂.embedding

Tactic:
· contrapose h_eq
    rw [← mk_embedding w₁, h_eq, mk_conjugate_eq, mk_embedding]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : mixedSpace K
⊢ (∃ w, (normAtPlace w) x ≠ 0) ↔ x ≠ 0

Tactic:
by
  rw [ne_eq, ← forall_normAtPlace_eq_zero_iff, not_forall]

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

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = Nat.card ↑{1}

Tactic:
congr with x

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ
x : Gal(K/k)
⊢ x ∈ ↑(Stab (mk w.embedding)) ↔ x ∈ {1}
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
hv : ¬ComplexEmbedding.IsReal v.embedding
⊢ ¬ComplexEmbedding.IsReal w.embedding

Tactic:
ComplexEmbedding.isReal_iff,

Goal state after:
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
hv : ¬conjugate v.embedding = v.embedding
⊢ ¬conjugate w.embedding = w.embedding
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
⊢ (unramifiedPlacesOver L v).ncard = (unmixedEmbeddingsOver L v.embedding).ncard

Tactic:
rw [(bijOn_extensionIte L v).ncard_eq]

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)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K

Tactic:
have hB : 0 ≤ B := by
    contrapose! h
    rw [convexBodySum_volume_eq_zero_of_le_zero K (le_of_lt h)]
    exact minkowskiBound_pos K I

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Group G
inst✝¹⁰ : MulSemiringAction G S
inst✝⁹ : IsGaloisGroup G R S
inst✝⁸ : Finite G
inst✝⁷ : IsDomain R
inst✝⁶ : IsDomain S
inst✝⁵ : Module.Finite R S
inst✝⁴ : Flat R S
p : Ideal R
P : Ideal S
inst✝³ : P.LiesOver p
inst✝² : p.IsPrime
inst✝¹ : P.IsPrime
inst✝ : PerfectField p.ResidueField
H :
  (p.primesOver S).ncard * (Nat.card ↥(inertia G P) * p.inertiaDegIn S) =
    (p.primesOver S).ncard * (p.ramificationIdxIn S * p.inertiaDegIn S)
h1 : (p.primesOver S).ncard ≠ 0
h2 : p.inertiaDegIn S ≠ 0
⊢ Nat.card ↥(inertia G P) = p.ramificationIdxIn S

Tactic:
mul_right_inj' h1,

Goal state after:
R : Type u_1
S : Type u_2
G : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Group G
inst✝¹⁰ : MulSemiringAction G S
inst✝⁹ : IsGaloisGroup G R S
inst✝⁸ : Finite G
inst✝⁷ : IsDomain R
inst✝⁶ : IsDomain S
inst✝⁵ : Module.Finite R S
inst✝⁴ : Flat R S
p : Ideal R
P : Ideal S
inst✝³ : P.LiesOver p
inst✝² : p.IsPrime
inst✝¹ : P.IsPrime
inst✝ : PerfectField p.ResidueField
H : Nat.card ↥(inertia G P) * p.inertiaDegIn S = p.ramificationIdxIn S * p.inertiaDegIn S
h1 : (p.primesOver S).ncard ≠ 0
h2 : p.inertiaDegIn S ≠ 0
⊢ Nat.card ↥(inertia G P) = p.ramificationIdxIn S