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

Goal state before:
pp: p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
⊢ ∃ u n, discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = ↑↑u * ↑p ^ n

Tactic:
rw [discr_prime_pow hζ hirr]
  by_cases heven : Even ((p ^ k).totient / 2)
  · exact ⟨1, p ^ (k - 1) * ((p - 1) * k - 1), by rw [heven.neg_one_pow]; simp⟩
  · exact ⟨-1, p ^ (k - 1) * ((p - 1) * k - 1), by
      rw [(not_even_iff_odd.1 heven).neg_one_pow]; simp⟩

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
v : α → ℕ
⊢ v ∈ {v | f v < g v} ∪ {v | g v < f v} ↔ v ∈ {v | f v ≠ g v}

Tactic:
dsimp; exact lt_or_lt_iff_ne (α := ℕ)

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ ∃ a b, (a ⊆ k.primesBelow ∧ b ≠ 0 ∧ b < N.sqrt + 1) ∧ b ^ 2 * ∏ x ∈ a, x = n

Tactic:
refine ⟨s, m, ⟨Finset.mem_powerset.mp hs, ?_, ?_⟩, hm.symm⟩

Goal state after:
case refine_1
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ≠ 0

case refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m < N.sqrt + 1
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
⊢ P.ε⁻¹ * ↑(x ^ P.k) * (P.ε * ↑((1 / x) ^ P.k)) = 1

Tactic:
rw [one_div, inv_rpow hx.le, ofReal_inv]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ P.ε⁻¹ * ↑(x ^ P.k) * (P.ε * (↑(x ^ P.k))⁻¹) = 1
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case convert_3.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : IntegrableOn (fun x ↦ ↑(rexp (-x)) * ↑x ^ (s - 1)) (Ioi (p i * 0)) volume
⊢ Integrable (fun t ↦ a i * (↑t ^ (s - 1) * ↑(rexp (-p i * t)))) (volume.restrict (Ioi 0))

Tactic:
← integrableOn_Ioi_comp_mul_left_iff _ _ hpi

Goal state after:
case convert_3.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : IntegrableOn (fun x ↦ ↑(rexp (-(p i * x))) * ↑(p i * x) ^ (s - 1)) (Ioi 0) volume
⊢ Integrable (fun t ↦ a i * (↑t ^ (s - 1) * ↑(rexp (-p i * t)))) (volume.restrict (Ioi 0))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) •
        ((2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ + (↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ)‖ ≤
    3 * π * ↑|n| ^ 2 * ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖

Tactic:
hns,

Goal state after:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ *
      ‖(2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ + (↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤
    3 * π * ↑|n| ^ 2 * ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_1
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖(2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ‖ ≤ 2 * π * ↑|n| ^ 2

Tactic:
hns,

Goal state after:
case refine_1
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖2 * ↑π * I * ↑n‖ * ‖ContinuousLinearMap.fst ℂ ℂ ℂ‖ ≤ 2 * π * ↑|n| ^ 2
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_2
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖(↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤ 1 * π * ↑|n| ^ 2

Tactic:
hns,

Goal state after:
case refine_2
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖↑π * I * ↑n ^ 2‖ * ‖ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤ 1 * π * ↑|n| ^ 2
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Tactic:
by
  -- substitute `t ↦ t⁻¹` in `mellin P.g s`
  have step1 := mellin_comp_rpow P.g (-s) (-1)
  simp_rw [abs_neg, abs_one, inv_one, one_smul, ofReal_neg, ofReal_one, div_neg, div_one, neg_neg,
    rpow_neg_one, ← one_div] at step1
  -- introduce a power of `t` to match the hypothesis `P.h_feq`
  have step2 := mellin_cpow_smul (fun t ↦ P.g (1 / t)) (P.k - s) (-P.k)
  rw [← sub_eq_add_neg, sub_right_comm, sub_self, zero_sub, step1] at step2
  -- put in the constant `P.ε`
  have step3 := mellin_const_smul (fun t ↦ (t : ℂ) ^ (-P.k : ℂ) • P.g (1 / t)) (P.k - s) P.ε
  rw [step2] at step3
  rw [← step3]
  -- now the integrand matches `P.h_feq'` on `Ioi 0`, so we can apply `setIntegral_congr_fun`
  refine setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)
  simp_rw [P.h_feq' t ht, ← mul_smul]
  -- some simple `cpow` arithmetic to finish
  rw [cpow_neg, ofReal_cpow (le_of_lt ht)]
  have : (t : ℂ) ^ (P.k : ℂ) ≠ 0 := by simpa [← ofReal_cpow ht.le] using (rpow_pos_of_pos ht _).ne'
  field_simp [P.hε]

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

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

Tactic:
exact Or.inr (lt_of_le_of_ne (hp i) (Ne.symm h))

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

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
⊢ HasDerivAt (fun x ↦ jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z

Tactic:
by
  -- This proof is annoyingly fiddly, because of the need to commute "evaluation at a point"
  -- through infinite sums of continuous linear maps.
  let eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
  { toFun := fun f ↦ f (1, 0)
    map_add' := by simp only [add_apply, forall_const]
    map_smul' := by simp }
  have step1 : HasSum (fun n ↦ (jacobiTheta₂_term_fderiv n z τ) (1, 0))
      ((jacobiTheta₂_fderiv z τ) (1, 0)) := by
    apply eval_fst_CLM.hasSum (hasSum_jacobiTheta₂_term_fderiv z hτ)
  have step2 (n : ℤ) : (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ := by
    simp [jacobiTheta₂_term_fderiv, jacobiTheta₂'_term, jacobiTheta₂_term, mul_comm]
  simp only [step2] at step1
  have step3 : HasDerivAt (fun x ↦ jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ) (1, 0)) z :=
    (((hasFDerivAt_jacobiTheta₂ z hτ).comp z (hasFDerivAt_prodMk_left z τ)).hasDerivAt :)
  rwa [← step1.tsum_eq] at step3

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}
⊢ ContinuousAt (fun p ↦ jacobiTheta₂' p.1 p.2) (z, τ)

Tactic:
have hVo : IsOpen V := ((_root_.continuous_abs.comp continuous_im).isOpen_preimage _
    isOpen_Iio).prod (continuous_im.isOpen_preimage _ isOpen_Ioi)

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
⊢ ContinuousAt (fun p ↦ jacobiTheta₂' p.1 p.2) (z, τ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inl
z : ℂ
⊢ jacobiTheta₂' z 0 = -2 * ↑π / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)

pp: case inr
z τ : ℂ
hτ : τ ≠ 0
⊢ jacobiTheta₂' z τ = -2 * ↑π / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)

Tactic:
· rw [jacobiTheta₂'_undef _ (by simp), mul_zero, zero_cpow (by simp), div_zero, zero_mul]

Goal state after:
case inr
z τ : ℂ
hτ : τ ≠ 0
⊢ jacobiTheta₂' z τ = -2 * ↑π / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case neg
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ¬∃ n, ↑n = a
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - 0)

Tactic:
suffices ∀ (n : ℤ), n + a ≠ 0 by simpa [this] using hasSum_int_evenKernel a ht
    contrapose! h
    let ⟨n, hn⟩ := h
    exact ⟨-n, by simpa [neg_eq_iff_add_eq_zero]⟩

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

Goal state before:
pp: case H
x : ℝ
hx : x ≤ 0
a : ℝ
⊢ ↑(sinKernel (↑a) x) = 0

Tactic:
sinKernel_def,

Goal state after:
case H
x : ℝ
hx : x ≤ 0
a : ℝ
⊢ jacobiTheta₂' (↑a) (I * ↑x) / (-2 * ↑π) = 0
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)) * ↑(sinKernel (↑a) (1 / x))

Tactic:
sinKernel_def,

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)) * (jacobiTheta₂' (↑a) (I * ↑(1 / x)) / (-2 * ↑π))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
⊢ ∃ p, 0 < p ∧ (fun x ↦ cosKernel a x - 1) =O[atTop] fun x ↦ rexp (-p * x)

Tactic:
induction a using QuotientAddGroup.induction_on with | H a =>
  obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_nat_zero_sub zero_le_one
  refine ⟨p, hp, (Eventually.isBigO ?_).trans (hp'.const_mul_left 2)⟩
  filter_upwards [eventually_gt_atTop 0] with t ht
  simp only [eq_false_intro one_ne_zero, if_false, sub_zero,
    ← (hasSum_nat_cosKernel₀ a ht).tsum_eq, HurwitzKernelBounds.F_nat]
  apply tsum_of_norm_bounded ((HurwitzKernelBounds.summable_f_nat 0 1 ht).hasSum.mul_left 2)
  intro n
  rw [norm_mul, norm_mul, norm_two, mul_assoc, mul_le_mul_iff_of_pos_left two_pos,
    norm_of_nonneg (exp_pos _).le, HurwitzKernelBounds.f_nat, pow_zero, one_mul, Real.norm_eq_abs]
  exact mul_le_of_le_one_left (exp_pos _).le (abs_cos_le_one _)

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

Goal state before:
pp: case inr
a b : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) 1

Tactic:
· convert!
    (differentiableAt_hurwitzZetaEven_sub_one_div a).fun_sub
      (differentiableAt_hurwitzZetaEven_sub_one_div b) using
    2 with s
    abel

Goal state after:
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:
simp_rw [← ofReal_natCast]

Goal state after:
s : ℂ
n✝ : ℕ
χ : DirichletCharacter ℂ n✝
hs : s ≠ 0
m n : ℕ
⊢ χ ↑(m * n) * ↑↑(m * n) ^ (-s) = χ ↑m * ↑↑m ^ (-s) * (χ ↑n * ↑↑n ^ (-s))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaOdd (-a) s / (s + 1).Gammaℝ = -(completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)

Tactic:
completedHurwitzZetaOdd_neg,

Goal state after:
a : UnitAddCircle
s : ℂ
⊢ -completedHurwitzZetaOdd a s / (s + 1).Gammaℝ = -(completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
this : -(↑n + 1) + a = -(↑n + 1 - a)
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -(↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2) =
    ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + ↑(-SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2

Tactic:
SignType.coe_neg,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
this : -(↑n + 1) + a = -(↑n + 1 - a)
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -(↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2) =
    ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m n : ℤ
h : m.gcd n = 1
hmn : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

Tactic:
rcases hmn with h1 | h2

Goal state after:
case inl
m n : ℤ
h : m.gcd n = 1
h1 : m % 2 = 0 ∧ n % 2 = 1
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

case inr
m n : ℤ
h : m.gcd n = 1
h2 : m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
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
ha : Irreducible a
hb : b ≠ 0
⊢ a ∣ radical b ↔ a ∣ b

Tactic:
by
  constructor
  · intro ha
    exact ha.trans radical_dvd_self
  · intro ha'
    obtain ⟨c, hc, hc'⟩ := exists_mem_normalizedFactors_of_dvd hb ha ha'
    exact hc'.dvd.trans (Finset.dvd_prod_of_mem _ (by simpa [mem_primeFactors] using hc))

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : 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
⊢ IsCoprime b c

Tactic:
add_eq_zero_iff_neg_eq

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
w : k[X] := a.wronskian b
wab : w = a.wronskian b
⊢ IsCoprime b c
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
⊢ Squarefree (radical a)

Tactic:
by
  nontriviality M
  exact isRadical_radical.squarefree (by simp [radical_ne_zero])

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : 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
⊢ IsCoprime c a

Tactic:
add_eq_zero_iff_neg_eq

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
⊢ IsCoprime c a
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
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime b c

Tactic:
add_eq_zero_iff_neg_eq

Goal state after:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : -(C u * a ^ p + C v * b ^ q) = C w * c ^ r
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime b c
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ p * a * (q * r) + q * b * (r * p) + r * c * (p * q) + 1 ≤
    (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q)

Tactic:
rw [Nat.succ_le_iff]
      gcongr

Goal state after:
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 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
⊢ w = ↑((m ^ 2 - n ^ 2) / 2) / ↑((m ^ 2 + n ^ 2) / 2)

Tactic:
rw [← Rat.divInt_eq_div, ← Rat.divInt_mul_right (by simp : (2 : ℤ) ≠ 0)]

Goal state after:
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 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
⊢ w = Rat.divInt ((m ^ 2 - n ^ 2) / 2 * 2) ((m ^ 2 + n ^ 2) / 2 * 2)
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_2.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 = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrictField)
hψ₁ : Continuous ⇑ψ₁
x : ↥K
r : ℝ
hr : ofRealHom.rangeRestrictField r = j (ι x)
this : extψ (j.symm.toRingHom (ofRealHom.rangeRestrictField r)) = ofRealHom r
⊢ (↑↑ψ).toFun x = K.subtype x

Tactic:
hr,

Goal state after:
case refine_2.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 = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrictField)
hψ₁ : Continuous ⇑ψ₁
x : ↥K
r : ℝ
hr : ofRealHom.rangeRestrictField r = j (ι x)
this : extψ (j.symm.toRingHom (j (ι x))) = ofRealHom r
⊢ (↑↑ψ).toFun x = K.subtype 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
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
⊢ |(Algebra.norm ℚ) ((algebraMap R K) r)| / |(Algebra.norm ℚ) ((algebraMap R K) ↑d)| = |(Algebra.norm ℚ) x|

Tactic:
hr,

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
⊢ |(Algebra.norm ℚ) (↑d • x)| / |(Algebra.norm ℚ) ((algebraMap R K) ↑d)| = |(Algebra.norm ℚ) x|
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
x y : ↥φ.range
⊢ ‖ψ (ι.symm x - ι.symm y)‖ ≤ dist x y

Tactic:
← map_sub

Goal state after:
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
x y : ↥φ.range
⊢ ‖ψ (ι.symm (x - y))‖ ≤ dist x y
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
⊢ (∃ a, ↑d • a • x = x✝) ↔ ∃ a, (algebraMap R K) a * (algebraMap R K) r = x✝

Tactic:
hr,

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 * ↑d • x = x✝