mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ |(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| = absNorm I

Tactic:
let b₀ : Basis ι ℚ K := b.localizationLocalization ℚ ℤ⁰ K

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
⊢ |(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| = absNorm I
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl.right.inl.right
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos✝ : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_pos : z = m ^ 2 + n ^ 2
⊢ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ -m

Tactic:
apply And.intro ht4

Goal state after:
case h.inl.right.inl.right
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos✝ : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_pos : z = m ^ 2 + n ^ 2
⊢ 0 ≤ -m
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ #{φ | mkComplex φ = ⟨w, hw⟩} = #{φ | mk φ = w}

Tactic:
rw [← Fintype.card_subtype, ← Fintype.card_subtype]

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

Goal state before:
pp: K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
E : Subfield K
h : E ≤ maximalRealSubfield K
x✝ : Algebra ↥E ↥(maximalRealSubfield K) := (Subfield.inclusion h).toAlgebra
this : IsScalarTower (↥E) (↥(maximalRealSubfield K)) K
⊢ IsTotallyReal ↥E

Tactic:
have : Algebra.IsAlgebraic E (maximalRealSubfield K) :=
      Algebra.IsAlgebraic.tower_bot E (maximalRealSubfield K) K

Goal state after:
K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
E : Subfield K
h : E ≤ maximalRealSubfield K
x✝ : Algebra ↥E ↥(maximalRealSubfield K) := (Subfield.inclusion h).toAlgebra
this✝ : IsScalarTower (↥E) (↥(maximalRealSubfield K)) K
this : Algebra.IsAlgebraic ↥E ↥(maximalRealSubfield K)
⊢ IsTotallyReal ↥E
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : 0 ≤ r
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
· lift r to NNReal using hr
    simp_rw [← coe_nnnorm, nnnorm_eq, NNReal.coe_le_coe, Finset.sup_le_iff, Finset.mem_univ,
      forall_true_left]

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.comp f)).embedding = w.embedding.comp f

Tactic:
embedding_mk_eq_of_isReal
    (by rwa [← isReal_mk_iff, ← comap_mk, 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.embedding.comp f = w.embedding.comp f
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ Nontrivial (mixedSpace K)

pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ Nontrivial (mixedSpace K)

Tactic:
· have : Nonempty {w : InfinitePlace K // IsReal w} := ⟨⟨w, hw⟩⟩
    exact nontrivial_prod_left

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ Nontrivial (mixedSpace K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding.latticeBasis K))
h_zero : (commMap K) x = 0
⊢ x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))

Tactic:
refine (Submodule.span_mono ?_) h_mem

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding.latticeBasis K))
h_zero : (commMap K) x = 0
⊢ Set.range ⇑(canonicalEmbedding.latticeBasis K) ⊆ Set.range ⇑(canonicalEmbedding K)
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 : IsRamified k w
⊢ (w.comap (algebraMap k K)).embedding = w.embedding.comp (algebraMap k K)

Tactic:
by
  rw [← comap_embedding_of_isReal _ (isRamified_iff.1 h).2]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
x✝ : mixedSpace K
⊢ convexBodySumFun x✝ ≤ 0 ↔ x✝ = 0

Tactic:
← convexBodySumFun_eq_zero_iff

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
x✝ : mixedSpace K
⊢ convexBodySumFun x✝ ≤ 0 ↔ convexBodySumFun x✝ = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) =
    ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * volume (fundamentalDomain (latticeBasis K))

Tactic:
let e : (Module.Free.ChooseBasisIndex ℤ I) ≃ (Module.Free.ChooseBasisIndex ℤ (𝓞 K)) := by
    refine Fintype.equivOfCardEq ?_
    rw [← finrank_eq_card_chooseBasisIndex, ← finrank_eq_card_chooseBasisIndex,
      fractionalIdeal_rank]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ ↥↑↑I ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
⊢ volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) =
    ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * volume (fundamentalDomain (latticeBasis 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))
⊢ minkowskiBound K I = ↑(convexBodySumFactor K) * ENNReal.ofReal (B ^ finrank ℚ K)

Tactic:
← Real.rpow_natCast,

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))
⊢ minkowskiBound K I = ↑(convexBodySumFactor K) * ENNReal.ofReal (B ^ ↑(finrank ℚ K))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case inr
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : ψ ∈ unmixedEmbeddingsOver L v.embedding
hψ : (mk ψ).embedding = conjugate ψ
⊢ v.embeddingConjugateIte (mk ψ) = ψ

Tactic:
simpa [embeddingConjugateIte, hψ] using fun ⟨_⟩ ↦
      h.2.isReal_iff_isReal.1 <| by have := h.1.over; aesop

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

Goal state before:
pp: case pos.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ : |(w₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ |(w₀.embedding ↑a).im| < ↑B

Tactic:
← NNReal.sq_sqrt B

Goal state after:
case pos.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ : |(w₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B ^ 2)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case fst
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
⊢ ((negAt s).symm x).1 w = ((negAt s) x).1 w

pp: case snd
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsComplex }
⊢ ((negAt s).symm x).2 w = ((negAt s) x).2 w

