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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ ∫ (x : ℝ) in Ioi 0,
      ↑x ^ (s - 1) •
        ((Ioo 0 1).indicator (fun t ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x) =
    ∫ (x : ℝ) in Ioi 0, ↑x ^ (s - 1) • (Ioo 0 1).indicator (fun t ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x

Tactic:
refine setIntegral_congr_ae measurableSet_Ioi (eventually_of_mem (U := {1}ᶜ)
        (compl_mem_ae_iff.mpr (subsingleton_singleton.measure_zero _)) (fun x hx _ ↦ ?_))

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
x : ℝ
hx : x ∈ {1}ᶜ
x✝ : x ∈ Ioi 0
⊢ ↑x ^ (s - 1) •
      ((Ioo 0 1).indicator (fun t ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x) =
    ↑x ^ (s - 1) • (Ioo 0 1).indicator (fun t ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂' z τ = 0

Tactic:
apply tsum_eq_zero_of_not_summable
  rw [summable_jacobiTheta₂'_term_iff]
  exact not_lt.mpr hτ

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
x : ℝ
x✝ : x ∈ Ioc 0 1
hx : 0 < x
right✝ : x ≤ 1
⊢ ↑x ^ (s - 1) • (P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) = ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀

Tactic:
ofReal_cpow hx.le,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
x : ℝ
x✝ : x ∈ Ioc 0 1
hx : 0 < x
right✝ : x ≤ 1
⊢ ↑x ^ (s - 1) • (P.f₀ - (P.ε * ↑x ^ ↑(-P.k)) • P.g₀) = ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1)) • P.f₀ - P.ε • (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - ↑P.k - 1)) • P.g₀ =
    (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀

Tactic:
simp_rw [← intervalIntegral.integral_of_le zero_le_one]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ (∫ (x : ℝ) in 0..1, ↑x ^ (s - 1)) • P.f₀ - P.ε • (∫ (x : ℝ) in 0..1, ↑x ^ (s - ↑P.k - 1)) • P.g₀ =
    (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀
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
⊢ 1 / ↑x ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))

Tactic:
ofReal_cpow hx.le,

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
⊢ 1 / ↑x ^ (1 / 2) = 1 / ↑x ^ ↑(1 / 2)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ (s - ↑P.k) • P.Λ₀ s) (𝓝 ↑P.k) (𝓝 0)

Tactic:
rw [(by simp : 𝓝 0 = 𝓝 ((P.k - P.k : ℂ) • P.Λ₀ P.k))]

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ (s - ↑P.k) • P.Λ₀ s) (𝓝 ↑P.k) (𝓝 ((↑P.k - ↑P.k) • P.Λ₀ ↑P.k))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: z τ : ℂ
⊢ jacobiTheta₂'' (-z) τ = -jacobiTheta₂'' z τ

Tactic:
simp [jacobiTheta₂'', jacobiTheta₂'_neg_left, neg_div, -neg_add_rev, ← neg_add]

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 * ↑π / (-I * (I * ↑(1 / x))) ^ (3 / 2) * jacobiTheta₂'' (↑a) (I * ↑x) / (-2 * ↑π))

Tactic:
h2

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 ≠ π
⊢ jacobiTheta₂'' (↑a) (I * ↑x) =
    ↑(1 / x ^ (3 / 2)) * (-2 * ↑π / (1 / ↑x) ^ (3 / 2) * jacobiTheta₂'' (↑a) (I * ↑x) / (-2 * ↑π))
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 ≠ π
J : ℂ
⊢ J = (↑(x ^ (3 / 2)))⁻¹ * (-2 * ↑π * ↑x ^ (3 / 2) * J / (-2 * ↑π))

Tactic:
ofReal_cpow hx.le,

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ if n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) ((↑(cosKernel (↑a) t) - 1) / 2)

Tactic:
refine ((hasSum_int_cosKernel₀ a ht).div_const 2).congr_fun fun n ↦ ?_

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
t : ℝ
ht : 0 < t
n : ℤ
⊢ (if n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) =
    (if n = 0 then 0 else cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) / 2
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
n : ℕ
⊢ term (fun n ↦ if n = 0 then 0 else 1) s n = 1 / ↑n ^ s

Tactic:
rcases eq_or_ne n 0 with hn | hn <;>
  simp [hn, ne_zero_of_one_lt_re hs]

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

Goal state before:
pp: case refine_2
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ),
    0 < t →
      HasSum (fun n ↦ if ↑n + a = 0 then 0 else 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t)))
        ((↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2)
n : ℤ
⊢ s.Gammaℝ / ↑|↑n + a| ^ s / 2 = s.Gammaℝ / 2 / ↑|↑n + a| ^ s

Tactic:
div_right_comm

Goal state after:
case refine_2
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ),
    0 < t →
      HasSum (fun n ↦ if ↑n + a = 0 then 0 else 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t)))
        ((↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2)
n : ℤ
⊢ s.Gammaℝ / 2 / ↑|↑n + a| ^ s = s.Gammaℝ / 2 / ↑|↑n + a| ^ s
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case 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 : Even n
⊢ False

Tactic:
refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)

