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

Goal state before:
pp: n : ℤ
z τ : ℂ
⊢ 2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ = ↑(π * (2 * ↑n)) * z * I + ↑(π * ↑n ^ 2) * τ * I

Tactic:
by push_cast; ring

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

Goal state before:
pp: case hf
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun b ↦ ↑b * rexp (-π * (↑b + a ^ 2) * t)) (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2)

Tactic:
have h0' : ‖rexp (-π * t)‖ < 1 := by
      simpa only [norm_eq_abs, abs_exp] using exp_lt_aux ht

Goal state after:
case hf
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ HasSum (fun b ↦ ↑b * rexp (-π * (↑b + a ^ 2) * t)) (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ (fun b ↦ ↑b * rexp (-π * (↑b + a ^ 2) * t)) = fun i ↦ rexp (-π * a ^ 2 * t) * (↑i * rexp (-π * t) ^ i)

Tactic:
ext1 n
      rw [mul_comm (exp _), ← Real.exp_nat_mul, mul_assoc (n : ℝ), ← Real.exp_add]
      ring_nf

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

Goal state before:
pp: case inl
ι : 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 : a i = 0
⊢ a i / ↑(π * q i) ^ s = ↑π ^ (-s) * a i / ↑(q i) ^ s

Tactic:
simp [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
x : ℝ
hx : 0 < x
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) x + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x -
        P.f x +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x

Tactic:
rcases lt_trichotomy x 1 with hx' | rfl | hx'

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) x + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x -
        P.f x +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x

case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hx : 0 < 1
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) 1 + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) 1 -
        P.f 1 +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) 1 + {1}.indicator (fun x ↦ P.f₀ - P.f 1) 1

case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) x + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x -
        P.f x +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case inl
ι : 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 : a i = 0
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

Tactic:
simp [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
⊢ HasMellin (fun x ↦ P.f x - P.f₀) s (P.Λ s)

Tactic:
have hc1 : MellinConvergent (P.f · - P.f₀) s :=
    let ⟨_, ht⟩ := exists_gt s.re
    mellinConvergent_of_isBigO_rpow (P.hf_int.sub (locallyIntegrableOn_const _)) (P.hf_top _) ht
      P.hf_zero' hs

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
hc1 : MellinConvergent (fun x ↦ P.f x - P.f₀) s
⊢ HasMellin (fun x ↦ P.f x - P.f₀) s (P.Λ s)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
n : ℤ
⊢ ↑π * I * ↑n ^ 2 * 2 = ↑(n ^ 2) * (2 * ↑π * I)

Tactic:
by push_cast; ring

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

Goal state before:
pp: case pos
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
i : ι
t : ℝ
h : r i = 0
⊢ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = 0

Tactic:
simp [h]

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

Goal state before:
pp: case neg
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
i : ι
t : ℝ
h : ¬r i = 0
⊢ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))

Tactic:
simp [h]

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

Goal state before:
pp: z τ : ℂ
n : ℤ
⊢ jacobiTheta₂'_term n z (τ + 2) = jacobiTheta₂'_term n z τ

Tactic:
simp_rw [jacobiTheta₂'_term, jacobiTheta₂_term, Complex.exp_add]

Goal state after:
z τ : ℂ
n : ℤ
⊢ 2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * (τ + 2))) =
    2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ))
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
⊢ completedRiemannZeta s = ↑π ^ (-s / 2) * Gamma (s / 2) * ∑' (n : ℕ), 1 / ↑n ^ s

Tactic:
simp only [this, Gammaℝ_def, mul_zero, zero_mul, Real.cos_zero, ofReal_one, mul_one, mul_one_div,
    ← tsum_mul_left]

Goal state after:
s : ℂ
hs : 1 < s.re
this : completedRiemannZeta s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
⊢ (∑' (b : ℕ), if b = 0 then 0 else ↑π ^ (-s / 2) * Gamma (s / 2) / ↑b ^ s) =
    ∑' (x : ℕ), ↑π ^ (-s / 2) * Gamma (s / 2) / ↑x ^ s
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: x✝ : ℕ
⊢ 1 x✝ = δ x✝

Tactic:
simp [one_apply, LSeries.delta]

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

Goal state before:
pp: χ : DirichletCharacter ℂ 0
⊢ (fun n ↦ χ ↑n) = δ

Tactic:
by
  ext n
  rcases eq_or_ne n 0 with rfl | hn
  · simp_rw [cast_zero, χ.map_nonunit not_isUnit_zero, delta, reduceCtorEq, if_false]
  rcases eq_or_ne n 1 with rfl | hn'
  · simp [delta]
  have : ¬ IsUnit (n : ZMod 0) := fun h ↦ hn' <| ZMod.eq_one_of_isUnit_natCast h
  simp_all [χ.map_nonunit this, delta]

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

Goal state before:
pp: N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
H : LSeriesSummable (fun n ↦ χ ↑n) s
h : s.re ≤ 1
⊢ s.re ≤ re 1

Tactic:
simp [h]

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)
t : ℝ
ht : 0 < t
⊢ ∀ (i : ℕ), ‖2 * ↑i * Real.sin (2 * π * a * ↑i) * rexp (-π * ↑i ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 1 0 t i

Tactic:
intro n
    rw [norm_mul, norm_mul, norm_mul, norm_two, mul_assoc, mul_assoc,
      mul_le_mul_iff_of_pos_left two_pos, HurwitzKernelBounds.f_nat, pow_one, add_zero,
      norm_of_nonneg (exp_pos _).le, Real.norm_eq_abs, Nat.abs_cast, ← mul_assoc,
      mul_le_mul_iff_of_pos_right (exp_pos _)]
    exact mul_le_of_le_one_right (Nat.cast_nonneg _) (abs_sin_le_one _)

Goal state after:
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)
h_sum : Summable fun i ↦ ‖c i‖ / |↑i| ^ s.re
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2)
    (mellin (hurwitzOddFEPair ↑a).g ((s + 1) / 2) / 2)

Tactic:
refine (mellin_div_const .. ▸ hasSum_mellin_pi_mul_sq' (zero_lt_one.trans hs) hF h_sum).congr_fun
    fun n ↦ ?_

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)
h_sum : Summable fun i ↦ ‖c i‖ / |↑i| ^ s.re
n : ℤ
⊢ (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 =
    (s + 1).Gammaℝ * c n * ↑(SignType.sign ↑n) / ↑|↑n| ^ s
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inl
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ 0 + b ^ 0 + c ^ 0 = 0
⊢ p ∣ c

pp: case inr
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ p ∣ c

Tactic:
· simp at HF

Goal state after:
case inr
n : ℕ
p : ℤ
hp : Prime p
a b c : ℤ
hpa : p ∣ a
hpb : p ∣ b
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ p ∣ c
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: case pos
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
⊢ (if Nat.Prime p then (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ else 1) =
    if Nat.Prime p ∧ p ∣ N ∧ ¬N = 0 then (if Nat.Prime p then (1 - χ ↑p * ↑p ^ (-s))⁻¹ else 1) * (1 - χ ↑p * ↑p ^ (-s))
    else if Nat.Prime p then (1 - χ ↑p * ↑p ^ (-s))⁻¹ else 1

pp: case neg
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : ¬Nat.Prime p
⊢ (if Nat.Prime p then (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ else 1) =
    if Nat.Prime p ∧ p ∣ N ∧ ¬N = 0 then (if Nat.Prime p then (1 - χ ↑p * ↑p ^ (-s))⁻¹ else 1) * (1 - χ ↑p * ↑p ^ (-s))
    else if Nat.Prime p then (1 - χ ↑p * ↑p ^ (-s))⁻¹ else 1

Tactic:
swap

Goal state after:
case neg
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : ¬Nat.Prime p
⊢ (if Nat.Prime p then (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ else 1) =
    if Nat.Prime p ∧ p ∣ N ∧ ¬N = 0 then (if Nat.Prime p then (1 - χ ↑p * ↑p ^ (-s))⁻¹ else 1) * (1 - χ ↑p * ↑p ^ (-s))
    else if Nat.Prime p then (1 - χ ↑p * ↑p ^ (-s))⁻¹ else 1

case pos
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
⊢ (if Nat.Prime p then (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ else 1) =
    if Nat.Prime p ∧ p ∣ N ∧ ¬N = 0 then (if Nat.Prime p then (1 - χ ↑p * ↑p ^ (-s))⁻¹ else 1) * (1 - χ ↑p * ↑p ^ (-s))
    else if Nat.Prime p then (1 - χ ↑p * ↑p ^ (-s))⁻¹ else 1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ sinZeta (-a) s = -sinZeta a s

Tactic:
by
  simp_rw [sinZeta, completedSinZeta_neg, neg_div]

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

Goal state before:
pp: case pos
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
⊢ (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ =
    if p ∣ N ∧ ¬N = 0 then (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s)) else (1 - χ ↑p * ↑p ^ (-s))⁻¹

pp: case neg
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : ¬p ∣ N
⊢ (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ =
    if p ∣ N ∧ ¬N = 0 then (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s)) else (1 - χ ↑p * ↑p ^ (-s))⁻¹

Tactic:
swap

Goal state after:
case neg
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : ¬p ∣ N
⊢ (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ =
    if p ∣ N ∧ ¬N = 0 then (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s)) else (1 - χ ↑p * ↑p ^ (-s))⁻¹

case pos
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
⊢ (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ =
    if p ∣ N ∧ ¬N = 0 then (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s)) else (1 - χ ↑p * ↑p ^ (-s))⁻¹
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
⊢ Minimal a b c → Minimal a b (-c)

Tactic:
by
  rintro ⟨⟨ha, hb, heq⟩, h2⟩
  constructor
  · apply And.intro ha (And.intro hb _)
    rw [heq]
    exact (neg_sq c).symm
  rwa [Int.natAbs_neg c]

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

Goal state before:
pp: case inr.inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 = c0
⊢ False

Tactic:
exact ne_zero hf.1 h1.symm

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

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = m * (r * s)
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi : m = i ^ 2 ∨ m = -i ^ 2
hi' : ¬m = -i ^ 2
⊢ False

Tactic:
replace hi : m = i ^ 2 := Or.resolve_right hi hi'

Goal state after:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = m * (r * s)
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
⊢ False
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ max (a * derivative b).degree (derivative a * b).degree < a.degree + b.degree

Tactic:
rw [max_lt_iff]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * derivative b).degree < a.degree + b.degree ∧ (derivative a * b).degree < a.degree + b.degree
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ a.degree + (derivative b).degree < a.degree + b.degree

Tactic:
← Polynomial.degree_ne_bot

Goal state after:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a.degree ≠ ⊥
hb : b ≠ 0
⊢ a.degree + (derivative b).degree < a.degree + b.degree
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (derivative a).degree + b.degree < a.degree + b.degree

Tactic:
← Polynomial.degree_ne_bot

Goal state after:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b.degree ≠ ⊥
⊢ (derivative a).degree + b.degree < a.degree + b.degree
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ cexp (L (fun n ↦ ↑(Λ n) / ↑(Real.log ↑n)) s) = L 1 s

Tactic:
convert LSeries_eq_exp_LSeries (1 : DirichletCharacter ℂ 1) hs

Goal state after:
case e'_2
s : ℂ
hs : 1 < s.re
x✝ : ℕ
⊢ ↑(Λ x✝) = 1 ↑x✝ * ↑(Λ x✝)

case e'_3
s : ℂ
hs : 1 < s.re
x✝ : ℕ
⊢ 1 x✝ = 1 ↑x✝
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
⊢ 0 ∉ normalizedFactors a

Tactic:
exact zero_notMem_normalizedFactors _

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

Goal state before:
pp: case hb
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
p : M
ha : radical a ∣ p ^ n
i : M
hi : i ∈ normalizedFactors a
⊢ a ≠ 0

Tactic:
· rintro rfl
      simp only [normalizedFactors_zero, Multiset.notMem_zero] at hi

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

Goal state before:
pp: case inl
k : Type u_1
inst✝ : Field k
p q r : ℕ
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
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
nd_lt :
  (C u * a ^ p).natDegree + 1 ≤ (radical (a ^ p) * radical (b ^ q) * radical (c ^ r)).natDegree ∧
    (C v * b ^ q).natDegree + 1 ≤ (radical (a ^ p) * radical (b ^ q) * radical (c ^ r)).natDegree ∧
      (C w * c ^ r).natDegree + 1 ≤ (radical (a ^ p) * radical (b ^ q) * radical (c ^ r)).natDegree
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
radical_pow a hp,

Goal state after:
case inl
k : Type u_1
inst✝ : Field k
p q r : ℕ
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
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
nd_lt :
  (C u * a ^ p).natDegree + 1 ≤ (radical a * radical (b ^ q) * radical (c ^ r)).natDegree ∧
    (C v * b ^ q).natDegree + 1 ≤ (radical a * radical (b ^ q) * radical (c ^ r)).natDegree ∧
      (C w * c ^ r).natDegree + 1 ≤ (radical a * radical (b ^ q) * radical (c ^ r)).natDegree
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_2.inr.inl
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ := ⋯
this : IsTopologicalRing ↥K.topologicalClosure := ⋯
ι : ↥K → ↥K.topologicalClosure := ⋯
ui : IsUniformInducing ι
di : IsDenseInducing ι := ⋯
extψ : ↥K.topologicalClosure →+* ℂ := ⋯
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := ⋯
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = RingHom.id ℂ
⊢ (↑↑ψ).toFun = ⇑K.subtype

Tactic:
ext1 z

Goal state after:
case refine_2.inr.inl
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := extψ.comp ((RingEquiv.subfieldCongr h✝).symm.toRingHom.comp Subfield.topEquiv.symm.toRingHom)
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = RingHom.id ℂ
z : ↥K
⊢ (↑↑ψ).toFun z = K.subtype z
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_2.inr.inr
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ := ⋯
this : IsTopologicalRing ↥K.topologicalClosure := ⋯
ι : ↥K → ↥K.topologicalClosure := ⋯
ui : IsUniformInducing ι
di : IsDenseInducing ι := ⋯
extψ : ↥K.topologicalClosure →+* ℂ := ⋯
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := ⋯
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = starRingEnd ℂ
⊢ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype

Tactic:
ext1 z

Goal state after:
case refine_2.inr.inr
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := extψ.comp ((RingEquiv.subfieldCongr h✝).symm.toRingHom.comp Subfield.topEquiv.symm.toRingHom)
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = starRingEnd ℂ
z : ↥K
⊢ (↑↑ψ).toFun z = (⇑(starRingEnd ℂ) ∘ ⇑K.subtype) z
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
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
x✝ : K
⊢ (∃ b, (∃ z, z • x = b) ∧ ↑d • b = x✝) ↔ ∃ y, (∃ a, a * r = y) ∧ (algebraMap R K) y = x✝

Tactic:
exists_exists_eq_and,

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
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
x✝ : K
⊢ (∃ a, ↑d • a • x = x✝) ↔ ∃ a, (algebraMap R K) (a * r) = x✝
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 }
inst✝ : NumberField K
⊢ ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2

Tactic:
intro B

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2