mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card { φ // ComplexEmbedding.IsReal φ } + Fintype.card { φ // ¬ComplexEmbedding.IsReal φ } =
    Fintype.card (K →+* ℂ)

Tactic:
Fintype.card_subtype_compl,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card { φ // ComplexEmbedding.IsReal φ } +
      (Fintype.card (K →+* ℂ) - Fintype.card { x // ComplexEmbedding.IsReal x }) =
    Fintype.card (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
F : Type u_3
inst✝² : Field F
inst✝¹ : Algebra k K
inst✝ : Algebra k F
w : InfinitePlace F
h : IsUnramified k w
f : K →ₐ[k] F
⊢ IsUnramified k (w.comap ↑f)

Tactic:
rw [InfinitePlace.isUnramified_iff_mult_le, ← InfinitePlace.comap_comp, f.comp_algebraMap, h.eq]
  exact InfinitePlace.mult_comap_le _ _

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

Goal state before:
pp: case refine_1.fst
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = 0
w : { w // w.IsReal }
⊢ x.1 w = 0.1 w

Tactic:
exact norm_eq_zero.mp (normAtPlace_apply_of_isReal w.prop _ ▸ h w.1)

Goal state after:
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 : ∫ (x : mixedSpace K), rexp (-convexBodySumFun x) = 2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K
⊢ ENNReal.ofReal (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K) / ↑(finrank ℚ K).factorial =
    ↑(2 ^ nrRealPlaces K * (NNReal.pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)

Tactic:
ofReal_mul (by positivity),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : ∫ (x : mixedSpace K), rexp (-convexBodySumFun x) = 2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K
⊢ ENNReal.ofReal (2 ^ nrRealPlaces K) * ENNReal.ofReal ((π / 2) ^ nrComplexPlaces K) / ↑(finrank ℚ K).factorial =
    ↑(2 ^ nrRealPlaces K * (NNReal.pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)
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 (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal

pp: case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
⊢ ↑(finrank ℚ K) ≠ 0

Tactic:
ofReal_toReal,

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) * (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹)

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)⁻¹ ≠ ∞

case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
⊢ ↑(finrank ℚ K) ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : LinearIndependent ℝ (⇑(commMap K) ∘ ⇑(canonicalEmbedding.latticeBasis K))
⊢ Fintype.card (K →+* ℂ) =
    Fintype.card { φ // ComplexEmbedding.IsReal φ } + Fintype.card { φ // ¬ComplexEmbedding.IsReal φ }

Tactic:
Fintype.card_subtype_compl,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : LinearIndependent ℝ (⇑(commMap K) ∘ ⇑(canonicalEmbedding.latticeBasis K))
⊢ Fintype.card (K →+* ℂ) =
    Fintype.card { φ // ComplexEmbedding.IsReal φ } +
      (Fintype.card (K →+* ℂ) - Fintype.card { x // ComplexEmbedding.IsReal x })
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : LinearIndependent ℝ (⇑(commMap K) ∘ ⇑(canonicalEmbedding.latticeBasis K))
⊢ Fintype.card (ChooseBasisIndex ℤ (𝓞 K)) = finrank ℝ (mixedSpace K)

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

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
⊢ ((latticeBasis K).repr ((mixedEmbedding K) x)) i = ↑(((integralBasis K).repr x) i)

Tactic:
← Basis.restrictScalars_repr_apply ℚ _ ⟨_, mem_rat_span_latticeBasis K x⟩,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
⊢ (algebraMap ℚ ℝ) (((Basis.restrictScalars ℚ (latticeBasis K)).repr ⟨(mixedEmbedding K) x, ⋯⟩) i) =
    ↑(((integralBasis K).repr x) i)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
⊢ (unramifiedPlacesOver L v).ncard + 2 * (ramifiedPlacesOver L v).ncard = finrank K L

Tactic:
classical
  let : Algebra K ℂ := v.embedding.toAlgebra
  rw [← AlgHom.card K L ℂ, ramifiedPlacesOver_ncard, unramifiedPlacesOver_ncard,
    ← Set.ncard_union_eq (disjoint_unmixedEmbeddingsOver_mixedEmbeddingsOver L v.embedding),
    union_unmixedEmbeddingsOver_mixedEmbeddingsOver, Set.ncard_eq_toFinset_card]
  apply (card_nbij AlgHom.toRingHom (fun σ _ ↦ by simpa using ⟨by aesop⟩)
    AlgHom.coe_ringHom_injective.injOn (fun ψ hψ ↦ ?_)).symm
  simp only [Set.Finite.toFinset_ofPred, coe_filter, mem_univ, true_and, Set.mem_ofPred_eq] at hψ
  exact ⟨⟨ψ, fun _ ↦ by simp [RingHom.algebraMap_toAlgebra, ← hψ.over]⟩, by simp⟩

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
⊢ ((∃ i, x ∈ ⇑(negAt i) '' plusPart A) ∨ x ∈ A ∧ ∃ i, x ∈ {x | x.1 i = 0}) → x ∈ A

Tactic:
rintro (⟨s, ⟨x, ⟨hx, _⟩, rfl⟩⟩ | h)

Goal state after:
case refine_1.inl
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
s : Set { w // w.IsReal }
x : mixedSpace K
hx : x ∈ A
right✝ : x ∈ {x | ∀ (w : { w // w.IsReal }), 0 < x.1 w}
⊢ (negAt s) x ∈ A

case refine_1.inr
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ A ∧ ∃ i, x ∈ {x | x.1 i = 0}
⊢ x ∈ A
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 : Ideal B
hPp : P.IsPrime
hp : 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✝¹² : Algebra A C
inst✝¹¹ : Algebra B C
inst✝¹⁰ : Nonempty ↑(P.primesOver 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
GBC : Type u_6
inst✝⁴ : Group GBC
inst✝³ : Finite GBC
inst✝² : MulSemiringAction GBC C
inst✝¹ : IsGaloisGroup GBC B C
inst✝ : Flat B C
Q : Ideal C
left✝ : Q.IsPrime
hQ : Q.LiesOver P
this : Q.LiesOver p
⊢ P.ramificationIdx A * P.ramificationIdxIn C = Q.ramificationIdx A

Tactic:
ramificationIdxIn_eq_ramificationIdx P Q GBC,

Goal state after:
A : Type u_1
B : Type u_2
inst✝²⁰ : CommRing A
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : 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✝¹² : Algebra A C
inst✝¹¹ : Algebra B C
inst✝¹⁰ : Nonempty ↑(P.primesOver 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
GBC : Type u_6
inst✝⁴ : Group GBC
inst✝³ : Finite GBC
inst✝² : MulSemiringAction GBC C
inst✝¹ : IsGaloisGroup GBC B C
inst✝ : Flat B C
Q : Ideal C
left✝ : Q.IsPrime
hQ : Q.LiesOver P
this : Q.LiesOver p
⊢ P.ramificationIdx A * Q.ramificationIdx B = Q.ramificationIdx A
Module: Mathlib.NumberTheory.NumberField.ClassNumber

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
a : 𝓞 K
ha : a ∈ ↑↑J
h_nz : (Algebra.linearMap (𝓞 K) K) a ≠ 0
h_nm :
  ↑|(Algebra.norm ℚ) ((Algebra.linearMap (𝓞 K) K) a)| ≤
    ↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K)! /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
I₀ : Ideal (𝓞 K)
hI : span {a} = ↑J * I₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ := ⟨I₀, ⋯⟩
⊢ ↑(absNorm ↑I) ≤ (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)

Tactic:
· rw [← FractionalIdeal.absNorm_span_singleton (𝓞 K), Algebra.linearMap_apply,
      ← FractionalIdeal.coeIdeal_span_singleton, FractionalIdeal.coeIdeal_absNorm, hI, map_mul,
      cast_mul, Rat.cast_mul, absNorm_apply, Rat.cast_natCast, Rat.cast_natCast,
      FractionalIdeal.coe_mk0, FractionalIdeal.coeIdeal_absNorm, Rat.cast_natCast, mul_div_assoc,
      mul_assoc, mul_assoc] at h_nm
    refine le_of_mul_le_mul_of_pos_left h_nm ?_
    exact cast_pos.mpr <| pos_of_ne_zero <| absNorm_ne_zero_of_nonZeroDivisors J

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
N : Submodule R M
inst✝ : Finite (R ⧸ I)
s : Finset M
hs : span R ↑s = N
val✝ : Fintype (R ⧸ I)
e : (↥N ⧸ comap N.subtype (I • N)) ≃ₗ[R] (R ⧸ I) ⊗[R] ↥N :=
  (comap N.subtype (I • N)).quotEquivOfEq (I • ⊤) ⋯ ≪≫ₗ (quotTensorEquivQuotSMul (↥N) I).symm
H : (Finsupp.linearCombination R Subtype.val).range = N
c : ↥s →₀ R
⊢ (Finsupp.linearCombination R Subtype.val) c ∈ N

Tactic:
by rw [← H, LinearMap.mem_range]; exact exists_apply_eq_apply _ _

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: 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
⊢ Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    Submodule.restrictScalars R (span (R ⧸ p) (⇑(algebraMap S (S ⧸ pS)) '' s))

Tactic:
Ideal.Quotient.algebraMap_eq

Goal state after:
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
⊢ Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s))
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
ι : Type u_2 := Free.ChooseBasisIndex R S
b : Basis ι R S := Free.chooseBasis R S
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((leftMulMatrix b) x).trace

Tactic:
trace_eq_matrix_trace (basisQuotient b),

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
ι : Type u_2 := Free.ChooseBasisIndex R S
b : Basis ι R S := Free.chooseBasis R S
⊢ ((leftMulMatrix (basisQuotient b)) ((Ideal.Quotient.mk pS) x)).trace =
    (Ideal.Quotient.mk p) ((leftMulMatrix b) x).trace
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
inst✝¹¹ : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : IsLocalization.AtPrime Rₚ p
inst✝⁶ : IsLocalRing Rₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
⊢ (Algebra.trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) =
    (equivQuotMaximalIdeal p Rₚ).symm ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap S (Sₚ ⧸ pSₚ)) x))

Tactic:
have : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ) := by
    apply IsScalarTower.of_algebraMap_eq'
    rw [IsScalarTower.algebraMap_eq R Rₚ (Rₚ ⧸ _), IsScalarTower.algebraMap_eq R Rₚ (Sₚ ⧸ _),
      ← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq Rₚ]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
inst✝¹¹ : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹⁰ : CommRing Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : IsLocalization.AtPrime Rₚ p
inst✝⁶ : IsLocalRing Rₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (Algebra.trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) =
    (equivQuotMaximalIdeal p Rₚ).symm ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap S (Sₚ ⧸ pSₚ)) x))
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case mpr
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)) =
    (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))).range
hs : span R s = ⊤
⊢ Function.Surjective ⇑(algebraMap S (S ⧸ pS))

Tactic:
Ideal.Quotient.algebraMap_eq

Goal state after:
case mpr
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)) =
    (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))).range
hs : span R s = ⊤
⊢ Function.Surjective ⇑(Ideal.Quotient.mk pS)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Tactic:
obtain ⟨w₀⟩ := (inferInstance : Nonempty (InfinitePlace K))

Goal state after:
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
w₀ : InfinitePlace ↥K
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: 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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁵ : CommRing Rₘ
inst✝¹⁴ : Algebra R Rₘ
inst✝¹³ : CommRing Sₘ
inst✝¹² : Algebra S Sₘ
inst✝¹¹ : Algebra Rₘ Sₘ
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : IsScalarTower R Rₘ Sₘ
inst✝⁸ : IsScalarTower R S Sₘ
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁵ : IsIntegrallyClosed Rₘ
inst✝⁴ : IsDomain Rₘ
inst✝³ : IsDomain Sₘ
inst✝² : IsTorsionFree Rₘ Sₘ
inst✝¹ : Module.Finite Rₘ Sₘ
inst✝ : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
⊢ spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)

Tactic:
let L := FractionRing S

Goal state after:
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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁵ : CommRing Rₘ
inst✝¹⁴ : Algebra R Rₘ
inst✝¹³ : CommRing Sₘ
inst✝¹² : Algebra S Sₘ
inst✝¹¹ : Algebra Rₘ Sₘ
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : IsScalarTower R Rₘ Sₘ
inst✝⁸ : IsScalarTower R S Sₘ
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁵ : IsIntegrallyClosed Rₘ
inst✝⁴ : IsDomain Rₘ
inst✝³ : IsDomain Sₘ
inst✝² : IsTorsionFree Rₘ Sₘ
inst✝¹ : Module.Finite Rₘ Sₘ
inst✝ : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
L : Type u_3 := FractionRing S
⊢ spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: case refine_4
K : Type u_1
𝒪 : Type u_2
inst✝⁷ : Field K
inst✝⁶ : NumberField K
inst✝⁵ : CommRing 𝒪
inst✝⁴ : Algebra 𝒪 K
inst✝³ : IsFractionRing 𝒪 K
inst✝² : IsDedekindDomain 𝒪
inst✝¹ : CharZero 𝒪
inst✝ : Module.Finite ℤ 𝒪
this✝ :
  (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) ≃ₗ[𝒪]
    ↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1
this :
  Nat.card (↥↑1 ⧸ Submodule.comap (↑1).subtype ↑↑(differentIdeal ℤ 𝒪)) =
    Nat.card (↥↑(↑(differentIdeal ℤ 𝒪))⁻¹ ⧸ Submodule.comap (↑(↑(differentIdeal ℤ 𝒪))⁻¹).subtype ↑1)
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := (Algebra.traceForm ℚ K).dualBasis ⋯ b
hb : Submodule.span ℤ (Set.range ⇑b) = Submodule.restrictScalars ℤ 1
⊢ |b'.det ⇑b| = |↑(discr K)|

Tactic:
simp only [Module.Basis.det_apply, discr, Algebra.discr]
    rw [← eq_intCast (algebraMap ℤ ℚ), RingHom.map_det]
    congr! 2
    ext i j
    simp [b', Module.Basis.toMatrix_apply, mul_comm (RingOfIntegers.basis K i),
      b, integralBasis_apply, ← map_mul, Algebra.trace_localization ℤ ℤ⁰]

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

Goal state before:
pp: 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
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst✝ : p.IsPrime
hp : ¬p = ⊥
s : ℕ
left✝ : s ≤ finrank R S
hs : Associated ((relNorm R) P) (p ^ s)
⊢ (relNorm R) P = p ^ s

Tactic:
associated_iff_eq

Goal state after:
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
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
P : Ideal S
p : Ideal R
hPp : P.LiesOver p
inst✝ : p.IsPrime
hp : ¬p = ⊥
s : ℕ
left✝ : s ≤ finrank R S
hs : (relNorm R) P = p ^ s
⊢ (relNorm R) P = p ^ s
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case refine_1
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))
hodd : p ≠ 2
this : NumberField K := numberField {p ^ (k + 1)} ℚ K
h : hζ.toInteger = 1
⊢ ζ ^ 1 = 1

Tactic:
simpa using congrArg (algebraMap _ K) h

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

Goal state before:
pp: case refine_1
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))
hodd : p ≠ 2
this : NumberField K := numberField {p ^ (k + 1)} ℚ K
h : hζ.toInteger - 1 = 0
⊢ False

pp: case refine_2
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))
hodd : p ≠ 2
this : NumberField K := numberField {p ^ (k + 1)} ℚ K
⊢ Irreducible (Ideal.absNorm (Ideal.span {hζ.toInteger - 1}))

Tactic:
· apply hζ.pow_ne_one_of_pos_of_lt one_ne_zero (one_lt_pow₀ hp.out.one_lt (by simp))
    rw [sub_eq_zero] at h
    simpa using congrArg (algebraMap _ K) h

Goal state after:
case refine_2
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))
hodd : p ≠ 2
this : NumberField K := numberField {p ^ (k + 1)} ℚ K
⊢ Irreducible (Ideal.absNorm (Ideal.span {hζ.toInteger - 1}))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case e_a.coprime
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₂ :
  ∀ (K : Type u) [inst : Field K] [inst_1 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K]
    (this : NumberField K), (NumberField.discr K).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this✝² : NumberField K
this✝¹ : NeZero n₁
this✝ : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))

Tactic:
have := hζ₂.intermediateField_adjoin_isCyclotomicExtension ℚ

Goal state after:
case e_a.coprime
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₂ :
  ∀ (K : Type u) [inst : Field K] [inst_1 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K]
    (this : NumberField K), (NumberField.discr K).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this✝³ : NumberField K
this✝² : NeZero n₁
this✝¹ : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this✝ : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
⊢ (NumberField.discr K).natAbs = (n₁ * n₂) ^ φ (n₁ * n₂) / ∏ p ∈ (n₁ * n₂).primeFactors, p ^ (φ (n₁ * n₂) / (p - 1))