Goal state after:
case 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 : Even n
⊢ ↑(a.natAbs ^ n + b.natAbs ^ n) = ↑(c.natAbs ^ n)
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.inl.inl.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 : b < 0
hc : c < 0
⊢ False

Tactic:
refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)

Goal state after:
case inr.inl.inl.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 : b < 0
hc : c < 0
⊢ ↑(a.natAbs ^ n + b.natAbs ^ n) = ↑(c.natAbs ^ n)
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.inr.inr.inr
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 : 0 < a
hb : 0 < b
hc : 0 < c
⊢ False

Tactic:
refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)

Goal state after:
case inr.inr.inr.inr
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 : 0 < a
hb : 0 < b
hc : 0 < c
⊢ ↑(a.natAbs ^ n + b.natAbs ^ n) = ↑(c.natAbs ^ n)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun i ↦ 1 / 2 / |↑i| ^ s.re

Tactic:
div_right_comm

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun i ↦ 1 / |↑i| ^ s.re / 2
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case neg
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
ha : a ^ n = 1 ∨ a ^ n = -1
hb : b ^ n = 1 ∨ b ^ n = -1
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rcases ha with ha | ha <;> rcases hb with hb | hb <;> rcases hc with hc | hc

Goal state after:
case neg.inl.inl.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = 1
hc : c ^ n = 1
⊢ a ^ n + b ^ n ≠ c ^ n

case neg.inl.inl.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = 1
hc : c ^ n = -1
⊢ a ^ n + b ^ n ≠ c ^ n

case neg.inl.inr.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
hc : c ^ n = 1
⊢ a ^ n + b ^ n ≠ c ^ n

case neg.inl.inr.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
hc : c ^ n = -1
⊢ a ^ n + b ^ n ≠ c ^ n

case neg.inr.inl.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
hc : c ^ n = 1
⊢ a ^ n + b ^ n ≠ c ^ n

case neg.inr.inl.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
hc : c ^ n = -1
⊢ a ^ n + b ^ n ≠ c ^ n

case neg.inr.inr.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = -1
hc : c ^ n = 1
⊢ a ^ n + b ^ n ≠ c ^ n

case neg.inr.inr.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = -1
hc : c ^ n = -1
⊢ a ^ n + b ^ n ≠ c ^ n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: 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 : ℕ
⊢ (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s =
    ((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

Tactic:
div_right_comm

Goal state after:
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 : ℕ
⊢ (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s =
    ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) +
          (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) /
        2 /
      ↑n ^ s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
rw [cosZeta, Function.update_of_ne, div_eq_mul_inv]

Goal state after:
case h
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
⊢ 1 - s ≠ 0
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Fermat42 a b c
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1

Tactic:
by
  obtain ⟨a0, b0, c0, hf⟩ := exists_minimal h
  rcases Int.emod_two_eq_zero_or_one a0 with hap | hap
  · rcases Int.emod_two_eq_zero_or_one b0 with hbp | hbp
    · exfalso
      have h1 : 2 ∣ (Int.gcd a0 b0 : ℤ) :=
        Int.dvd_coe_gcd (Int.dvd_of_emod_eq_zero hap) (Int.dvd_of_emod_eq_zero hbp)
      rw [Int.isCoprime_iff_gcd_eq_one.mp (coprime_of_minimal hf)] at h1
      revert h1
      decide
    · exact ⟨b0, ⟨a0, ⟨c0, minimal_comm hf, hbp⟩⟩⟩
  exact ⟨a0, ⟨b0, ⟨c0, hf, hap⟩⟩⟩

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

Goal state before:
pp: case inl
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb✝ : 0 ≤ b
hb : 0 < ↑n + b
⊢ ↑(SignType.sign (↑n + b)) / ↑(↑n + b) ^ s = 1 / ↑(↑n + b) ^ s

pp: case inr
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb✝ : 0 ≤ b
hb : 0 = ↑n + b
⊢ ↑(SignType.sign (↑n + b)) / ↑(↑n + b) ^ s = 1 / ↑(↑n + b) ^ s

Tactic:
· simp [sign_pos hb]

Goal state after:
case inr
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb✝ : 0 ≤ b
hb : 0 = ↑n + b
⊢ ↑(SignType.sign (↑n + b)) / ↑(↑n + b) ^ s = 1 / ↑(↑n + b) ^ s
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
⊢ 2 = 1 + 1

Tactic:
h2

Goal state after:
K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x : K
h2 : 1 + 1 = 2
⊢ 2 = 2
Module: Mathlib.NumberTheory.PythagoreanTriples

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

Tactic:
have h4 : (2 : K) ≠ 0 := by
      convert! hk 1
      rw [one_pow 2]
      ring

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

Goal state after:
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 : ↑2 ∣ 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
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inr.inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
ha : a ≠ 0
hb : b ≠ 0
⊢ primeFactors (a * b) = primeFactors a ∪ primeFactors b

Tactic:
primeFactors_mul_eq_union ha hb

Goal state after:
case inr.inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
ha : a ≠ 0
hb : b ≠ 0
⊢ primeFactors a ∪ primeFactors b = primeFactors a ∪ primeFactors b
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
adr_dvd_w : divRadical a ∣ w
bdr_dvd_w : divRadical b ∣ w
cdr_dvd_w : divRadical c ∣ b.wronskian c
⊢ divRadical (a * b * c) ∣ w

Tactic:
← wbc

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
adr_dvd_w : divRadical a ∣ w
bdr_dvd_w : divRadical b ∣ w
cdr_dvd_w : divRadical c ∣ w
⊢ divRadical (a * b * c) ∣ w
Module: Mathlib.NumberTheory.NumberField.Norm

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
F : Type u_3
inst✝³ : Field F
inst✝² : Algebra K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Tactic:
let L := normalClosure K F (AlgebraicClosure F)

Goal state after:
K : Type u_2
inst✝⁴ : Field K
F : Type u_3
inst✝³ : Field F
inst✝² : Algebra K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
⊢ IsUnit ((norm K) x) ↔ IsUnit x
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
ch0 : ringChar k = 0
da : derivative a = 0
n : ℕ
⊢ ↑n = 0 → n = 0

Tactic:
rw [ringChar.spec, ch0]

Goal state after:
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
ch0 : ringChar k = 0
da : derivative a = 0
n : ℕ
⊢ 0 ∣ n → n = 0
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
⊢ S ≠ 0

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₁.mult ≠ 0

Tactic:
· rw [Finset.prod_ne_zero_iff]
      exact fun w hw => pow_ne_zero _ (hf w (Finset.ne_of_mem_erase hw))

Goal state after:
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₁.mult ≠ 0
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
w : InfinitePlace ↥(maximalRealSubfield K)
⊢ w.IsReal

Tactic:
rw [InfinitePlace.isReal_iff, ComplexEmbedding.isReal_iff]

Goal state after:
F : Type u_1
inst✝³ : Field F
K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
w : InfinitePlace ↥(maximalRealSubfield K)
⊢ conjugate w.embedding = w.embedding
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 : InfinitePlace K
h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2

Tactic:
· left
    trans Nat.card ({1} : Set Gal(K/k))
    · congr with x
      simp only [SetLike.mem_coe, mem_stabilizer_mk_iff, Set.mem_singleton_iff, or_iff_left_iff_imp,
        h x, IsEmpty.forall_iff]
    · simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ∫ (x : mixedSpace K), rexp (-∑ w, ‖x.1 w‖ + -(2 * ∑ w, ‖x.2 w‖)) =
    (∫ (x : { w // w.IsReal } → ℝ), ∏ w, rexp (-‖x w‖)) * ∫ (x : { w // w.IsComplex } → ℂ), ∏ w, rexp (-2 * ‖x w‖)

Tactic:
← neg_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ∫ (x : mixedSpace K), rexp (-∑ w, ‖x.1 w‖ + -2 * ∑ w, ‖x.2 w‖) =
    (∫ (x : { w // w.IsReal } → ℝ), ∏ w, rexp (-‖x w‖)) * ∫ (x : { w // w.IsComplex } → ℂ), ∏ w, rexp (-2 * ‖x w‖)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLTFactor K) *
      ↑((∏ x ∈ Finset.univ.erase w₀, (if x = w₀ then B else 1) ^ x.mult) * (if True then B else 1) ^ w₀.mult)

Tactic:
ite_pow,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLTFactor K) *
      ↑((∏ x ∈ Finset.univ.erase w₀, if x = w₀ then B ^ x.mult else 1 ^ x.mult) *
          if True then B ^ w₀.mult else 1 ^ w₀.mult)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLT'Factor K) *
      ↑((∏ x ∈ Finset.univ.erase w₀, (if x = w₀ then NNReal.sqrt B else 1) ^ x.mult) *
          (if True then NNReal.sqrt B else 1) ^ w₀.mult)

Tactic:
ite_pow,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLT'Factor K) *
      ↑((∏ x ∈ Finset.univ.erase w₀, if x = w₀ then NNReal.sqrt B ^ x.mult else 1 ^ x.mult) *
          if True then NNReal.sqrt B ^ w₀.mult else 1 ^ w₀.mult)
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 + (mixedEmbeddingsOver L v.embedding).ncard = Fintype.card (L →ₐ[K] ℂ)

Tactic:
unramifiedPlacesOver_ncard,

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
⊢ (unmixedEmbeddingsOver L v.embedding).ncard + (mixedEmbeddingsOver L v.embedding).ncard = Fintype.card (L →ₐ[K] ℂ)