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

Goal state before:
pp: a x : ℝ
hx : 0 < x
h1 : HasSum (fun n ↦ jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n ↦ jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ ↑((↑n + a) * rexp (-π * (↑n + a) ^ 2 * x)) =
    (↑n + ↑a) * (cexp (-↑π * ↑a ^ 2 * ↑x) * cexp (2 * ↑π * I * ↑n * (↑a * I * ↑x) + ↑π * I * ↑n ^ 2 * (I * ↑x)))

Tactic:
← Complex.exp_add

Goal state after:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n ↦ jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n ↦ jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ ↑((↑n + a) * rexp (-π * (↑n + a) ^ 2 * x)) =
    (↑n + ↑a) * cexp (-↑π * ↑a ^ 2 * ↑x + (2 * ↑π * I * ↑n * (↑a * I * ↑x) + ↑π * I * ↑n ^ 2 * (I * ↑x)))
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: k : ℕ
hk : 1 < k
⊢ riemannZeta ↑k = ∑' (n : ℕ), 1 / ↑n ^ k

Tactic:
by
  simp only [zeta_eq_tsum_one_div_nat_cpow
      (by rwa [← ofReal_natCast, ofReal_re, ← Nat.cast_one, Nat.cast_lt] : 1 < re k),
    cpow_natCast]

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

Goal state before:
pp: case H
b p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_int 1 ↑b =O[atTop] fun t ↦ rexp (-p * t)
⊢ ∃ p, 0 < p ∧ oddKernel ↑b =O[atTop] fun x ↦ rexp (-p * x)

Tactic:
refine ⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩

Goal state after:
case H
b p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_int 1 ↑b =O[atTop] fun t ↦ rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop, ‖oddKernel (↑b) x‖ ≤ HurwitzKernelBounds.F_int 1 (↑b) x
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: m n : ℕ
hmn : m ∣ n
hm : FermatLastTheoremFor m
⊢ FermatLastTheoremFor n

Tactic:
exact FermatLastTheoremWith.mono hmn hm

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

Goal state before:
pp: a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖oddKernel a x‖) =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ ‖(ofReal ∘ oddKernel a) x - 0‖) =O[atTop] fun x ↦ x ^ r

Tactic:
simpa using hv'.trans (isLittleO_exp_neg_mul_rpow_atTop hv _).isBigO

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

Goal state before:
pp: a : UnitAddCircle
r : ℝ
⊢ (fun x ↦ (ofReal ∘ sinKernel a) x - 0) =O[atTop] fun x ↦ x ^ r

Tactic:
let ⟨v, hv, hv'⟩ := isBigO_atTop_sinKernel a

Goal state after:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : sinKernel a =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ (ofReal ∘ sinKernel a) x - 0) =O[atTop] fun x ↦ x ^ r
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖sinKernel a x‖) =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ ‖(ofReal ∘ sinKernel a) x - 0‖) =O[atTop] fun x ↦ x ^ r

Tactic:
simpa using hv'.trans (isLittleO_exp_neg_mul_rpow_atTop hv _).isBigO

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

Goal state before:
pp: n a✝ b✝ c✝ : ℕ
ha : a✝ = 1
hb : b✝ = 1
hc : c✝ = 1
⊢ a✝ ^ n + b✝ ^ n ≠ c✝ ^ n

Tactic:
ha,

Goal state after:
n a✝ b✝ c✝ : ℕ
ha : a✝ = 1
hb : b✝ = 1
hc : c✝ = 1
⊢ 1 ^ n + b✝ ^ n ≠ c✝ ^ n
Module: Mathlib.NumberTheory.FLT.Basic

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

Tactic:
ha,

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

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

Tactic:
ha,

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

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

Tactic:
ha,

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

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

Tactic:
ha,

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

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

Tactic:
ha,

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

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

Tactic:
ha,

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

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

Tactic:
ha,

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

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

Tactic:
ha,

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

