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

Goal state before:
pp: case hf
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ Function.Even fun n ↦ (↑n ^ k)⁻¹

Tactic:
intro n

Goal state after:
case hf
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
n : ℤ
⊢ (fun n ↦ (↑n ^ k)⁻¹) (-n) = (fun n ↦ (↑n ^ k)⁻¹) n
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: case pos
r : ℝ
h : r < -1
⊢ (Summable fun p ↦ ↑↑p ^ r) ↔ r < -1

Tactic:
simp only [h, iff_true]

Goal state after:
case pos
r : ℝ
h : r < -1
⊢ Summable fun p ↦ ↑↑p ^ r
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: N : ℕ
hn : N ≠ 0
χ : DirichletCharacter ℂ N
⊢ (abscissaOfAbsConv fun n ↦ χ ↑n) = 1

Tactic:
by
  simpa [abscissaOfAbsConv, LSeriesSummable_iff hn χ, Set.Ioi_def, EReal.image_coe_Ioi]
    using csInf_Ioo <| EReal.coe_lt_top 1

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

Goal state before:
pp: case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n ↦ χ ↑n) s
hs' : (abscissaOfAbsConv fun n ↦ χ ↑n) < ↑s.re
hΛ : LSeriesSummable ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ Complex.log ↑n) s = - -L (logMul fun n ↦ χ ↑n) s

Tactic:
neg_neg

Goal state after:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n ↦ χ ↑n) s
hs' : (abscissaOfAbsConv fun n ↦ χ ↑n) < ↑s.re
hΛ : LSeriesSummable ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ Complex.log ↑n) s = L (logMul fun n ↦ χ ↑n) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case h
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ∀ (i : ℕ), ‖2 * ↑i * Real.sin (2 * π * a * ↑i) * rexp (-π * ↑i ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 1 0 t i

Tactic:
intro n

Goal state after:
case h
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖2 * ↑n * Real.sin (2 * π * a * ↑n) * rexp (-π * ↑n ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 1 0 t n
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case e'_1
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ ↑(x.gcd y) ∣ x

Tactic:
exact Int.gcd_dvd_left ..

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
⊢ Function.support f ⊆ {n | IsPrimePow n}

Tactic:
intro n

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
n : ℕ
⊢ n ∈ Function.support f → n ∈ {n | IsPrimePow n}
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:
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 : Prime a
n : ℕ
hn : n ≠ 0
⊢ radical (a ^ n) = normalize a

Tactic:
radical_pow a hn

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : Prime a
n : ℕ
hn : n ≠ 0
⊢ radical a = normalize a
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
⊢ w.natDegree < a.natDegree + b.natDegree

Tactic:
wab

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : a.wronskian b ≠ 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
⊢ (a.wronskian b).natDegree < a.natDegree + b.natDegree
Module: Mathlib.RingTheory.Radical.Basic

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

Tactic:
intro n

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
⊢ ∀ (x : M), radical a ∣ x ^ n → radical a ∣ x
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
⊢ ∀ (x : M), radical a ∣ x ^ n → radical a ∣ x

Tactic:
p

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
p : M
⊢ radical a ∣ p ^ n → radical a ∣ p
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ a ^ 4 + b ^ 4 ≠ c ^ 2

Tactic:
intro h
  obtain ⟨a0, b0, c0, ⟨hf, h2, hp⟩⟩ :=
    Fermat42.exists_pos_odd_minimal (And.intro ha (And.intro hb h))
  apply Fermat42.not_minimal hf h2 hp

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

Goal state before:
pp: hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
⊢ FermatLastTheorem

Tactic:
intro n

Goal state after:
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
⊢ n ≥ 3 → FermatLastTheoremFor n
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
have hsum' : b + c + a = 0 := by rwa [add_rotate] at hsum

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
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
ch0 : ringChar k = 0
da : derivative a = 0
⊢ ∀ (n : ℕ), ↑n = 0 → n = 0

Tactic:
intro n

Goal state after:
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
ch0 : ringChar k = 0
da : derivative a = 0
n : ℕ
⊢ ↑n = 0 → n = 0
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v₁ v₂ : InfinitePlace K
h : v₁.embedding = ComplexEmbedding.conjugate v₂.embedding
⊢ mk v₂.embedding = v₂

Tactic:
mk_embedding

Goal state after:
K : Type u_1
inst✝ : Field K
v₁ v₂ : InfinitePlace K
h : v₁.embedding = ComplexEmbedding.conjugate v₂.embedding
⊢ v₂ = v₂
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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

Tactic:
dist_eq_norm,

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
⊢ mk φ = mk (mk φ).embedding

Tactic:
mk_embedding

Goal state after:
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
⊢ mk φ = mk φ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : mixedSpace K
hx : x ∈ convexBodyLT K f
⊢ -x ∈ convexBodyLT K f

Tactic:
simp only [Set.mem_prod, Prod.fst_neg, Set.mem_pi, Set.mem_univ, Pi.neg_apply,
    mem_ball_zero_iff, norm_neg, Real.norm_eq_abs, forall_true_left, Subtype.forall,
    Prod.snd_neg] at hx ⊢

Goal state after:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : mixedSpace K
hx :
  (∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex), ‖x.2 ⟨a, b⟩‖ < ↑(f a)
⊢ (∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex), ‖x.2 ⟨a, b⟩‖ < ↑(f a)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ volume (convexBodyLT K f) = (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) * ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi

Tactic:
simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball, Complex.volume_ball]

Goal state after:
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 }
⊢ Convex ℝ (convexBodyLT' K f w₀)

Tactic:
by
  refine Convex.prod (convex_pi (fun _ _ => convex_ball _ _)) (convex_pi (fun _ _ => ?_))
  split_ifs
  · simp_rw [abs_lt]
    refine Convex.inter ((convex_halfSpace_re_gt _).inter (convex_halfSpace_re_lt _))
      ((convex_halfSpace_im_gt _).inter (convex_halfSpace_im_lt _))
  · exact convex_ball _ _

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 : (w.comap f).IsReal
⊢ ((mk w.embedding).comap f).IsReal

Tactic:
mk_embedding

Goal state after:
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h : (w.comap f).IsReal
⊢ (w.comap f).IsReal
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : w₁.embedding = conjugate w₂.embedding
⊢ mk w₂.embedding = w₂

Tactic:
mk_embedding

Goal state after:
case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : w₁.embedding = conjugate w₂.embedding
⊢ w₂ = w₂
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
hw : ((mk w.embedding).comap (algebraMap k K)).IsReal
⊢ ComplexEmbedding.IsReal w.embedding

Tactic:
mk_embedding

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
hw : (w.comap (algebraMap k K)).IsReal
⊢ ComplexEmbedding.IsReal w.embedding
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
hw : ((mk w.embedding).comap (algebraMap k K)).IsReal
⊢ ComplexEmbedding.IsReal (conjugate w.embedding)

Tactic:
mk_embedding

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
hw : (w.comap (algebraMap k K)).IsReal
⊢ ComplexEmbedding.IsReal (conjugate w.embedding)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ volume (convexBodySum K B) = ↑(convexBodySumFactor K) * ENNReal.ofReal B ^ finrank ℚ K

Tactic:
rw [mul_comm]
      convert! addHaar_smul volume B (convexBodySum K 1)
      · simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hB), Set.preimage_ofPred_eq, convexBodySumFun,
        normAtPlace_smul, abs_inv, abs_eq_self.mpr (le_of_lt hB), ← mul_assoc, mul_comm, mul_assoc,
        ← Finset.mul_sum, inv_mul_le_iff₀ hB, mul_one]
      · rw [abs_pow, ofReal_pow (abs_nonneg _), abs_eq_self.mpr (le_of_lt hB),
          mixedEmbedding.finrank]
      · exact this.symm

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)ᵀ
⊢ ‖I‖₊ = 1

