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

Goal state before:
pp: case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + ↑a) ^ s = 1 / ↑|↑n + a| ^ s

Tactic:
rw [abs_of_nonneg (by linarith [ha.1, ha.2])]

Goal state after:
case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + ↑a) ^ s = 1 / ↑(↑n + a) ^ s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + 1 - ↑a) ^ s = 1 / ↑|↑n + 1 - a| ^ s

Tactic:
rw [abs_of_nonneg (by linarith [ha.1, ha.2])]

Goal state after:
case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + 1 - ↑a) ^ s = 1 / ↑(↑n + 1 - a) ^ s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum (fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 + cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (cosZeta (↑a) s + cexp (2 * ↑π * I * ↑a * 0) / 0 ^ s / 2)
⊢ HasSum (fun n ↦ ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (cosZeta (↑a) s)

Tactic:
zero_cpow (ne_zero_of_one_lt_re hs),

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum (fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 + cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (cosZeta (↑a) s + cexp (2 * ↑π * I * ↑a * 0) / 0 / 2)
⊢ HasSum (fun n ↦ ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (cosZeta (↑a) s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (sinZeta (↑a) s + -I * ↑(Int.sign 0) * cexp (2 * ↑π * I * ↑a * 0) / 0 ^ s / 2)
⊢ HasSum (fun n ↦ ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)

Tactic:
zero_cpow (ne_zero_of_one_lt_re hs),

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (sinZeta (↑a) s + -I * ↑(Int.sign 0) * cexp (2 * ↑π * I * ↑a * 0) / 0 / 2)
⊢ HasSum (fun n ↦ ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b : R[X]
hw : wronskian 0 b ≠ 0
⊢ False

Tactic:
wronskian_zero_left

Goal state after:
R : Type u_1
inst✝ : CommRing R
b : R[X]
hw : 0 ≠ 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 b : M
h : Associated a b
⊢ primeFactors a = primeFactors b

Tactic:
by
  unfold primeFactors
  rw [h.normalizedFactors_eq]

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
⊢ primeFactors a = ∅ ↔ IsUnit a

Tactic:
rw [primeFactors, Multiset.toFinset_eq_empty, normalizedFactors_eq_zero_iff ha]

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

Goal state before:
pp: case cons
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
i : ι
s : Finset ι
h : i ∉ s
ih : radical (∏ i ∈ s, f i) ∣ ∏ i ∈ s, radical (f i)
⊢ radical (f i * ∏ i ∈ s, f i) ∣ radical (f i) * ∏ i ∈ s, radical (f i)

Tactic:
exact radical_mul_dvd.trans (mul_dvd_mul_left _ ih)

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < m ^ 2 + n ^ 2
hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
h2 : y = m ^ 2 - n ^ 2 ∧ z = m ^ 2 + n ^ 2
⊢ x = 2 * m * n

Tactic:
← Rat.intCast_inj,

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < m ^ 2 + n ^ 2
hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
h2 : y = m ^ 2 - n ^ 2 ∧ z = m ^ 2 + n ^ 2
⊢ ↑x = ↑(2 * m * n)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
⊢ ℚ⟮↑x⟯ = ⊤

Tactic:
by
  rw [Field.primitive_element_iff_algHom_eq_of_eval ℚ ℂ ?_ _ w.embedding.toRatAlgHom]
  · intro ψ hψ
    have h : 1 ≤ w x := one_le_of_lt_one h₁ h₂
    have main : w = InfinitePlace.mk ψ.toRingHom := by
      simp only [RingHom.toRatAlgHom_apply] at hψ
      rw [← norm_embedding_eq, hψ] at h
      contrapose! h
      exact h₂ h.symm
    rw [(mk_embedding w).symm, mk_eq_iff] at main
    cases h₃ with
    | inl hw =>
      rw [conjugate_embedding_eq_of_isReal hw, or_self] at main
      exact congr_arg RingHom.toRatAlgHom main
    | inr hw =>
      refine congr_arg RingHom.toRatAlgHom (main.resolve_right fun h' ↦ hw.not_ge ?_)
      have : (embedding w x).im = 0 := by
        rw [← Complex.conj_eq_iff_im]
        have := RingHom.congr_fun h' x
        simp only [ComplexEmbedding.conjugate_coe_eq, AlgHom.toRingHom_eq_coe,
          RingHom.coe_coe] at this
        rw [this]
        exact hψ.symm
      rwa [← norm_embedding_eq, ← Complex.re_add_im (embedding w x), this, Complex.ofReal_zero,
        zero_mul, add_zero, Complex.norm_real] at h
  · exact fun x ↦ IsAlgClosed.splits _

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

Goal state before:
pp: case e'_2.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝¹ x✝ : { x // mkComplex x = ⟨w, hw⟩ }
h : ↑↑x✝¹ = ↑↑x✝
⊢ x✝¹ = x✝

Tactic:
← Subtype.ext_iff,

Goal state after:
case e'_2.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝¹ x✝ : { x // mkComplex x = ⟨w, hw⟩ }
h : ↑x✝¹ = ↑x✝
⊢ x✝¹ = x✝
Module: Mathlib.NumberTheory.NumberField.EquivReindex

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i✝ j✝ : K →+* ℂ
⊢ basisMatrix K i✝ j✝ =
    Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑(equivReindex K)) (RingHom.equivRatAlgHom K ℂ) i✝ j✝

Tactic:
simp [Algebra.embeddingsMatrixReindex]

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
hφ : ComplexEmbedding.IsReal w.embedding
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)

Tactic:
exact hφ.comp f

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ ↑(Algebra.discr ℚ ⇑(integralBasis K)) = (algebraMap ℚ ℂ) (Algebra.discr ℚ (⇑(integralBasis K) ∘ ⇑(equivReindex K)))

Tactic:
← (equivReindex K).symm_symm,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ ↑(Algebra.discr ℚ ⇑(integralBasis K)) =
    (algebraMap ℚ ℂ) (Algebra.discr ℚ (⇑(integralBasis K) ∘ ⇑(equivReindex K).symm.symm))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case refine_1.inr
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnramified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsUnmixed k φ

Tactic:
· rw [← star_star φ]; simpa [← congrArg conjugate hr] using h.isUnmixed_conjugate

Goal state after:
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 : IsUnmixed k φ
⊢ ComplexEmbedding.IsReal (mk φ).embedding ∨ ((mk φ).comap (algebraMap k K)).IsComplex

Tactic:
by_cases hv : ComplexEmbedding.IsReal (φ.comp (algebraMap k K))

Goal state after:
case pos
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnmixed k φ
hv : ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ ComplexEmbedding.IsReal (mk φ).embedding ∨ ((mk φ).comap (algebraMap k K)).IsComplex

case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnmixed k φ
hv : ¬ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ ComplexEmbedding.IsReal (mk φ).embedding ∨ ((mk φ).comap (algebraMap k K)).IsComplex
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ DiscreteTopology ↥(mixedEmbedding.integerLattice K)

Tactic:
by
  classical
  rw [← span_latticeBasis]
  infer_instance

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measure.map (⇑(toMixed K)) (stdOrthonormalBasis K).toBasis.addHaar = volume

Tactic:
Basis.map_addHaar,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ((stdOrthonormalBasis K).toBasis.map ↑(toMixed K)).addHaar = volume
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
⊢ MeasurableSet (A ∩ ⋂ w, {x | 0 < x.1 w})

Tactic:
refine hm.inter (MeasurableSet.iInter fun _ ↦ ?_)

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
x✝ : { w // w.IsReal }
⊢ MeasurableSet {x | 0 < x.1 x✝}
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ finrank ℚ K ≤ ⌊Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4)⌋₊

Tactic:
Nat.le_floor_iff

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ ↑(finrank ℚ K) ≤ Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4)

case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 0 ≤ Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4)
Module: Mathlib.NumberTheory.NumberField.ClassNumber

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑I).IsPrime →
      ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) →
        Submodule.IsPrincipal ↑I
I : ↥(Ideal (𝓞 K))⁰
hI : ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
⊢ (UniqueFactorizationMonoid.normalizedFactors ↑I).prod ∈ isPrincipalSubmonoid (𝓞 K)

Tactic:
refine Submonoid.multiset_prod_mem _ _ (fun J hJ ↦ mem_isPrincipalSubmonoid_iff.mp ?_)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑I).IsPrime →
      ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) →
        Submodule.IsPrincipal ↑I