Tactic:
· by_cases hw : w ∈ s
    · simp_rw [negAt_apply_isReal_and_mem _ hw, negAt, prodCongr_symm,
        prodCongr_apply, piCongrRight_symm_apply, if_pos hw, symm_neg,
        ContinuousLinearEquiv.neg_apply]
    · simp_rw [negAt_apply_isReal_and_notMem _ hw, negAt, prodCongr_symm,
        prodCongr_apply, piCongrRight_symm_apply, if_neg hw, refl_symm,
        refl_apply]

Goal state after:
case snd
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsComplex }
⊢ ((negAt s).symm x).2 w = ((negAt s) x).2 w
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
p : Ideal A
P Q : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
hQp : Q.IsPrime
inst✝⁴ : Q.LiesOver p
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
⊢ P.ramificationIdx A = Q.ramificationIdx A

Tactic:
rcases exists_smul_eq_of_isGaloisGroup p P Q G with ⟨σ, rfl⟩
  rw [ramificationIdx_smul]

Goal state after:
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
⊢ 0 ≤ Real.log (9 / 4 * ↑N) / Real.log (3 * π / 4)

Tactic:
· refine div_nonneg (Real.log_nonneg ?_) (Real.log_nonneg (le_of_lt h₂))
      rw [mul_comm, ← mul_div_assoc, _root_.le_div_iff₀ (by positivity), one_mul,
        ← _root_.div_le_iff₀ (by positivity)]
      exact le_trans (by norm_num) (Nat.one_le_cast.mpr (Nat.one_le_iff_ne_zero.mpr h_nz))

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.IsPrime
inst✝¹⁴ : P.LiesOver p
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : Finite G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : IsGaloisGroup G A B
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : IsDomain C
inst✝⁷ : Algebra A C
inst✝⁶ : Algebra B C
inst✝⁵ : FaithfulSMul B C
inst✝⁴ : IsScalarTower A B C
GAC : Type u_5
inst✝³ : Group GAC
inst✝² : Finite GAC
inst✝¹ : MulSemiringAction GAC C
inst✝ : IsGaloisGroup GAC A C
this✝¹ : Algebra.IsIntegral A C
this✝ : Algebra.IsIntegral B C
f : GAC →* G := restrictHom GAC G A B C
H : Subgroup GAC := Subgroup.comap f (stabilizer G P)
key : ∀ (Q Q' : Ideal C) [Q.LiesOver P] [Q'.LiesOver P] (g : GAC), g • Q = Q' → g ∈ H
Q : Ideal C
left✝ : Q.IsPrime
right✝ : Q.LiesOver P
this : Q.LiesOver p
⊢ orbit (↥H) Q = P.primesOver C

Tactic:
ext Q'

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝¹⁵ : P.IsPrime
inst✝¹⁴ : P.LiesOver p
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : Finite G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : IsGaloisGroup G A B
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : IsDomain C
inst✝⁷ : Algebra A C
inst✝⁶ : Algebra B C
inst✝⁵ : FaithfulSMul B C
inst✝⁴ : IsScalarTower A B C
GAC : Type u_5
inst✝³ : Group GAC
inst✝² : Finite GAC
inst✝¹ : MulSemiringAction GAC C
inst✝ : IsGaloisGroup GAC A C
this✝¹ : Algebra.IsIntegral A C
this✝ : Algebra.IsIntegral B C
f : GAC →* G := restrictHom GAC G A B C
H : Subgroup GAC := Subgroup.comap f (stabilizer G P)
key : ∀ (Q Q' : Ideal C) [Q.LiesOver P] [Q'.LiesOver P] (g : GAC), g • Q = Q' → g ∈ H
Q : Ideal C
left✝ : Q.IsPrime
right✝ : Q.LiesOver P
this : Q.LiesOver p
Q' : Ideal C
⊢ Q' ∈ orbit (↥H) Q ↔ Q' ∈ P.primesOver C
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case refine_2.refine_1
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)
i : ℕ
⊢ ↑|(minpoly ℤ ↑x).coeff i| = ‖↑((minpoly ℤ ((algebraMap (𝓞 ↥K) ↥K) x)).coeff i)‖

Tactic:
Int.norm_cast_rat,

Goal state after:
case refine_2.refine_1
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)
i : ℕ
⊢ ↑|(minpoly ℤ ↑x).coeff i| = ‖(minpoly ℤ ((algebraMap (𝓞 ↥K) ↥K) x)).coeff i‖
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
⊢ IsPrincipalIdealRing (𝓞 K)

Tactic:
refine isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime <|
    fun ⟨P, HP⟩ hP hPN ↦ ?_

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)|)
⊢ Submodule.IsPrincipal ↑⟨P, HP⟩
Module: Mathlib.NumberTheory.RamificationInertia.Unramified

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain R
inst✝³ : IsDomain S
inst✝² : Module.IsTorsionFree R S
inst✝¹ : CharZero R
inst✝ : Algebra.IsIntegral R S
⊢ IsUnramifiedAt R ⊥