Tactic:
rw [← norm_toNNReal, norm_I, Real.toNNReal_one]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (2⁻¹ * I) ^ #univ = (2⁻¹ * I) ^ Fintype.card { w // w.IsComplex }

Tactic:
Fintype.card

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (2⁻¹ * I) ^ #univ = (2⁻¹ * I) ^ #univ
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
⊢ ↑(FractionalIdeal.absNorm ↑I) * 2 ^ (-↑(nrComplexPlaces K)) * √‖discr K‖ * 2 ^ ↑(finrank ℚ K) *
      (↑(finrank ℚ K).factorial *
        (2 ^ (-↑(nrRealPlaces K)) * (π ^ (-↑(nrComplexPlaces K)) * 2 ^ ↑(nrComplexPlaces K)))) =
    ↑(FractionalIdeal.absNorm ↑I) *
            2 ^ (↑(finrank ℚ K) + -↑(nrComplexPlaces K) + -↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π ^ (-↑(nrComplexPlaces K))

Tactic:
zpow_add₀ (two_ne_zero : (2 : ℝ) ≠ 0)

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
⊢ ↑(FractionalIdeal.absNorm ↑I) * 2 ^ (-↑(nrComplexPlaces K)) * √‖discr K‖ * 2 ^ ↑(finrank ℚ K) *
      (↑(finrank ℚ K).factorial *
        (2 ^ (-↑(nrRealPlaces K)) * (π ^ (-↑(nrComplexPlaces K)) * 2 ^ ↑(nrComplexPlaces K)))) =
    ↑(FractionalIdeal.absNorm ↑I) *
            (2 ^ ↑(finrank ℚ K) * 2 ^ (-↑(nrComplexPlaces K)) * 2 ^ (-↑(nrRealPlaces K)) * 2 ^ ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π ^ (-↑(nrComplexPlaces K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
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 : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K

Tactic:
refine ⟨a, ha, by simpa using h_nz, ?_⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
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 : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
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 : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ ↑|(Algebra.norm ℚ) a| ^ (↑(finrank ℚ K))⁻¹ ≤ (B / ↑(finrank ℚ K)) ^ 1

Tactic:
rpow_one,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
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 : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ ↑|(Algebra.norm ℚ) a| ^ (↑(finrank ℚ K))⁻¹ ≤ B / ↑(finrank ℚ K)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
⊢ ∀ (n : ℕ), 2 ≤ n → 4 / 9 * (3 * π / 4) ^ n ≤ a n

Tactic:
intro n

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n : ℕ
⊢ 2 ≤ n → 4 / 9 * (3 * π / 4) ^ n ≤ a n
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case e'_2
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F // p F }
T : Set A
hT : Finite ↑T
h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯
x✝¹ x✝ : ↑S
h_eq :
  (fun x ↦
        match x with
        | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩)
      x✝¹ =
    (fun x ↦
        match x with
        | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩)
      x✝
⊢ ↑↑x✝¹ = ℚ⟮⋯.choose⟯

pp: case e'_3
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F // p F }
T : Set A
hT : Finite ↑T
h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯
x✝¹ x✝ : ↑S
h_eq :
  (fun x ↦
        match x with
        | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩)
      x✝¹ =
    (fun x ↦
        match x with
        | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩)
      x✝
⊢ ↑↑x✝ = ℚ⟮⋯.choose⟯

Tactic:
all_goals exact (h _ (Subtype.mem _)).choose_spec.2

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
I : Ideal R
hI : ¬I = 0
x : R
hx₁ : x ∈ I
hx₂ : x ≠ 0
⊢ Ideal.span {x} ≠ ⊥

Tactic:
simp [hx₂]

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Group G
inst✝⁶ : MulSemiringAction G S
inst✝⁵ : IsGaloisGroup G R S
inst✝⁴ : Finite G
p : Ideal R
inst✝³ : p.IsPrime
P : Ideal S
inst✝² : P.LiesOver p
inst✝¹ : P.IsPrime
inst✝ : PerfectField p.ResidueField
⊢ (p.primesOver S).ncard * Nat.card ↥(inertia G P) * P.inertiaDeg R = Nat.card G

Tactic:
by
  rw [mul_assoc, ← card_stabilizer_eq_card_inertia_mul_finrank p P,
    ← IsInvariant.orbit_eq_primesOver R S G p P]
  simpa using Nat.card_congr (MulAction.orbitProdStabilizerEquivGroup G P)

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Group G
inst✝¹⁰ : MulSemiringAction G S
inst✝⁹ : IsGaloisGroup G R S
inst✝⁸ : Finite G
inst✝⁷ : IsDomain R
inst✝⁶ : IsDomain S
inst✝⁵ : Module.Finite R S
inst✝⁴ : Flat R S
p : Ideal R
P : Ideal S
inst✝³ : P.LiesOver p
inst✝² : p.IsPrime
inst✝¹ : P.IsPrime
inst✝ : PerfectField p.ResidueField
H : (p.primesOver S).ncard * Nat.card ↥(inertia G P) * p.inertiaDegIn S = Nat.card G
h1 : (p.primesOver S).ncard ≠ 0
h2 : p.inertiaDegIn S ≠ 0
⊢ Nat.card ↥(inertia G P) = p.ramificationIdxIn S

Tactic:
rwa [← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn p S G,
    mul_assoc, mul_right_inj' h1, mul_left_inj' h2] at H

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

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

Tactic:
rw [← classNumber_eq_one_iff, classNumber, Fintype.card_eq_one_iff]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) →
      Submodule.IsPrincipal ↑I
⊢ ∃ x, ∀ (y : ClassGroup (𝓞 K)), y = x
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case hs
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
I J : FractionalIdeal M K
i : K
hi : i ∈ I
j : K
hj : j ∈ J
hy : i + j ∈ ↑(I + J)
⊢ (IsLocalization.map L f hf) i + (IsLocalization.map L f hf) j ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' (↑I ∪ ↑J)))

Tactic:
exact add_mem (Submodule.subset_span ⟨i, Set.mem_union_left _ hi, by simp⟩)
      (Submodule.subset_span ⟨j, Set.mem_union_right _ hj, by simp⟩)

Goal state after: