mathlib-initiative/mathlib-tactics huggingface dataset:
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
n : ℤ
⊢ 2 * ↑π * I * ↑a * ↑n = ↑(2 * π * a * ↑n) * I

Tactic:
push_cast

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
n : ℤ
⊢ 2 * ↑π * I * ↑a * ↑n = 2 * ↑π * ↑a * ↑n * I
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ 1 / ↑|↑n + a| ^ s / 2)
    (Function.update (fun s ↦ completedHurwitzZetaEven (↑a) s / s.Gammaℝ) 0 (if ↑a = 0 then -1 / 2 else 0) s)

Tactic:
Function.update_of_ne (ne_zero_of_one_lt_re hs)

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2)
    (Function.update (fun s ↦ completedCosZeta (↑a) s / s.Gammaℝ) 0 (-1 / 2) s)

Tactic:
Function.update_of_ne (ne_zero_of_one_lt_re hs)

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedCosZeta (↑a) s / s.Gammaℝ)
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
⊢ IsCoprime a b

Tactic:
by
  apply Int.isCoprime_iff_gcd_eq_one.mpr
  by_contra hab
  obtain ⟨p, hp, hpa, hpb⟩ := Nat.Prime.not_coprime_iff_dvd.mp hab
  obtain ⟨a1, rfl⟩ := Int.natCast_dvd.mpr hpa
  obtain ⟨b1, rfl⟩ := Int.natCast_dvd.mpr hpb
  have hpc : (p : ℤ) ^ 2 ∣ c := by
    rw [← Int.pow_dvd_pow_iff two_ne_zero, ← h.1.2.2]
    apply Dvd.intro (a1 ^ 4 + b1 ^ 4)
    ring
  obtain ⟨c1, rfl⟩ := hpc
  have hf : Fermat42 a1 b1 c1 :=
    (Fermat42.mul (Int.natCast_ne_zero.mpr (Nat.Prime.ne_zero hp))).mpr h.1
  apply Nat.le_lt_asymm (h.2 _ _ _ hf)
  rw [Int.natAbs_mul, lt_mul_iff_one_lt_left, Int.natAbs_pow, Int.natAbs_natCast]
  · exact Nat.one_lt_pow two_ne_zero (Nat.Prime.one_lt hp)
  · exact Nat.pos_of_ne_zero (Int.natAbs_ne_zero.2 (ne_zero hf))

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
⊢ 0 ≠ m

Tactic:
rintro rfl

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
n : ℤ
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
ht1 : a ^ 2 = 0 ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * 0 * n
ht3 : c = 0 ^ 2 + n ^ 2
ht4 : Int.gcd 0 n = 1
ht5 : 0 % 2 = 0 ∧ n % 2 = 1 ∨ 0 % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ 0
htt : PythagoreanTriple a n 0
⊢ False
Module: Mathlib.NumberTheory.PythagoreanTriples

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

Tactic:
rintro rfl

Goal state after:
x y : ℤ
hc : x.gcd y = 1
h : PythagoreanTriple x y 0
this : 0 < 0 * 0
⊢ False
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: case e'_2
s : ℝ
hs : 1 < s
⊢ ∑' (n : ℕ), ↑(Λ n) / ↑(Real.log ↑n) / ↑n ^ ↑s = ↑(∑' (n : ℕ), Λ n / (↑n ^ s * Real.log ↑n))

Tactic:
push_cast

Goal state after:
case e'_2
s : ℝ
hs : 1 < s
⊢ ∑' (n : ℕ), ↑(Λ n) / Complex.log ↑n / ↑n ^ ↑s = ∑' (a : ℕ), ↑(Λ a) / (↑(↑a ^ s) * Complex.log ↑a)
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical b ∣ a.wronskian b

Tactic:
← wronskian_neg_eq,

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical b ∣ -b.wronskian a
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

Goal state after:
case hb
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
n : ℕ
p i : M
ha : radical 0 ∣ p ^ n
hi : i ∈ normalizedFactors 0
⊢ False
Module: Mathlib.NumberTheory.NumberField.Norm

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
F : Type u_3
inst✝³ : Field F
inst✝² : Algebra K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Tactic:
have : FiniteDimensional F L := FiniteDimensional.right K F L

Goal state after:
K : Type u_2
inst✝⁴ : Field K
F : Type u_3
inst✝³ : Field F
inst✝² : Algebra K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this✝ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this : FiniteDimensional F ↥L
⊢ IsUnit ((norm K) x) ↔ IsUnit 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✝² : 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 ℤ ℚ) ((Algebra.norm ℤ) ↑I.den)| ≠ 0

Tactic:
by
    rw [ne_eq, abs_eq_zero, IsFractionRing.to_map_eq_zero_iff, Algebra.norm_eq_zero_iff_of_basis b]
    exact nonZeroDivisors.coe_ne_zero _

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)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
this : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
⊢ ENNReal.ofReal |(Basis.det ?b₀) ⇑((latticeBasis K).reindex e.symm)| * volume (fundamentalDomain ?b₀) =
    ↑‖((mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)).det‖.toNNReal

pp: case b₀
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) := ⋯
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := ⋯
M : Matrix (index K) (index K) ℝ := ⋯
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := ⋯
this : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
⊢ Basis (index K) ℝ (mixedSpace K)

Tactic:
volume_fundamentalDomain_stdBasis,

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 ℂ)
this : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
⊢ ENNReal.ofReal |(mixedEmbedding.stdBasis K).det ⇑((latticeBasis K).reindex e.symm)| * 1 =
    ↑‖((mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)).det‖.toNNReal
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ mixedEmbedding.norm x ≠ 0 ↔ ∀ (w : InfinitePlace K), (normAtPlace w) x ≠ 0

Tactic:
rw [← not_iff_not]
  simp_rw [ne_eq, mixedEmbedding.norm_eq_zero_iff, not_not, not_forall, not_not]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = (normAtPlace w) y
⊢ mixedEmbedding.norm x = mixedEmbedding.norm y

Tactic:
mixedEmbedding.norm_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = (normAtPlace w) y
⊢ ∏ w, (normAtPlace w) x ^ w.mult = ∏ w, (normAtPlace w) y ^ w.mult
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : mixedSpace K
⊢ mixedEmbedding.norm (c • x) = |c| ^ finrank ℚ K * mixedEmbedding.norm x

Tactic:
mixedEmbedding.norm_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : mixedSpace K
⊢ ∏ w, (normAtPlace w) (c • x) ^ w.mult = |c| ^ finrank ℚ K * ∏ w, (normAtPlace w) x ^ w.mult
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ mixedEmbedding.norm ((mixedEmbedding K) x) = ↑|(Algebra.norm ℚ) x|

Tactic:
mixedEmbedding.norm_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w, (normAtPlace w) ((mixedEmbedding K) x) ^ w.mult = ↑|(Algebra.norm ℚ) x|
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (∏ i, volume (Set.Ico 0 1)) * ∏ i, volume (⇑measurableEquivPi ⁻¹' Set.univ.pi fun x ↦ Set.Ico 0 1) = 1

Tactic:
Complex.volume_preserving_equiv_pi.measure_preimage ?_,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (∏ i, volume (Set.Ico 0 1)) * ∏ i, volume (Set.univ.pi fun x ↦ Set.Ico 0 1) = 1

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ NullMeasurableSet (Set.univ.pi fun x ↦ Set.Ico 0 1) volume
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    ∑ x_1,
        fromBlocks 1 0 0
            ((blockDiagonal fun x ↦
                  of
                    (vecCons (vecCons 2⁻¹ (vecCons 2⁻¹ (2⁻¹ • ![])))
                      (vecCons (vecCons (2⁻¹ * -I) (vecCons (2⁻¹ * I) (2⁻¹ • ![]))) (2⁻¹ • ![])))).submatrix
              ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
            c (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0
              ((blockDiagonal fun x ↦
                    of
                      (vecCons (vecCons 2⁻¹ (vecCons 2⁻¹ (2⁻¹ • ![])))
                        (vecCons (vecCons (2⁻¹ * -I) (vecCons (2⁻¹ * I) (2⁻¹ • ![]))) (2⁻¹ • ![])))).submatrix
                ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
              c (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0
              ((blockDiagonal fun x ↦
                    of
                      (vecCons (vecCons 2⁻¹ (vecCons 2⁻¹ (2⁻¹ • ![])))
                        (vecCons (vecCons (2⁻¹ * -I) (vecCons (2⁻¹ * I) (2⁻¹ • ![]))) (2⁻¹ • ![])))).submatrix
                ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
              c (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Tactic:
Matrix.smul_empty,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    ∑ x_1,
        fromBlocks 1 0 0
            ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix
              ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
            c (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0
              ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix
                ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
              c (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0
              ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix
                ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
              c (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
h : minkowskiBound K I < volume (convexBodyLT K f)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w a < ↑(f w)

Tactic:
obtain ⟨⟨x, hx⟩, h_nz, h_mem⟩ := exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure
    h_fund (convexBodyLT_neg_mem K f) (convexBodyLT_convex K f) h

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
h : minkowskiBound K I < volume (convexBodyLT K f)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
x : mixedSpace K
hx : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨x, hx⟩ ≠ 0
h_mem : ↑⟨x, hx⟩ ∈ convexBodyLT K f
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w a < ↑(f w)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (ENNReal.toReal 2)⁻¹ ^ nrComplexPlaces K * (↑(sqrt ‖discr K‖₊)).toReal = 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|

Tactic:
toReal_ofNat,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2⁻¹ ^ nrComplexPlaces K * (↑(sqrt ‖discr K‖₊)).toReal = 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ (ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I)).toReal *
      ((ENNReal.toReal 2)⁻¹ ^ nrComplexPlaces K * (↑(sqrt ‖discr K‖₊)).toReal) =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|

Tactic:
toReal_ofNat,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ (ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I)).toReal * (2⁻¹ ^ nrComplexPlaces K * (↑(sqrt ‖discr K‖₊)).toReal) =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|
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)).toReal *
          ((ENNReal.toReal 2)⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊)) *
        ENNReal.toReal 2 ^ finrank ℝ (mixedSpace K) *
      ↑(2 ^ nrRealPlaces K * (pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹ =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹

Tactic:
toReal_ofNat,

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 * ↑(sqrt ‖discr K‖₊)) *
        2 ^ finrank ℝ (mixedSpace K) *
      ↑(2 ^ nrRealPlaces K * (pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹ =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝³¹ : CommRing A
inst✝³⁰ : CommRing B
inst✝²⁹ : CommRing B₂
inst✝²⁸ : CommRing B₃
inst✝²⁷ : Algebra A B
inst✝²⁶ : Algebra A B₂
inst✝²⁵ : Algebra A B₃
inst✝²⁴ : Field K
inst✝²³ : Field L
inst✝²² : Field L₂
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 K L₂
inst✝¹⁴ : Algebra A L₂
inst✝¹³ : IsScalarTower A K L₂
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✝⁶ : Algebra B₂ L₂
inst✝⁵ : IsScalarTower A B₂ L₂
inst✝⁴ : IsIntegralClosure B₂ A L₂
inst✝³ : Algebra B₃ L₃
inst✝² : IsScalarTower A B₃ L₃
inst✝¹ : IsIntegralClosure B₃ A L₃
inst✝ : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B₂
this✝¹ : IsDomain A
this✝ : IsTorsionFree A L₂
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
H : ∀ (y : ↥(Algebra.algebraMapSubmonoid B A⁰)), IsUnit (((algebraMap B₂ L₂).comp ↑σ) ↑y)
⊢ (IsLocalization.lift H).comp (algebraMap K L) = algebraMap K L₂

Tactic:
by
    apply IsLocalization.ringHom_ext A⁰
    ext
    simp only [RingHom.coe_comp, Function.comp_apply, ← IsScalarTower.algebraMap_apply A K L,
      ← IsScalarTower.algebraMap_apply A K L₂,
      IsScalarTower.algebraMap_apply A B L, IsScalarTower.algebraMap_apply A B₂ L₂,
      IsLocalization.lift_eq, RingHom.coe_coe, AlgHom.commutes]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
B : Type u_6
B₂ : Type u_7
inst✝²² : CommRing A
inst✝²¹ : CommRing B
inst✝²⁰ : CommRing B₂
inst✝¹⁹ : Algebra A B
inst✝¹⁸ : Algebra A B₂
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
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 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✝³ : Algebra B₂ L₂
inst✝² : IsScalarTower A B₂ L₂
inst✝¹ : IsIntegralClosure B₂ A L₂
inst✝ : Algebra.IsAlgebraic K L
σ : L →ₐ[K] L₂
this✝ : IsDomain A
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
x : B
⊢ ((↑(galLift K L L₂ (galRestrict' A B B₂ σ))).comp (algebraMap B L)) x = ((↑σ).comp (algebraMap B L)) x

Tactic:
simp [galRestrict', Subalgebra.algebraMap_eq, galLift]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ Function.Injective ⇑mixedSpaceOfRealSpace

Tactic:
refine (injective_iff_map_eq_zero mixedSpaceOfRealSpace).mpr fun _ h ↦ ?_
  rw [mixedSpaceOfRealSpace_apply, Prod.mk_eq_zero, funext_iff, funext_iff] at h
  ext w
  obtain hw | hw := isReal_or_isComplex w
  · exact h.1 ⟨w, hw⟩
  · exact Complex.ofReal_inj.mp <| h.2 ⟨w, hw⟩

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: case neg
A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ IsIntegral A
    (((algebraMap B E) x)⁻¹ * ((minpoly K ((algebraMap B L) x)).aroots E).prod ^ finrank (↥K⟮(algebraMap B L) x⟯) L)

Tactic:
← Multiset.prod_erase
    (a := algebraMap B E x)

Goal state after:
case neg
A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ IsIntegral A
    (((algebraMap B E) x)⁻¹ *
      ((algebraMap B E) x * (((minpoly K ((algebraMap B L) x)).aroots E).erase ((algebraMap B E) x)).prod) ^
        finrank (↥K⟮(algebraMap B L) x⟯) L)

case neg
A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ (algebraMap B E) x ∈ (minpoly K ((algebraMap B L) x)).aroots E
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings

Goal state before:
pp: 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:
simp [NeZero.ne _]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊,
    Nat.Prime p →
      ∀ P ∈ (span {↑p}).primesOver (𝓞 K),
        p ^ P.inertiaDeg ℤ ≤
            ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ →
          Submodule.IsPrincipal P
x✝ : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : P ∈ (Ideal (𝓞 K))⁰
hP : (↑⟨P, HP⟩).IsPrime
hPN :
  ↑(absNorm ↑⟨P, HP⟩) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
hp0 : p ≠ 0
⊢ Submodule.IsPrincipal ↑⟨P, HP⟩

Tactic:
have hpprime := (span_singleton_prime hp0).mp

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊,
    Nat.Prime p →
      ∀ P ∈ (span {↑p}).primesOver (𝓞 K),
        p ^ P.inertiaDeg ℤ ≤
            ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ →
          Submodule.IsPrincipal P
x✝ : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : P ∈ (Ideal (𝓞 K))⁰
hP : (↑⟨P, HP⟩).IsPrime
hPN :
  ↑(absNorm ↑⟨P, HP⟩) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
hp0 : p ≠ 0
hpprime : (span {p}).IsPrime → _root_.Prime p
⊢ Submodule.IsPrincipal ↑⟨P, HP⟩