mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
c' : k[X]
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = d * c'
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
mul_comm

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_4
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
x✝ :
  (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
    |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
h₁ : ∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)
h₂ : |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
w : InfinitePlace K
hw : w.IsComplex
⊢ w.embedding x ∈ if ⟨w, hw⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f w) ^ 2} else ball 0 ↑(f w)

Tactic:
by_cases h_ne : w = w₀

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
x✝ :
  (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
    |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
h₁ : ∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)
h₂ : |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
w : InfinitePlace K
hw : w.IsComplex
h_ne : w = ↑w₀
⊢ w.embedding x ∈ if ⟨w, hw⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f w) ^ 2} else ball 0 ↑(f w)

case neg
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
x✝ :
  (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
    |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
h₁ : ∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)
h₂ : |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
w : InfinitePlace K
hw : w.IsComplex
h_ne : ¬w = ↑w₀
⊢ w.embedding x ∈ if ⟨w, hw⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f w) ^ 2} else ball 0 ↑(f w)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
a✝ b✝ : K
hx : a✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
hy : b✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
x✝ : K →+* ℂ
⊢ x✝ b✝ * x✝ a✝ = x✝ a✝ * x✝ b✝

Tactic:
mul_comm

Goal state after:
F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
a✝ b✝ : K
hx : a✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
hy : b✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
x✝ : K →+* ℂ
⊢ x✝ a✝ * x✝ b✝ = x✝ a✝ * x✝ b✝
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
this : Algebra.IsAlgebraic ↥E ↥(maximalRealSubfield K)
⊢ IsTotallyReal ↥E

Tactic:
exact IsTotallyReal.of_algebra _ (maximalRealSubfield K)

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

Goal state before:
pp: case inl
F : Type u_1
inst✝⁴ : Field F
K : Type u_2
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst✝ : ∀ (i : ι), IsTotallyReal ↥(k i)
hι : IsEmpty ι
⊢ IsTotallyReal ↥⊥

Tactic:
infer_instance

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : K
w : { w // w.IsReal }
⊢ ((mixedEmbedding K) x).1 w = (embedding_of_isReal ⋯) x

Tactic:
by
  simp_rw [mixedEmbedding, RingHom.prod_apply, RingHom.pi_apply]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : K
w : { w // w.IsComplex }
⊢ ((mixedEmbedding K) x).2 w = (↑w).embedding x

Tactic:
by
  simp_rw [mixedEmbedding, RingHom.prod_apply, RingHom.pi_apply]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ ∀ (x y : (K →+* ℂ) → ℂ),
    ((fun w ↦ (x (↑w).embedding).re + (y (↑w).embedding).re) =
        (fun w ↦ (x (↑w).embedding).re) + fun w ↦ (y (↑w).embedding).re) ∧
      (fun w ↦ x (↑w).embedding + y (↑w).embedding) = (fun w ↦ x (↑w).embedding) + fun w ↦ y (↑w).embedding

Tactic:
exact fun _ _ => ⟨rfl, rfl⟩

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ ∀ (m : ℝ) (x : (K →+* ℂ) → ℂ),
    ((fun w ↦ m * (x (↑w).embedding).re) = m • fun w ↦ (x (↑w).embedding).re) ∧
      (fun w ↦ ↑m * x (↑w).embedding) = m • fun w ↦ x (↑w).embedding

Tactic:
exact fun _ _ => ⟨rfl, rfl⟩

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 : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ volume (convexBodySum K B) = ↑(convexBodySumFactor K) * ENNReal.ofReal B ^ finrank ℚ K

Tactic:
mul_comm

Goal state after:
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) = ENNReal.ofReal B ^ finrank ℚ K * ↑(convexBodySumFactor 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
inst✝ : IsGalois k K
⊢ IsUnramified k w ↔ Stab w = ⊥

Tactic:
rw [← mk_embedding w, isUnramified_mk_iff_forall_isConj]

Goal state after:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ (∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj w.embedding σ → σ = 1) ↔ Stab (mk w.embedding) = ⊥
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
⊢ Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I)))

Tactic:
infer_instance

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) = 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|

Tactic:
Real.coe_sqrt,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2⁻¹ ^ nrComplexPlaces K * √↑‖discr K‖₊ = 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|
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
⊢ Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I)))

Tactic:
infer_instance

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ (ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I)).toReal * (2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊)) =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|

Tactic:
Real.coe_sqrt,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ (ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I)).toReal * (2⁻¹ ^ nrComplexPlaces K * √↑‖discr K‖₊) =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * √|↑(discr K)|
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ DiscreteTopology ↥(Submodule.span ℤ (Set.range ⇑(latticeBasis K)))

Tactic:
infer_instance

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ IsZLattice ℝ (Submodule.span ℤ (Set.range ⇑(latticeBasis K)))

Tactic:
infer_instance

Goal state after:
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
⊢ (ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I)).toReal *
      (2⁻¹ ^ nrComplexPlaces K *
        (↑(sqrt ‖discr K‖₊) *
          (2 ^ finrank ℚ K * ↑(2 ^ nrRealPlaces K * (pi / 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:
ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.1))

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 * (pi / 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)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I := Fintype.equivOfCardEq ⋯
this :
  LinearIndependent ℝ (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e) ∧
    Submodule.span ℝ (Set.range (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e)) = ⊤
⊢ ⊤ ≤ Submodule.span ℝ (Set.range (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e))

Tactic:
rw [this.2]

Goal state after:
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) *
      (↑(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:
Real.coe_sqrt,

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) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π ^ (-↑(nrComplexPlaces K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ DiscreteTopology ↥(Submodule.span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I)))

Tactic:
infer_instance

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ IsZLattice ℝ (Submodule.span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I)))

Tactic:
infer_instance

Goal state after:
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
⊢ Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I)))

Tactic:
infer_instance

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

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

Tactic:
infer_instance

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ IsZLattice ℝ (ZLattice.comap ℝ (mixedEmbedding.integerLattice K) ↑↑(toMixed K))

Tactic:
infer_instance

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

Goal state before:

Tactic:
_ = FractionalIdeal.absNorm I.1 * (2 : ℝ)⁻¹ ^ nrComplexPlaces K * sqrt ‖discr K‖₊ *
          (2 : ℝ) ^ finrank ℚ K * ((2 : ℝ) ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K /
            (Nat.factorial (finrank ℚ K)))⁻¹ := by
      simp_rw [minkowskiBound, convexBodySumFactor,
        volume_fundamentalDomain_fractionalIdealLatticeBasis,
        volume_fundamentalDomain_latticeBasis, toReal_mul, toReal_pow, toReal_inv, coe_toReal,
        toReal_ofNat, mixedEmbedding.finrank, mul_assoc]
      rw [ENNReal.toReal_ofReal (Rat.cast_nonneg.mpr (FractionalIdeal.absNorm_nonneg I.1))]
      simp_rw [NNReal.coe_inv, NNReal.coe_div, NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_div,
        coe_real_pi, NNReal.coe_ofNat, NNReal.coe_natCast]
    _ = FractionalIdeal.absNorm I.1 * (2 : ℝ) ^ (finrank ℚ K - nrComplexPlaces K - nrRealPlaces K +
          nrComplexPlaces K : ℤ) * Real.sqrt ‖discr K‖ * Nat.factorial (finrank ℚ K) *
            π⁻¹ ^ (nrComplexPlaces K) := by
      simp_rw [inv_div, div_eq_mul_inv, mul_inv, ← zpow_neg_one, ← zpow_natCast, mul_zpow,
        ← zpow_mul, neg_one_mul, mul_neg_one, neg_neg, Real.coe_sqrt, coe_nnnorm, sub_eq_add_neg,
        zpow_add₀ (two_ne_zero : (2 : ℝ) ≠ 0)]
      ring
    _ = FractionalIdeal.absNorm I.1 * (2 : ℝ) ^ (2 * nrComplexPlaces K : ℤ) * Real.sqrt ‖discr K‖ *
          Nat.factorial (finrank ℚ K) * π⁻¹ ^ (nrComplexPlaces K) := by
      congr
      rw [← card_add_two_mul_card_eq_rank, Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat]
      ring
    _ = FractionalIdeal.absNorm I.1 * (4 / π) ^ nrComplexPlaces K * (finrank ℚ K).factorial *
          Real.sqrt |discr K| := by
      rw [Int.norm_eq_abs, zpow_mul, show (2 : ℝ) ^ (2 : ℤ) = 4 by norm_cast, div_pow,
        inv_eq_one_div, div_pow, one_pow, zpow_natCast]
      ring

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ↑(finrank ℚ K) ^ (2 * finrank ℚ K) / ((4 / π) ^ (2 * nrComplexPlaces K) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|

Tactic:
obtain ⟨x, h_nz, h_bd⟩ := exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr K

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_bd :
  ↑|(Algebra.norm ℚ) ↑x| ≤
    (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
⊢ ↑(finrank ℚ K) ^ (2 * finrank ℚ K) / ((4 / π) ^ (2 * nrComplexPlaces K) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case hmn
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)
this : ∀ (n : ℕ), 2 ≤ n → 4 / 9 * (3 * π / 4) ^ n ≤ a n
⊢ 2 * nrComplexPlaces K ≤ nrRealPlaces K + 2 * nrComplexPlaces K

Tactic:
mul_comm

Goal state after:
case hmn
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)
this : ∀ (n : ℕ), 2 ≤ n → 4 / 9 * (3 * π / 4) ^ n ≤ a n
⊢ nrComplexPlaces K * 2 ≤ nrRealPlaces K + nrComplexPlaces K * 2
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
h_nz : N ≠ 0
⊢ 1 < 3 * π / 4

Tactic:
_root_.lt_div_iff₀ (by positivity),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
h_nz : N ≠ 0
⊢ 1 * 4 < 3 * π
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings

Goal state before:
pp: n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
⊢ φ n = 1

Tactic:
by_cases h1 : 1 < n

Goal state after:
case pos
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : 1 < n
⊢ φ n = 1

case neg
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : ¬1 < n
⊢ φ n = 1
Module: Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : HasFiniteQuotients R
inst✝² : IsDomain R
inst✝¹ : PerfectField (FractionRing R)
P : Ideal R
inst✝ : P.IsPrime
hP : P ≠ ⊥
this : Finite (R ⧸ P)
⊢ PerfectField P.ResidueField

Tactic:
infer_instance

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

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing T
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S T
inst✝⁸ : Algebra R T
inst✝⁷ : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst✝⁶ : P.LiesOver p
inst✝⁵ : p.IsPrime
inst✝⁴ : P.IsPrime
inst✝³ : IsUnramifiedAt R P
inst✝² : EssFiniteType R S
inst✝¹ : EssFiniteType R T
inst✝ : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this✝⁵ : P.LiesOver p₀
this✝⁴ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime p) := Localization.AtPrime.algebraOfLiesOver p₀ p
this✝³ : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
this✝² : Algebra (Localization.AtPrime p₀) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this✝¹ : EssFiniteType S T
this✝ : IsNoetherianRing T
h₁ : Algebra.IsSeparable p₀.ResidueField P.ResidueField
h₂ : Ideal.map (algebraMap R (Localization.AtPrime P)) p₀ = maximalIdeal (Localization.AtPrime P)
hp : ¬p = ⊥
this : ¬Ideal.map (algebraMap R T) p₀ ≤ P ^ 2
H :
  Ideal.map (algebraMap S T) (Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) p)) ≤
    Ideal.map (algebraMap S T) (p ^ 2)
⊢ False

Tactic:
Ideal.map_map,

Goal state after:
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing T
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S T
inst✝⁸ : Algebra R T
inst✝⁷ : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst✝⁶ : P.LiesOver p
inst✝⁵ : p.IsPrime
inst✝⁴ : P.IsPrime
inst✝³ : IsUnramifiedAt R P
inst✝² : EssFiniteType R S
inst✝¹ : EssFiniteType R T
inst✝ : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this✝⁵ : P.LiesOver p₀
this✝⁴ : Algebra (Localization.AtPrime p₀) (Localization.AtPrime p) := Localization.AtPrime.algebraOfLiesOver p₀ p
this✝³ : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
this✝² : Algebra (Localization.AtPrime p₀) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this✝¹ : EssFiniteType S T
this✝ : IsNoetherianRing T
h₁ : Algebra.IsSeparable p₀.ResidueField P.ResidueField
h₂ : Ideal.map (algebraMap R (Localization.AtPrime P)) p₀ = maximalIdeal (Localization.AtPrime P)
hp : ¬p = ⊥
this : ¬Ideal.map (algebraMap R T) p₀ ≤ P ^ 2
H :
  Ideal.map ((algebraMap S T).comp (algebraMap R S)) (Ideal.comap (algebraMap R S) p) ≤
    Ideal.map (algebraMap S T) (p ^ 2)
⊢ False
Module: Mathlib.NumberTheory.NumberField.ClassNumber

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsGalois ℚ 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),
        ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ <
            p ^ P.inertiaDeg ℤ ∨
          Submodule.IsPrincipal P
p : ℕ
hpmem :
  p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊
hp : Nat.Prime p
P : Ideal (𝓞 K)
x✝ : P ∈ (span {↑p}).primesOver (𝓞 K)
hple :
  p ^ P.inertiaDeg ℤ ≤ ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊
hP1 : P.IsPrime
hP2 : P.LiesOver (span {↑p})
Q : Ideal (𝓞 K)
H :
  ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ <
      p ^ Q.inertiaDeg ℤ ∨
    Submodule.IsPrincipal Q
hQ1 : Q.IsPrime
hQ2 : Q.LiesOver (span {↑p})
⊢ span {↑p} ≠ ⊥

Tactic:
by simp [hp.ne_zero]

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

Goal state before:
pp: case empty
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
I : ι → Ideal R
hI : ∀ i ∈ ∅, (I i).FG
hI' : ∀ i ∈ ∅, Finite (R ⧸ I i)
⊢ Finite (R ⧸ ⊤)

Tactic:
infer_instance

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

Goal state before:
pp: case insert
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
I : ι → Ideal R
a : ι
s : Finset ι
has : a ∉ s
IH : (∀ i ∈ s, (I i).FG) → (∀ i ∈ s, Finite (R ⧸ I i)) → Finite (R ⧸ ∏ i ∈ s, I i)
hI : ∀ i ∈ insert a s, (I i).FG
hI' : ∀ i ∈ insert a s, Finite (R ⧸ I i)
⊢ Finite (R ⧸ I a * ∏ x ∈ s, I x)

Tactic:
mul_comm

Goal state after:
case insert
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
I : ι → Ideal R
a : ι
s : Finset ι
has : a ∉ s
IH : (∀ i ∈ s, (I i).FG) → (∀ i ∈ s, Finite (R ⧸ I i)) → Finite (R ⧸ ∏ i ∈ s, I i)
hI : ∀ i ∈ insert a s, (I i).FG
hI' : ∀ i ∈ insert a s, Finite (R ⧸ I i)
⊢ Finite (R ⧸ (∏ x ∈ s, I x) * I a)
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
hI : I.FG
inst✝ : Finite (R ⧸ I)
⊢ Finite (R ⧸ ⊤)

Tactic:
infer_instance

Goal state after: