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

Goal state before:
pp: α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i ↦ fl i v) ∈ S}
v : α → ℕ
x : Fin2 (n + 1)
⊢ (f v :: fun i ↦ fl i v) x = (f :: fl) x v

Tactic:
obtain _ | _ | _ := x

Goal state after:
case fz
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i ↦ fl i v) ∈ S}
v : α → ℕ
⊢ (f v :: fun i ↦ fl i v) fz = (f :: fl) fz v

case fs.fz
α : Type
f✝ : (α → ℕ) → ℕ
df : DiophFn f✝
v : α → ℕ
n✝ : ℕ
S : Set (α ⊕ Fin2 (n✝ + 1).succ → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) (n✝ + 1).succ
fl : Vector3 ((α → ℕ) → ℕ) (n✝ + 1)
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f✝ (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f✝ v :: fun i ↦ fl i v) ∈ S}
⊢ (f✝ v :: fun i ↦ fl i v) fz.fs = (f✝ :: fl) fz.fs v

case fs.fs
α : Type
f✝ : (α → ℕ) → ℕ
df : DiophFn f✝
v : α → ℕ
n✝ : ℕ
a✝ : Fin2 n✝
S : Set (α ⊕ Fin2 (n✝ + 1).succ → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) (n✝ + 1).succ
fl : Vector3 ((α → ℕ) → ℕ) (n✝ + 1)
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f✝ (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f✝ v :: fun i ↦ fl i v) ∈ S}
⊢ (f✝ v :: fun i ↦ fl i v) a✝.fs.fs = (f✝ :: fl) a✝.fs.fs v
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case right
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ (List.filter (fun x ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m

Tactic:
· conv_rhs => rw [← prod_primeFactorsList hm₀]
      refine prod_eq <|
        (filter _ <| perm_primeFactorsList_mul (pow_ne_zero e hp.ne_zero) hm₀).trans ?_
      rw [filter_append, hp.primeFactorsList_pow, filter_eq_nil_iff.mpr <| by grind, nil_append,
        filter_eq_self.mpr <| by grind]

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v

Tactic:
rw [← one_div, lt_div_iff₀ (mul_pos hv₀ hv₀'), ← abs_of_pos (mul_pos hv₀ hv₀'), ← abs_mul,
    sub_mul, ← mul_assoc, ← mul_assoc, div_mul_cancel₀ _ hv₀.ne', abs_sub_comm, abs_lt,
    lt_sub_iff_add_lt, sub_lt_iff_lt_add, mul_assoc] at h

Goal state after:
ξ : ℝ
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
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k m : ℕ
⊢ (m < N + 1 ∧ m ≠ 0 ∧ ∃ x ≤ m, Prime x ∧ x ∣ m ∧ k ≤ x) ↔
    ∃ a, ((a < N + 1 ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N + 1 ∧ m ≠ 0 ∧ a ∣ m

Tactic:
← exists_and_left,

Goal state after:
N k m : ℕ
⊢ (∃ x, m < N + 1 ∧ m ≠ 0 ∧ x ≤ m ∧ Prime x ∧ x ∣ m ∧ k ≤ x) ↔
    ∃ a, ((a < N + 1 ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N + 1 ∧ m ≠ 0 ∧ a ∣ m
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedDivisionRing F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
p : ℕ
hp : 1 < p
⊢ Summable fun n ↦ f p ^ n

Tactic:
← map_pow

Goal state after:
F : Type u_1
inst✝¹ : NormedDivisionRing F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
p : ℕ
hp : 1 < p
⊢ Summable fun n ↦ f (p ^ n)
Module: Mathlib.NumberTheory.LSeries.Convolution

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2

Tactic:
by
  rcases eq_or_ne n 0 with rfl | hn
  · simp
  -- now `n ≠ 0`
  rw [term_of_ne_zero hn, convolution_def, Finset.sum_div]
  refine Finset.sum_congr rfl fun p hp ↦ ?_
  have ⟨hp₁, hp₂⟩ := ne_zero_of_mem_divisorsAntidiagonal hp
  rw [term_of_ne_zero hp₁, term_of_ne_zero hp₂, mul_comm_div, div_div, ← mul_div_assoc,
    ← natCast_mul_natCast_cpow, ← cast_mul, mul_comm p.2, (mem_divisorsAntidiagonal.mp hp).1]

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

Goal state before:
pp: a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
⊢ 0 ≤ term (logMul^[n] a) (↑x) k

Tactic:
rw [LSeries.term_def]

Goal state after:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
⊢ 0 ≤ if k = 0 then 0 else logMul^[n] a k / ↑k ^ ↑x
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: n : ℤ
z τ : ℂ
f : ℂ × ℂ → ℂ := fun p ↦ 2 * ↑π * I * ↑n * p.1 + ↑π * I * ↑n ^ 2 * p.2
⊢ HasFDerivAt (fun p ↦ jacobiTheta₂_term n p.1 p.2) (jacobiTheta₂_term_fderiv n z τ) (z, τ)

Tactic:
suffices HasFDerivAt f ((2 * π * I * n) • (ContinuousLinearMap.fst ℂ ℂ ℂ)
    + (π * I * n ^ 2) • (ContinuousLinearMap.snd ℂ ℂ ℂ)) (z, τ) from this.cexp

Goal state after:
n : ℤ
z τ : ℂ
f : ℂ × ℂ → ℂ := fun p ↦ 2 * ↑π * I * ↑n * p.1 + ↑π * I * ↑n ^ 2 * p.2
⊢ HasFDerivAt f ((2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ + (↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ)
    (z, τ)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
step1 : mellin (fun t ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t ↦ ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t ↦ P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (↑P.k - s - 1) • P.f t = (↑t ^ (↑P.k - s - 1) * (P.ε * (↑t ^ (-↑P.k) * (P.ε⁻¹ * ↑(t ^ P.k))))) • P.f t

Tactic:
rw [cpow_neg, ofReal_cpow (le_of_lt ht)]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
step1 : mellin (fun t ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t ↦ ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t ↦ P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (↑P.k - s - 1) • P.f t = (↑t ^ (↑P.k - s - 1) * (P.ε * ((↑t ^ ↑P.k)⁻¹ * (P.ε⁻¹ * ↑t ^ ↑P.k)))) • P.f t
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

Tactic:
· rw [mul_rpow pi_pos.le h.le, ← div_div, rpow_neg pi_pos.le, ← div_eq_inv_mul]

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

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n ↦ 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
⊢ Summable fun n ↦ f n (z, τ)

Tactic:
refine (summable_pow_mul_jacobiTheta₂_term_bound S hT 0).of_norm_bounded ?_

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n ↦ 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
⊢ ∀ (i : ℤ), ‖f i (z, τ)‖ ≤ ↑|i| ^ 0 * rexp (-π * (T * ↑i ^ 2 - 2 * S * ↑|i|))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case H
a' : ℝ
⊢ ContinuousOn (cosKernel ↑a') (Ioi 0)

Tactic:
apply continuous_re.comp_continuousOn (f := fun x ↦ (cosKernel a' x : ℂ))

Goal state after:
case H
a' : ℝ
⊢ ContinuousOn (fun x ↦ ↑(cosKernel (↑a') x)) (Ioi 0)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) =O[atTop] fun x ↦ rexp (-v * x)
| (fun x ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) =O[atTop] fun x ↦ rexp (-v * x)

Tactic:
enter [2, x]

Goal state after:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) =O[atTop] fun x ↦ rexp (-v * x)
x : ℝ
| ‖evenKernel a x - if a = 0 then 1 else 0‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ deriv (fun x ↦ jacobiTheta₂ x τ) z =
    deriv (fun z ↦ 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z

Tactic:
by
    rw [funext (jacobiTheta₂_functional_equation · τ)]

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

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ 2 * riemannZeta ↑k = (↑0 ^ k)⁻¹ + 2 • ∑' (n : ℕ+), (↑↑↑n ^ k)⁻¹

pp: case hf
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ Function.Even fun n ↦ (↑n ^ k)⁻¹

pp: case hf2
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ Summable fun n ↦ (↑n ^ k)⁻¹

Tactic:
· have h0 : (0 ^ k : ℂ)⁻¹ = 0 := by simp; lia
    norm_cast
    simp [h0, zeta_eq_tsum_one_div_nat_add_one_cpow (s := k) (by simp [hkk]),
      tsum_pnat_eq_tsum_succ (f := fun n => ((n : ℂ) ^ k)⁻¹)]

Goal state after:
case hf
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ Function.Even fun n ↦ (↑n ^ k)⁻¹

case hf2
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ Summable fun n ↦ (↑n ^ k)⁻¹
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: case inl
χ : DirichletCharacter ℂ 0
⊢ 0 = if False then 1 else 0

Tactic:
if_false

Goal state after:
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: case neg
r : ℝ
h : ¬r < -1
H : Summable fun p ↦ ↑↑p ^ r
p : Primes
⊢ 1 / ↑↑p ≤ ↑↑p ^ r

Tactic:
rw [one_div, ← Real.rpow_neg_one]

Goal state after:
case neg
r : ℝ
h : ¬r < -1
H : Summable fun p ↦ ↑↑p ^ r
p : Primes
⊢ ↑↑p ^ (-1) ≤ ↑↑p ^ r
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
n✝ : ℕ
χ : DirichletCharacter ℂ n✝
hs : s ≠ 0
m n : ℕ
⊢ χ ↑(m * n) * ↑↑(m * n) ^ (-s) = χ ↑m * ↑↑m ^ (-s) * (χ ↑n * ↑↑n ^ (-s))

Tactic:
simpa only [Nat.cast_mul, IsUnit.mul_iff, not_and, map_mul, ofReal_mul,
      mul_cpow_ofReal_nonneg m.cast_nonneg n.cast_nonneg _]
      using mul_mul_mul_comm ..

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ ↑(x.gcd y) ∣ z

Tactic:
obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0

Goal state after:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ ↑(x.gcd y) ∣ z
Module: Mathlib.NumberTheory.FLT.Four

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

Tactic:
by
  apply IsCoprime.mul_right (Int.isCoprime_of_sq_sum (isCoprime_comm.mp h))
  rw [add_comm]; apply Int.isCoprime_of_sq_sum h

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ PythagoreanTriple (x / ↑(x.gcd y)) (y / ↑(x.gcd y)) (z / ↑(x.gcd y))

Tactic:
obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0

Goal state after:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ PythagoreanTriple (x / ↑(x.gcd y)) (y / ↑(x.gcd y)) (z / ↑(x.gcd y))
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
⊢ IsCoprime (a ^ 2) n

Tactic:
ht1,

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
⊢ IsCoprime (m ^ 2 - n ^ 2) n
Module: Mathlib.NumberTheory.PythagoreanTriples

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

Tactic:
have h2 : (1 + 1 : K) = 2 := by norm_num

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
n : ℕ
hn : 1 < n
this : 0 < Real.log ↑n
⊢ (-s).re ≠ 0

Tactic:
by simp; grind

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

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ 1 < (↑s).re

Tactic:
by simpa using hs

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

Goal state before:
pp: case a
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
p : M
ha : radical a ∣ p ^ n
⊢ (↑(primeFactors a)).Pairwise (Function.onFun IsRelPrime id)

Tactic:
exact pairwise_primeFactors_isRelPrime

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : radical a = radical b
⊢ primeFactors a = primeFactors b

Tactic:
by rw [← primeFactors_radical, h]; exact primeFactors_radical

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
x✝ : a = 0 ∨ IsUnit a
⊢ a = 0 → radical a = 1

Tactic:
by simp +contextual

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Norm

Goal state before:
pp: L : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
F : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Algebra K F
inst✝³ : FiniteDimensional K F
inst✝² : Algebra F L
inst✝¹ : FiniteDimensional F L
inst✝ : IsScalarTower K F L
x : 𝓞 L
⊢ (Algebra.norm K) ((Algebra.norm F) ↑x) = (Algebra.norm K) ↑x

Tactic:
Algebra.norm_norm

Goal state after:
L : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
F : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Algebra K F
inst✝³ : FiniteDimensional K F
inst✝² : Algebra F L
inst✝¹ : FiniteDimensional F L
inst✝ : IsScalarTower K F L
x : 𝓞 L
⊢ (Algebra.norm K) ↑x = (Algebra.norm K) ↑x
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ 1 / 1 = 1

Tactic:
one_div_one

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ 1 = 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ h.IsClassified

Tactic:
obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0

Goal state after:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ h.IsClassified
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
⊢ ¬ComplexEmbedding.IsReal w.embedding

Tactic:
← isReal_iff

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
⊢ ¬w.IsReal
Module: Mathlib.NumberTheory.NumberField.Units.Basic

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

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

Goal state after:
x : 𝓞 ℚ
⊢ ↑x = ↑1 ∨ ↑x = ↑(-1) ↔ ↑x = 1 ∨ ↑x = -1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inr
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
⊢ (k * (2 * m * n) = k * (m ^ 2 - n ^ 2) ∧ k * (m ^ 2 - n ^ 2) = k * (2 * m * n) ∨
      k * (2 * m * n) = k * (2 * m * n) ∧ k * (m ^ 2 - n ^ 2) = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Tactic:
refine ⟨Or.inr ⟨rfl, rfl⟩, ?_⟩

Goal state after:
case h.inr
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
⊢ z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2)
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 ↑x = ψ ↑x
h : 1 ≤ w ↑x
⊢ w = mk ψ.toRingHom

Tactic:
rw [← norm_embedding_eq, hψ] 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 ≤ ‖ψ ↑x‖
⊢ w = mk ψ.toRingHom
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : K
⊢ (((RingHom.pi fun w ↦ embedding_of_isReal ⋯) x ∈ Set.univ.pi fun w ↦ ball 0 ↑(f ↑w)) ∧
      (RingHom.pi fun w ↦ (↑w).embedding) x ∈ Set.univ.pi fun w ↦ ball 0 ↑(f ↑w)) ↔
    ∀ (w : InfinitePlace K), w x < ↑(f w)

Tactic:
Set.mem_pi,

Goal state after:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : K
⊢ ((∀ i ∈ Set.univ, (RingHom.pi fun w ↦ embedding_of_isReal ⋯) x i ∈ ball 0 ↑(f ↑i)) ∧
      ∀ i ∈ Set.univ, (RingHom.pi fun w ↦ (↑w).embedding) x i ∈ ball 0 ↑(f ↑i)) ↔
    ∀ (w : InfinitePlace K), w x < ↑(f w)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : K
⊢ ((∀ (i : { w // w.IsReal }), (RingHom.pi fun w ↦ embedding_of_isReal ⋯) x i ∈ ball 0 ↑(f ↑i)) ∧
      ∀ (i : { w // w.IsComplex }), (RingHom.pi fun w ↦ (↑w).embedding) x i ∈ ball 0 ↑(f ↑i)) ↔
    ∀ (w : InfinitePlace K), w x < ↑(f w)

Tactic:
mem_ball_zero_iff,

Goal state after:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : K
⊢ ((∀ (i : { w // w.IsReal }), ‖(RingHom.pi fun w ↦ embedding_of_isReal ⋯) x i‖ < ↑(f ↑i)) ∧
      ∀ (i : { w // w.IsComplex }), ‖(RingHom.pi fun w ↦ (↑w).embedding) x i‖ < ↑(f ↑i)) ↔
    ∀ (w : InfinitePlace K), w x < ↑(f w)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:

Tactic:
_ = (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (2 * (f x.val))) *
          ∏ x : {w // InfinitePlace.IsComplex w}, ENNReal.ofReal (f x.val) ^ 2 * NNReal.pi := by
      simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball, Complex.volume_ball]
    _ = ((2 : ℝ≥0) ^ nrRealPlaces K
          * (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val)))
          * ((∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2) *
            NNReal.pi ^ nrComplexPlaces K) := by
      simp_rw [ofReal_mul (by simp : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
        Finset.card_univ, ofReal_ofNat, ofReal_coe_nnreal, coe_ofNat]
    _ = (convexBodyLTFactor K) * ((∏ x : {w // InfinitePlace.IsReal w}, .ofReal (f x.val)) *
        (∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2)) := by
      simp_rw [convexBodyLTFactor, coe_mul, ENNReal.coe_pow]
      ring
    _ = (convexBodyLTFactor K) * ∏ w, (f w) ^ (mult w) := by
      simp_rw [prod_eq_prod_mul_prod, coe_mul, ofNNReal_finsetProd, mult_isReal, mult_isComplex,
        pow_one, ENNReal.coe_pow, ofReal_coe_nnreal]

Goal state after:
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
⊢ (((RingHom.pi fun w ↦ embedding_of_isReal ⋯) x ∈ Set.univ.pi fun w ↦ ball 0 ↑(f ↑w)) ∧
      (RingHom.pi fun w ↦ (↑w).embedding) x ∈
        Set.univ.pi fun w ↦ if w = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑w) ^ 2} else ball 0 ↑(f ↑w)) ↔
    (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
      |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2

Tactic:
Set.mem_pi,

Goal state after:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
⊢ ((∀ i ∈ Set.univ, (RingHom.pi fun w ↦ embedding_of_isReal ⋯) x i ∈ ball 0 ↑(f ↑i)) ∧
      ∀ i ∈ Set.univ,
        (RingHom.pi fun w ↦ (↑w).embedding) x i ∈
          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
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 }), (embedding_of_isReal ⋯) x ∈ ball 0 ↑(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:
mem_ball_zero_iff,

Goal state after:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
⊢ ((∀ (i : { w // w.IsReal }), ‖(embedding_of_isReal ⋯) 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