mathlib-initiative/mathlib-tactics huggingface dataset:
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 ℂ)
⊢ M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ

Tactic:
ext : 2

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
  (canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ (K →+* ℂ))
e : index K ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
M : Matrix (index K) (index K) ℝ := (mixedEmbedding.stdBasis K).toMatrix ⇑((latticeBasis K).reindex e.symm)
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑f.symm) (RingHom.equivRatAlgHom K ℂ)
i✝ j✝ : index K
⊢ M.map (⇑ofRealHom) i✝ j✝ = (matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ) i✝ j✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

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

Tactic:
mem_toAddSubgroup,

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
w₀ : { w // w.IsComplex }
h : minkowskiBound K I < volume (convexBodyLT' K f w₀)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
x : mixedSpace K
hx : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨x, hx⟩ ≠ 0
h_mem : ↑⟨x, hx⟩ ∈ convexBodyLT' K f w₀
⊢ ∃ a ∈ ↑I,
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧
        |((↑w₀).embedding a).re| < 1 ∧ |((↑w₀).embedding a).im| < ↑(f ↑w₀) ^ 2

Tactic:
mem_toAddSubgroup,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
w₀ : { w // w.IsComplex }
h : minkowskiBound K I < volume (convexBodyLT' K f w₀)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
x : mixedSpace K
hx✝ : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
hx : x ∈ span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))
h_nz : ⟨x, hx✝⟩ ≠ 0
h_mem : ↑⟨x, hx✝⟩ ∈ convexBodyLT' K f w₀
⊢ ∃ a ∈ ↑I,
    a ≠ 0 ∧
      (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧
        |((↑w₀).embedding a).re| < 1 ∧ |((↑w₀).embedding a).im| < ↑(f ↑w₀) ^ 2
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))
⊢ finrank ℚ K = Fintype.card { φ // ComplexEmbedding.IsReal φ } + Fintype.card { φ // ¬ComplexEmbedding.IsReal φ }

Tactic:
← NumberField.Embeddings.card K ℂ,

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 { φ // ¬ComplexEmbedding.IsReal φ }
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 *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * (↑2 ^ nrRealPlaces K * (π / ↑2) ^ nrComplexPlaces K / ↑↑(finrank ℚ K).factorial)⁻¹))) =
    ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹)))

Tactic:
NNReal.coe_ofNat,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑↑(finrank ℚ K).factorial)⁻¹))) =
    ↑(FractionalIdeal.absNorm ↑I) *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹)))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ Fintype.card (ChooseBasisIndex ℤ (𝓞 K)) = Fintype.card (ChooseBasisIndex ℤ ↥↑↑I)

Tactic:
rw [← finrank_eq_card_chooseBasisIndex, ← finrank_eq_card_chooseBasisIndex,
      fractionalIdeal_rank]

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.abs_eq,

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| < ↑B
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
x : mixedSpace K
hx : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨x, hx⟩ ≠ 0
h_mem : ↑⟨x, hx⟩ ∈ convexBodySum K B
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K

Tactic:
mem_toAddSubgroup,

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
x : mixedSpace K
hx✝ : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
hx : x ∈ span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))
h_nz : ⟨x, hx✝⟩ ≠ 0
h_mem : ↑⟨x, hx✝⟩ ∈ convexBodySum K B
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

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

Tactic:
exact (one_le_div Real.pi_pos).2 Real.pi_le_four

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

Goal state before:
pp: A : Type u_1
B : Type u_6
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : IsIntegrallyClosed A
inst✝⁶ : IsDomain A
inst✝⁵ : IsDomain B
inst✝⁴ : IsIntegrallyClosed B
inst✝³ : Algebra.IsIntegral A B
inst✝² : IsTorsionFree A B
inst✝¹ : Free A B
inst✝ : Module.Finite A B
⊢ intNorm A B = norm A

Tactic:
ext x
  have : IsIntegralClosure B A (FractionRing B) :=
    IsIntegralClosure.of_isIntegrallyClosed _ _ _
  apply IsFractionRing.injective A (FractionRing A)
  rw [Algebra.algebraMap_intNorm_fractionRing, Algebra.norm_localization A A⁰]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Tactic:
have h_nz : N ≠ 0 := by
    refine fun h ↦ discr_ne_zero K ?_
    rwa [h, Nat.cast_zero, abs_nonpos_iff] at hK
  have h₂ : 1 < 3 * π / 4 := by
    rw [_root_.lt_div_iff₀ (by positivity), ← _root_.div_lt_iff₀' (by positivity), one_mul]
    linarith [Real.pi_gt_three]
  obtain h | h := lt_or_ge 1 (finrank ℚ K)
  · apply le_max_of_le_right
    rw [Nat.le_floor_iff]
    · have h := le_trans (abs_discr_ge h) (Int.cast_le.mpr hK)
      contrapose! h
      rw [← Real.rpow_natCast]
      rw [Real.log_div_log] at h
      refine lt_of_le_of_lt ?_ (mul_lt_mul_of_pos_left
        (Real.rpow_lt_rpow_of_exponent_lt h₂ h) (by positivity : (0 : ℝ) < 4 / 9))
      rw [Real.rpow_logb (lt_trans zero_lt_one h₂) (ne_of_gt h₂) (by positivity), ← mul_assoc,
            ← inv_div, inv_mul_cancel₀ (by simp), one_mul, Int.cast_natCast]
    · 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))
  · exact le_max_of_le_left h

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

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : HasFiniteQuotients R
B : ℕ
h✝ : Finite R
⊢ {I | Submodule.cardQuot I ≤ B}.Finite

Tactic:
apply Set.toFinite

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

Goal state before:
pp: case mp
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)
⊢ span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤ → span R s = ⊤

Tactic:
intro hs

Goal state after:
case mp
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 = ⊤
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)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
⊢ span R s = ⊤ → span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤

Tactic:
intro hs

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)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
hs : span R s = ⊤
⊢ span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg
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.IsMaximal
inst✝¹ : P.IsPrime
inst✝ : IsGalois (FractionRing R) (FractionRing S)
this✝¹ : P.IsMaximal
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this✝ : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R) P = p ^ s
⊢ (relNorm R) P = p ^ P.inertiaDeg R

Tactic:
suffices s = P.inertiaDeg R by rwa [this] at hs

Goal state after:
case neg
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.IsMaximal
inst✝¹ : P.IsPrime
inst✝ : IsGalois (FractionRing R) (FractionRing S)
this✝¹ : P.IsMaximal
G : Type u_3 := Gal(FractionRing S/FractionRing R)
this✝ : MulSemiringAction Gal(FractionRing S/FractionRing R) S :=
  IsIntegralClosure.MulSemiringAction R (FractionRing R) (FractionRing S) S
this : IsGaloisGroup G R S
hp : ¬p = ⊥
s : ℕ
hs : (relNorm R) P = p ^ s
⊢ s = P.inertiaDeg R
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : IsIntegrallyClosed S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
⊢ (relNorm ℤ) I = span {↑(absNorm I)}

Tactic:
rw [← Int.ideal_span_absNorm_eq_self (relNorm ℤ I), absNorm_relNorm]

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

Goal state before:
pp: p k : ℕ
hp : Fact (Nat.Prime p)
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)

Tactic:
have hζ := zeta_spec (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)

Goal state after:
p k : ℕ
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) (p ^ k)
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case refine_2.zero
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
this : NumberField K
inst✝ : IsCyclotomicExtension {2 ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
convert! Prime.neg Int.prime_two

Goal state after:
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
this : NumberField K
inst✝ : IsCyclotomicExtension {2 ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
⊢ (Algebra.norm ℤ) (hζ.toInteger - 1) = -2
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case 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] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₁), NumberField K → ℤ[hζ.toInteger] = ⊤
hK₂ :
  ∀ {K : Type u} [inst : Field K] [inst_1 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₂), NumberField K → ℤ[hζ.toInteger] = ⊤
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this : NumberField K
⊢ ℤ[hζ.toInteger] = ⊤

Tactic:
have : NeZero n₁ := NeZero.of_gt hn₁
    have : NeZero n₂ := NeZero.of_gt hn₂
    have hζ₁ := hζ.pow (NeZero.pos _) (a := n₂) (b := n₁) (by rw [mul_comm])
    have := hζ₁.intermediateField_adjoin_isCyclotomicExtension ℚ
    replace hζ₁ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₁
    replace hK₁ := @hK₁ ℚ⟮ζ ^ n₂⟯ _ _ _ _ (AdjoinSimple.gen _ _) hζ₁ (of_intermediateField _)
    have hζ₂ := hζ.pow (NeZero.pos _) (a := n₁) (b := n₂) rfl
    have := hζ₂.intermediateField_adjoin_isCyclotomicExtension ℚ
    replace hζ₂ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₂
    replace hK₂ := @hK₂ ℚ⟮ζ ^ n₁⟯ _ _ _ _ (AdjoinSimple.gen _ _) hζ₂ (of_intermediateField _)
    have h_top : ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤ := by
      have : IsCyclotomicExtension {n₁ * n₂} ℚ (⊤ : IntermediateField ℚ K) :=
          hK.equiv _ _ _ topEquiv.symm
      have : IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) := by
        rw [← Nat.Coprime.lcm_eq_mul h]
        exact isCyclotomicExtension_lcm_sup ℚ K n₁ n₂ ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯
      exact isCyclotomicExtension_eq {n₁ * n₂} ℚ K _ _
    exact adjoin_singleton_eq_top_aux K ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯ hζ₁ hK₁ hζ₂ hK₂ h h_top hζ

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : r < 0
⊢ ↑(unitLattice K) ∩ Metric.closedBall 0 r = ∅

Tactic:
rw [Metric.closedBall_eq_empty.mpr hr]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : r < 0
⊢ ↑(unitLattice K) ∩ ∅ = ∅
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
x : 𝓞 K
hx : x ≠ 0
hx' : (algebraMap (𝓞 K) K) x ≠ 0
f : InfinitePlace K → ℝ≥0 := fun w ↦ ⟨w ↑x / 2, ⋯⟩
w✝ : InfinitePlace K
a✝ : w✝ ≠ w₁
⊢ ¬↑x = 0 ∧ ¬2 = 0

Tactic:
exact ⟨hx', by simp⟩

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

Goal state before:
pp: n : ℤ
h : ¬3 ∣ n
⊢ (castHom ⋯ (ZMod 3)) ↑n ≠ 0

Tactic:
rwa [map_intCast, Ne, ZMod.intCast_zmod_eq_zero_iff_dvd]

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

Goal state before:
pp: case inl.inl.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 1
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
ha,

Goal state after:
case inl.inl.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 1
⊢ ¬1 + ↑b ^ 3 = ↑c ^ 3
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.inl.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 8
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
ha,

Goal state after:
case inl.inl.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 8
⊢ ¬1 + ↑b ^ 3 = ↑c ^ 3
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.inr.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 1
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
ha,

Goal state after:
case inl.inr.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 1
⊢ ¬1 + ↑b ^ 3 = ↑c ^ 3
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.inr.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 8
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
ha,

Goal state after:
case inl.inr.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 1
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 8
⊢ ¬1 + ↑b ^ 3 = ↑c ^ 3
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inl.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 1
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
ha,

Goal state after:
case inr.inl.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 1
⊢ ¬8 + ↑b ^ 3 = ↑c ^ 3
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inl.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 8
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
ha,

Goal state after:
case inr.inl.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 1
hc : ↑c ^ 3 = 8
⊢ ¬8 + ↑b ^ 3 = ↑c ^ 3
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inr.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 1
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
ha,

Goal state after:
case inr.inr.inl
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 1
⊢ ¬8 + ↑b ^ 3 = ↑c ^ 3
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inr.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 8
⊢ ¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3

Tactic:
ha,

Goal state after:
case inr.inr.inr
a b c : ℤ
hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c
ha : ↑a ^ 3 = 8
hb : ↑b ^ 3 = 8
hc : ↑c ^ 3 = 8
⊢ ¬8 + ↑b ^ 3 = ↑c ^ 3