Tactic:
have : IsFractionRing S (Localization.AtPrime (⊥ : Ideal S)) := by
    simpa [Ideal.primeCompl_bot] using Localization.isLocalization (M := (⊥ : Ideal S).primeCompl)
  let : Field (Localization.AtPrime (⊥ : Ideal S)) := IsFractionRing.toField S
  have : FaithfulSMul R (Localization.AtPrime (⊥ : Ideal S)) := by
    rw [faithfulSMul_iff_algebraMap_injective,
      IsScalarTower.algebraMap_eq R S (Localization.AtPrime ⊥)]
    exact (IsFractionRing.injective S _).comp (FaithfulSMul.algebraMap_injective R S)
  let := FractionRing.liftAlgebra R (Localization.AtPrime (⊥ : Ideal S))
  have : Algebra.IsAlgebraic (FractionRing R) (Localization.AtPrime ⊥) :=
    isAlgebraic_of_isFractionRing R S (FractionRing R) (Localization.AtPrime (⊥ : Ideal S))
  have : FormallyUnramified (FractionRing R) (Localization.AtPrime (⊥ : Ideal S)) :=
    FormallyUnramified.of_isSeparable _ _
  exact FormallyUnramified.comp R (FractionRing R) (Localization.AtPrime ⊥)

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

Goal state before:
pp: case refine_2.refine_1
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)
i : ℕ
⊢ ↑|(minpoly ℤ ↑x).coeff i| = ‖↑((minpoly ℤ ((algebraMap (𝓞 ↥K) ↥K) x)).coeff i)‖

Tactic:
Int.norm_cast_rat,

Goal state after:
case refine_2.refine_1
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)
i : ℕ
⊢ ↑|(minpoly ℤ ↑x).coeff i| = ‖(minpoly ℤ ((algebraMap (𝓞 ↥K) ↥K) x)).coeff i‖
Module: Mathlib.RingTheory.DedekindDomain.Instances

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
inst✝¹¹ : Algebra R Rₘ
inst✝¹⁰ : IsTorsionFree R S
inst✝⁹ : Algebra.IsSeparable K L
M : Submonoid R
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra (FractionRing Rₘ) (FractionRing Sₘ)
inst✝ : IsScalarTower Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := algebraMapSubmonoid S M
hM' : algebraMapSubmonoid S M ≤ S⁰
f₁ : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
f₂ : Sₘ →+* L := IsLocalization.map L (RingHom.id S) hM'
algInst✝¹ : Algebra Rₘ K := f₁.toAlgebra
algInst✝ : Algebra Sₘ L := f₂.toAlgebra
this✝ : IsScalarTower R Rₘ K
this : IsScalarTower S Sₘ L
⊢ Algebra.IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)

Tactic:
have := isFractionRing_of_isDomain_of_isLocalization M Rₘ K

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
inst✝¹¹ : Algebra R Rₘ
inst✝¹⁰ : IsTorsionFree R S
inst✝⁹ : Algebra.IsSeparable K L
M : Submonoid R
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra (FractionRing Rₘ) (FractionRing Sₘ)
inst✝ : IsScalarTower Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := algebraMapSubmonoid S M
hM' : algebraMapSubmonoid S M ≤ S⁰
f₁ : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
f₂ : Sₘ →+* L := IsLocalization.map L (RingHom.id S) hM'
algInst✝¹ : Algebra Rₘ K := f₁.toAlgebra
algInst✝ : Algebra Sₘ L := f₂.toAlgebra
this✝¹ : IsScalarTower R Rₘ K
this✝ : IsScalarTower S Sₘ L
this : IsFractionRing Rₘ K
⊢ Algebra.IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
Module: Mathlib.RingTheory.DedekindDomain.Instances

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✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : IsDomain T
inst✝² : Algebra R S
P : Ideal R
inst✝¹ : P.IsPrime
inst✝ : FaithfulSMul R S
⊢ IsScalarTower Rₚ Sₚ L

Tactic:
refine IsScalarTower.of_algebraMap_eq' <| IsLocalization.ringHom_ext P.primeCompl ?_
  rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq R Rₚ Sₚ, IsScalarTower.algebraMap_eq R S Sₚ,
    ← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq S Sₚ L, IsScalarTower.algebraMap_eq Rₚ K L,
    RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
    ← IsScalarTower.algebraMap_eq]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case inl
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊥
⊢ spanNorm R (I * J) ≤ spanNorm R I * spanNorm R J

Tactic:
rw [hI, spanNorm_eq_bot_iff.mp hI, bot_mul, spanNorm_bot]
    exact bot_le

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
hJ : spanNorm R J = ⊤
⊢ spanNorm R (I * J) ≤ spanNorm R J

Tactic:
hJ

Goal state after:
case inr.inr
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
hJ : spanNorm R J = ⊤
⊢ spanNorm R (I * J) ≤ ⊤