Goal state before:
pp: s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ HasProd (fun p ↦ (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) (∑' (n : ℕ), (dirichletSummandHom χ ⋯) n)

Tactic:
convert! eulerProduct_completely_multiplicative_hasProd <| summable_dirichletSummand χ hs

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
⊢ a ^ 2 % 2 = 1

Tactic:
rw [sq, Int.mul_emod, ha2]

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
⊢ 1 * 1 % 2 = 1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

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

Tactic:
rw [← hb, ofReal_zero, zero_cpow ((not_lt.mpr zero_le_one) ∘ (zero_re ▸ · ▸ hs)),
      div_zero, div_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 w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
⊢ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
set abc_r := radical (a * b * c)

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
⊢ c.natDegree + 1 ≤ abc_r.natDegree
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
⊢ normalizedFactors a ⊆ normalizedFactors b ↔ (normalizedFactors a).toFinset ⊆ (normalizedFactors b).toFinset

Tactic:
Multiset.toFinset_subset

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
⊢ normalizedFactors a ⊆ normalizedFactors b ↔ normalizedFactors a ⊆ normalizedFactors b
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥↑↑I
⊢ |(integralBasis K).det ⇑((basisOfFractionalIdeal K I).reindex e.symm)| = FractionalIdeal.absNorm ↑I

Tactic:
rw [← FractionalIdeal.abs_det_basis_change (RingOfIntegers.basis K) I.1
    ((fractionalIdealBasis K I.1).reindex e.symm)]
  congr
  ext
  simpa using basisOfFractionalIdeal_apply K I _

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg.inr.inl
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 = 0
⊢ h.IsPrimitiveClassified

pp: case neg.inr.inr
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
⊢ h.IsPrimitiveClassified

Tactic:
· -- m odd, n even
    apply h.isPrimitiveClassified_aux hc hzpos hm2n2 hv2 hw2 _ hmncp
    · apply Or.intro_right
      exact And.intro hm2 hn2
    apply coprime_sq_sub_sq_add_of_odd_even hmncp hm2 hn2

Goal state after:
case neg.inr.inr
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
⊢ h.IsPrimitiveClassified
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✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| = absNorm I

Tactic:
rw [absNorm_eq, ← Ideal.natAbs_det_basis_change b I.num bI.num, Nat.cast_natAbs, Int.cast_abs,
    Int.cast_abs, Basis.det_apply, Basis.det_apply]

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✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |((Basis.localizationLocalization ℚ ℤ⁰ K b).toMatrix (Subtype.val ∘ ⇑bI)).det| =
    |↑(b.toMatrix (Subtype.val ∘ ⇑bI.num)).det| / |↑((Algebra.norm ℤ) ↑I.den)|
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✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ (algebraMap ℤ ℚ).mapMatrix (b.toMatrix (Subtype.val ∘ ⇑bI.num)) =
    b₀.toMatrix ((algebraMap R K) ↑I.den • Subtype.val ∘ ⇑bI)

Tactic:
ext : 2

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✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
i✝ j✝ : ι
⊢ (algebraMap ℤ ℚ).mapMatrix (b.toMatrix (Subtype.val ∘ ⇑bI.num)) i✝ j✝ =
    b₀.toMatrix ((algebraMap R K) ↑I.den • Subtype.val ∘ ⇑bI) i✝ j✝
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case mp.inl
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑φ.fieldRange.subtype
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

Tactic:
left; ext1 x
        conv_rhs => rw [← hiφ x]
        exact (congrFun h (ι x)).symm

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

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

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

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.inl ⟨rfl, rfl⟩, ?_⟩
      have : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2 := by
        rw [sq, ← h.eq]
        ring
      simpa using eq_or_eq_neg_of_sq_eq_sq _ _ this

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
⊢ (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))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
x✝ :
  (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
    |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
h₁ : ∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)
h₂ : |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
w : InfinitePlace K
hw : w.IsComplex
h_ne : ¬w = ↑w₀
⊢ w.embedding x ∈ ball 0 ↑(f w)

Tactic:
rw [mem_ball_zero_iff, norm_embedding_eq]

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
x✝ :
  (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
    |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
h₁ : ∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)
h₂ : |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
w : InfinitePlace K
hw : w.IsComplex
h_ne : ¬w = ↑w₀
⊢ 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
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ volume (⇑Complex.measurableEquivRealProd.symm ⁻¹' {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2}) = 4 * ↑B ^ 2

Tactic:
simp_rw [Set.preimage_ofPred_eq, Complex.measurableEquivRealProd_symm_apply]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := B.toMatrix fun i ↦ (canonicalEmbedding K) ((integralBasis K) (e i))
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i ↦ (integralBasis K) (e i)) (RingHom.equivRatAlgHom K ℂ)
⊢ M = N.transpose

Tactic:
ext : 2

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := B.toMatrix fun i ↦ (canonicalEmbedding K) ((integralBasis K) (e i))
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i ↦ (integralBasis K) (e i)) (RingHom.equivRatAlgHom K ℂ)
i✝ j✝ : K →+* ℂ
⊢ M i✝ j✝ = N.transpose i✝ j✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card { φ // ComplexEmbedding.IsReal φ } + Fintype.card { φ // ¬ComplexEmbedding.IsReal φ } = finrank ℚ K

Tactic:
← NumberField.Embeddings.card K ℂ,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card { φ // ComplexEmbedding.IsReal φ } + Fintype.card { φ // ¬ComplexEmbedding.IsReal φ } =
    Fintype.card (K →+* ℂ)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℝ (mixedSpace K) = finrank ℚ K

Tactic:
by
  classical
  rw [finrank_prod, finrank_pi, finrank_pi_fintype, Complex.finrank_real_complex, sum_const,
    card_univ, ← nrRealPlaces, ← nrComplexPlaces, ← card_real_embeddings, smul_eq_mul,
    mul_comm, ← card_complex_embeddings, ← NumberField.Embeddings.card K ℂ,
    Fintype.card_subtype_compl, Nat.add_sub_of_le (Fintype.card_subtype_le _)]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
⊢ volume (fundamentalDomain (latticeBasis K)) = 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊)

Tactic:
let N := Algebra.embeddingsMatrixReindex ℚ ℂ (integralBasis K ∘ f.symm)
    (RingHom.equivRatAlgHom K ℂ)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
⊢ volume (fundamentalDomain (latticeBasis K)) = 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (2 * Gamma (1 / 1 + 1)) ^ nrRealPlaces K * (π * 2 ^ (-2 / 1) * Gamma (2 / 1 + 1)) ^ nrComplexPlaces K =
    2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K

Tactic:
by
        simp_rw [div_one, one_add_one_eq_two, Gamma_add_one two_ne_zero, Gamma_two, mul_one,
          mul_assoc, ← Real.rpow_add_one two_ne_zero, show (-2 : ℝ) + 1 = -1 by norm_num,
          Real.rpow_neg_one, div_eq_mul_inv]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ Fintype.card (Free.ChooseBasisIndex ℤ ↥↑↑I) = Fintype.card (Free.ChooseBasisIndex ℤ (𝓞 K))

Tactic:
rw [← finrank_eq_card_chooseBasisIndex, ← finrank_eq_card_chooseBasisIndex,
      fractionalIdeal_rank]

Goal state after: