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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
⊢ (((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) ⍟ fun n ↦ χ ↑n) = (fun n ↦ χ ↑n) * fun n ↦ Complex.log ↑n

Tactic:
by
  rw [← convolution_vonMangoldt_const_one, ← χ.mul_convolution_distrib, mul_one]

Goal state after:
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

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

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

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

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

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

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

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 ?_)
      push_cast
      simp only [abs_of_neg, neg_pow a, neg_pow b, neg_pow c, ← mul_add, *]

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

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

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

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

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

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

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
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ 1 / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)

Tactic:
have := (hasSum_int_completedHurwitzZetaEven a hs).div_const (Gammaℝ s)

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun i ↦ s.Gammaℝ / ↑|↑i + a| ^ s / 2 / s.Gammaℝ) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)
⊢ HasSum (fun n ↦ 1 / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ↑n ^ (-s).re = (↑n ^ s.re)⁻¹

Tactic:
neg_re,

Goal state after:
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ↑n ^ (-s.re) = (↑n ^ s.re)⁻¹
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ‖↑n ^ (-s)‖ = (↑n ^ s.re)⁻¹

Tactic:
rw [← ofReal_natCast,
    norm_cpow_eq_rpow_re_of_nonneg (Nat.cast_nonneg n) <| re_neg_ne_zero_of_one_lt_re hs,
    neg_re, Real.rpow_neg <| Nat.cast_nonneg n]

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

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

Tactic:
completedCosZeta_one_sub,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ completedHurwitzZetaEven a s * (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.cos (↑π * s / 2) * hurwitzZetaEven a s
Module: Mathlib.NumberTheory.FLT.Four

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

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

Goal state after:
case inl.inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 0
hbp : b0 % 2 = 0
h1 : 2 ∣ ↑(a0.gcd b0)
⊢ False
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Primes
⊢ 1 * ↑↑p ^ (-s).re < 1

Tactic:
neg_re,

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Primes
⊢ 1 * ↑↑p ^ (-s.re) < 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑k ^ 2 ∣ x0 * ↑k * (x0 * ↑k) + y0 * ↑k * (y0 * ↑k)

Tactic:
rw [(by ring : x0 * k * (x0 * k) + y0 * k * (y0 * k) = (k : ℤ) ^ 2 * (x0 * x0 + y0 * y0))]

Goal state after:
case neg
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑k ^ 2 ∣ ↑k ^ 2 * (x0 * x0 + y0 * y0)
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 * a) n

Tactic:
← sq,

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 (a ^ 2) n
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
hb2 : 2 ∣ b
⊢ False

Tactic:
obtain ⟨b', hb2'⟩ := hb2

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'
⊢ False
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 0 < x * x + y * y

Tactic:
← sq,

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 0 < x ^ 2 + y * 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
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
⊢ False

Tactic:
have h2b0 : b' ≠ 0 := by grind

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
⊢ False
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✝ : DecidableEq M
⊢ (normalizedFactors a).toFinset = primeFactors a

Tactic:
unfold primeFactors
  convert rfl

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 : s.gcd r = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hd' : ¬r * s = -d ^ 2
hd : s * r = d ^ 2
j : ℤ
hj : r = j ^ 2 ∨ r = -j ^ 2
hj0 : j ≠ 0
k : ℤ
hk : s = k ^ 2 ∨ s = -k ^ 2
hk0 : k ≠ 0
hj2 : r ^ 2 = j ^ 4
hk2 : s ^ 2 = k ^ 4
hh : i ^ 2 = j ^ 4 + k ^ 4
hn : n ≠ 0
⊢ m < c

Tactic:
ht3

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 : s.gcd r = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hd' : ¬r * s = -d ^ 2
hd : s * r = d ^ 2
j : ℤ
hj : r = j ^ 2 ∨ r = -j ^ 2
hj0 : j ≠ 0
k : ℤ
hk : s = k ^ 2 ∨ s = -k ^ 2
hk0 : k ≠ 0
hj2 : r ^ 2 = j ^ 4
hk2 : s ^ 2 = k ^ 4
hh : i ^ 2 = j ^ 4 + k ^ 4
hn : n ≠ 0
⊢ m < m ^ 2 + n ^ 2
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: 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

Tactic:
exact coprime_sq_sub_mul_of_even_odd h h1.left h1.right

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : ↥ℤ⁰
⊢ IsUnit ((algebraMap ℤ (End ℤ K)) ↑x)

Tactic:
by
    rw [← (Algebra.lmul _ _).commutes, Algebra.lmul_isUnit_iff, isUnit_iff_ne_zero, eq_intCast,
      Int.cast_ne_zero]
    exact nonZeroDivisors.coe_ne_zero x

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

Goal state before:
pp: case e_6
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥↑↑I
x✝ : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ ((basisOfFractionalIdeal K I).reindex e.symm) x✝ = (Subtype.val ∘ ⇑((fractionalIdealBasis K ↑I).reindex e.symm)) x✝

Tactic:
simpa using basisOfFractionalIdeal_apply K I _

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

Goal state before:
pp: case inr
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
chn0 : ringChar k ≠ 0
⊢ a.natDegree = 0

Tactic:
generalize eq_d : a.natDegree = d

Goal state after:
case inr
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
chn0 : ringChar k ≠ 0
d : ℕ
eq_d : a.natDegree = d
⊢ d = 0
Module: Mathlib.NumberTheory.NumberField.Units.Basic

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

Tactic:
(isUnit_map_iff (Rat.ringOfIntegersEquiv : 𝓞 ℚ →+* ℤ) x).symm,

Goal state after:
x : 𝓞 ℚ
⊢ IsUnit (↑ringOfIntegersEquiv x) ↔ ↑x = 1 ∨ ↑x = -1
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case hle
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
⊢ Subgroup.map (Units.complexEmbedding φ) (rootsOfUnity (torsionOrder K) (𝓞 K)) ≤ rootsOfUnity (torsionOrder K) ℂ

Tactic:
exact map_rootsOfUnity _ (torsionOrder K)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x✝ : { w // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (f ζ) k
⊢ (f ζ).im = 0

Tactic:
rw [← Complex.conj_eq_iff_im, ← NumberField.ComplexEmbedding.conjugate_coe_eq]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x✝ : { w // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (f ζ) k
⊢ (ComplexEmbedding.conjugate f) ζ = f ζ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case refine_2
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsMixed k φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding ∧ ComplexEmbedding.IsReal (mk (φ.comp (algebraMap k K))).embedding

Tactic:
embedding_mk_eq_of_isReal h.1

Goal state after:
case refine_2
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsMixed k φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
hw : w.IsReal
⊢ v.IsReal

Tactic:
rw [← not_isComplex_iff_isReal] at hw ⊢
  exact mt (isComplex_of_isComplex_under w) hw

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ (ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * (2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊)) *
          2 ^ finrank ℝ (mixedSpace K) *
        ↑(2 ^ nrRealPlaces K * (pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹).toReal =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹

Tactic:
toReal_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ (ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I)).toReal *
          ((2⁻¹ ^ nrComplexPlaces K).toReal * (↑(sqrt ‖discr K‖₊)).toReal) *
        (2 ^ finrank ℝ (mixedSpace K)).toReal *
      (↑(2 ^ nrRealPlaces K * (pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹).toReal =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
⊢ ⇑(negAt s) ⁻¹' A = ⇑(negAt s).symm ⁻¹' A

Tactic:
negAt_symm

Goal state after:
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
⊢ ⇑(negAt s) ⁻¹' A = ⇑(negAt s) ⁻¹' A
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
w : { w // w.IsReal }
hw : w ∉ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ 0 < ((negAt s) y).1 w

Tactic:
negAt_apply_isReal_and_notMem _ hw

Goal state after:
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
w : { w // w.IsReal }
hw : w ∉ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ 0 < y.1 w
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : Algebra B L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Algebra.IsIntegral A B
inst✝ : IsTorsionFree A B
x : B
⊢ (algebraMap A K) ((intNorm A B) x) = (norm K) ((algebraMap B L) x)

Tactic:
by
  have := IsIntegralClosure.isFractionRing_of_finite_extension A K L B
  apply (FractionRing.algEquiv A K).symm.injective
  rw [AlgEquiv.commutes, Algebra.intNorm, Algebra.map_intNormAux,
    ← AlgEquiv.commutes (FractionRing.algEquiv B L)]
  apply Algebra.norm_eq_of_equiv_equiv (FractionRing.algEquiv A K).toRingEquiv
    (FractionRing.algEquiv B L).toRingEquiv
  ext
  exact IsFractionRing.algEquiv_commutes (FractionRing.algEquiv A K) (FractionRing.algEquiv B L) _

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsReal }
⊢ normAtComplexPlaces x ↑w = x.1 w

Tactic:
normAtComplexPlaces,

Goal state after:
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsReal }
⊢ (if hw : (↑w).IsReal then x.1 ⟨↑w, hw⟩ else (normAtPlace ↑w) x) = x.1 w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsComplex }
⊢ normAtComplexPlaces x ↑w = ‖x.2 w‖

Tactic:
normAtComplexPlaces,

Goal state after:
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsComplex }
⊢ (if hw : (↑w).IsReal then x.1 ⟨↑w, hw⟩ else (normAtPlace ↑w) x) = ‖x.2 w‖
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings

Goal state before:
pp: case neg
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : ¬1 < n
⊢ φ n = 1

Tactic:
convert! totient_one
        exact eq_of_le_of_not_lt (not_lt.mp h1) (by simp [NeZero.ne _])

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
⊢ extended L hf 1 = 1

Tactic:
refine coeToSubmodule_injective <| Submodule.ext fun x ↦ ⟨fun hx ↦ span_induction
    ?_ (zero_mem _) (fun y z _ _ hy hz ↦ add_mem hy hz) (fun b y _ hy ↦ smul_mem _ b hy) hx, ?_⟩

Goal state after:
case refine_1
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
x : L
⊢ x ∈ (fun I ↦ ↑I) 1 → x ∈ (fun I ↦ ↑I) (extended L hf 1)

case refine_2
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
x : L
hx : x ∈ (fun I ↦ ↑I) (extended L hf 1)
⊢ ∀ x ∈ ⇑(IsLocalization.map L f hf) '' ↑1, x ∈ (fun I ↦ ↑I) 1