I : ↥(Ideal (𝓞 K))⁰
hI : ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
J : Ideal (𝓞 K)
hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors ↑I
⊢ J ∈ isPrincipalSubmonoid (𝓞 K)
Module: Mathlib.NumberTheory.RamificationInertia.Unramified

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing T
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S T
inst✝⁸ : Algebra R T
inst✝⁷ : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst✝⁶ : P.LiesOver p
inst✝⁵ : p.IsPrime
inst✝⁴ : P.IsPrime
inst✝³ : IsUnramifiedAt R P
inst✝² : EssFiniteType R S
inst✝¹ : EssFiniteType R T
inst✝ : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this✝¹ : P.LiesOver p₀
this✝ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime p) := Localization.AtPrime.algebraOfLiesOver p₀ p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
⊢ IsUnramifiedAt R p

Tactic:
let := Localization.AtPrime.algebraOfLiesOver p₀ P

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing T
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S T
inst✝⁸ : Algebra R T
inst✝⁷ : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst✝⁶ : P.LiesOver p
inst✝⁵ : p.IsPrime
inst✝⁴ : P.IsPrime
inst✝³ : IsUnramifiedAt R P
inst✝² : EssFiniteType R S
inst✝¹ : EssFiniteType R T
inst✝ : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this✝² : P.LiesOver p₀
this✝¹ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime p) := Localization.AtPrime.algebraOfLiesOver p₀ p
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
this : Algebra (Localization.AtPrime p₀) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p₀ P
⊢ IsUnramifiedAt R p
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case refine_4
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ K = ℚ⟮↑↑x⟯

Tactic:
rw [← (IntermediateField.lift_injective _).eq_iff, eq_comm] at hx₁

Goal state after:
case refine_4
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max B 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : IntermediateField.lift ⊤ = IntermediateField.lift ℚ⟮↑x⟯
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(max B 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ K = ℚ⟮↑↑x⟯
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case hNN
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ ⊤ ≤ span R s ⊔ p • ⊤

Tactic:
rw [Ideal.smul_top_eq_map]

Goal state after:
case hNN
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ ⊤ ≤ span R s ⊔ Submodule.restrictScalars R pS
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case refine_4
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsComplex}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLT'Factor ↥K) * ↑(boundOfDiscBdd N)
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < √(1 + ↑(boundOfDiscBdd N) ^ 2)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ K = ℚ⟮↑↑x⟯

Tactic:
rw [← (IntermediateField.lift_injective _).eq_iff, eq_comm] at hx₁

Goal state after:
case refine_4
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈max (sqrt (1 + B ^ 2)) 1 ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsComplex}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLT'Factor ↥K) * ↑(boundOfDiscBdd N)
x : 𝓞 ↥K
hx₁ : IntermediateField.lift ⊤ = IntermediateField.lift ℚ⟮↑x⟯
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < √(1 + ↑(boundOfDiscBdd N) ^ 2)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ K = ℚ⟮↑↑x⟯
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ Prime (hζ.toInteger - 1)

Tactic:
by_cases htwo : p = 2

Goal state after:
case pos
p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p = 2
⊢ Prime (hζ.toInteger - 1)

case neg
p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p = 2
⊢ Prime (hζ.toInteger - 1)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case neg.hx
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p ^ (k + 1) = 2
this : NumberField K
H : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p ^ 1
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
exact prime_norm_toInteger_sub_one_of_prime_pow_ne_two hζ htwo

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

Goal state before:
pp: n : ℕ
hn : NeZero n
⊢ IsIntegralClosure (CyclotomicRing n ℤ ℚ) ℤ (CyclotomicField n ℚ)

Tactic:
have hζ := zeta_spec n ℚ (CyclotomicField n ℚ)
  refine ⟨IsFractionRing.injective _ _, fun {x} => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩
  · obtain ⟨y, rfl⟩ := (isIntegralClosure_adjoin_singleton hζ).isIntegral_iff.1 h
    refine adjoin_mono ?_ y.2
    simp only [Set.singleton_subset_iff, Set.mem_ofPred_eq]
    exact hζ.pow_eq_one
  · rintro ⟨y, rfl⟩
    exact IsIntegral.algebraMap ((IsCyclotomicExtension.integral {n} ℤ _).isIntegral _)

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : Additive (𝓞 K)ˣ
⊢ (logEmbedding K) (Additive.ofMul (Additive.toMul x)) = 0 ↔
    Additive.ofMul (Additive.toMul x) ∈ Subgroup.toAddSubgroup (torsion K)

Tactic:
logEmbedding_eq_zero_iff

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : Additive (𝓞 K)ˣ
⊢ Additive.toMul x ∈ torsion K ↔ Additive.ofMul (Additive.toMul x) ∈ Subgroup.toAddSubgroup (torsion K)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case e'_3
n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : NeZero n
ζ : K
hζ✝ : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot ⋯.unit n
⊢ n = orderOf ⟨↑⋯.unit, ?m.41⟩

Tactic:
Subgroup.orderOf_mk

Goal state after:
case e'_3
n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : NeZero n
ζ : K
hζ✝ : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot ⋯.unit n
⊢ n = orderOf ↑⋯.unit
Module: Mathlib.RingTheory.Fintype

Goal state before:
pp: case pos
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : Finite M₀
a : M₀
h : IsUnit a
⊢ orderOf h.unit < Nat.card M₀

Tactic:
exact orderOf_le_card.trans_lt <| natCard_units_lt M₀

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, λ ^ 2 ∣ ↑u - ↑n
⊢ u = 1 ∨ u = -1

Tactic:
replace hcong : ∃ n : ℤ, (3 : 𝓞 K) ∣ (↑u - n : 𝓞 K) := by
    obtain ⟨n, x, hx⟩ := hcong
    exact ⟨n, -η * x, by rw [← mul_assoc, mul_neg, ← neg_mul, ← lambda_sq, hx]⟩
  have := Units.mem hζ u
  fin_cases this
  · left; rfl
  · right; rfl
  all_goals exfalso
  · exact hζ.not_exists_int_prime_dvd_sub_of_prime_ne_two' (by decide) hcong
  · apply hζ.not_exists_int_prime_dvd_sub_of_prime_ne_two' (by decide)
    obtain ⟨n, x, hx⟩ := hcong
    rw [sub_eq_iff_eq_add] at hx
    refine ⟨-n, -x, sub_eq_iff_eq_add.2 ?_⟩
    simp only [Nat.cast_ofNat, mul_neg, Int.cast_neg, ← neg_add, ← hx, Units.val_neg,
      IsUnit.unit_spec, RingOfIntegers.neg_mk, neg_neg]
  · exact (hζ.pow_of_coprime 2 (by decide)).not_exists_int_prime_dvd_sub_of_prime_ne_two'
      (by decide) hcong
  · apply (hζ.pow_of_coprime 2 (by decide)).not_exists_int_prime_dvd_sub_of_prime_ne_two'
      (by decide)
    obtain ⟨n, x, hx⟩ := hcong
    refine ⟨-n, -x, sub_eq_iff_eq_add.2 ?_⟩
    have : (hζ.pow_of_coprime 2 (by decide)).toInteger = hζ.toInteger ^ 2 := by ext; simp
    simp only [this, Nat.cast_ofNat, mul_neg, Int.cast_neg, ← neg_add, ← sub_eq_iff_eq_add.1 hx,
      Units.val_neg, val_pow_eq_pow_val, IsUnit.unit_spec, neg_neg]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ DiscreteTopology ↥(unitLattice K)

Tactic:
refine discreteTopology_of_isOpen_singleton_zero ?_
  refine isOpen_singleton_of_finite_mem_nhds 0 (s := Metric.closedBall 0 1) ?_ ?_
  · exact Metric.closedBall_mem_nhds _ (by simp)
  · refine Set.Finite.of_finite_image ?_ (Set.injOn_of_injective Subtype.val_injective)
    convert! unitLattice_inter_ball_finite K 1
    ext x
    refine ⟨?_, fun ⟨hx1, hx2⟩ ↦ ⟨⟨x, hx1⟩, hx2, rfl⟩⟩
    rintro ⟨x, hx, rfl⟩
    exact ⟨Subtype.mem x, hx⟩

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

Goal state before:
pp: a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
rcases cube_of_not_dvd hdvd.1.1 with ha | ha <;>
  rcases cube_of_not_dvd hdvd.1.2 with hb | hb <;>
  rcases cube_of_not_dvd hdvd.2 with hc | hc <;>
  rw [ha, hb, hc] <;> decide

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : x * y⁻¹ * (x * y⁻¹) = ↑a
⊢ legendreSym p a = 1

Tactic:
exact (eq_one_iff p ha).mpr ⟨x * y⁻¹, hxy.symm⟩

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ ¬(quadraticChar F) a = 1 ↔ ¬IsSquare a

Tactic:
quadraticChar_one_iff_isSquare ha

Goal state after:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ ¬IsSquare a ↔ ¬IsSquare a