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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsReal }
⊢ ↑(x (↑w).embedding).re =
    ∑ x_1,
        fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
            (Sum.inl w) (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Tactic:
fromBlocks_apply₁₁,

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsReal }
⊢ ↑(x (↑w).embedding).re =
    ∑ x_1, 1 w x_1 * x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : 𝓞 K
h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1
h_nz : (algebraMap (𝓞 K) K) a ≠ 0
h_nm :
  ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a)| ≤
    ↑(FractionalIdeal.absNorm ↑1) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
⊢ ∃ a,
    a ≠ 0 ∧
      ↑|(Algebra.norm ℚ) ↑a| ≤
        (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|

Tactic:
refine ⟨a, ne_zero_of_map h_nz, ?_⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : 𝓞 K
h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1
h_nz : (algebraMap (𝓞 K) K) a ≠ 0
h_nm :
  ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a)| ≤
    ↑(FractionalIdeal.absNorm ↑1) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
⊢ ↑|(Algebra.norm ℚ) ↑a| ≤
    (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ 0 < ∑ i, ↑i.mult

Tactic:
← Nat.cast_sum,

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ 0 < ↑(∑ x, x.mult)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

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

Tactic:
gcongr

Goal state after:
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 / π

case hmn
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
⊢ 2 * nrComplexPlaces K ≤ finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

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

Tactic:
convert_to _ ≤ (a m) * (1 + 1 / m : ℝ) ^ (2 * m) / (4 / π)

Goal state after:
case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + 1 / ↑m) ^ (2 * m)
⊢ a (m + 1) = a m * (1 + 1 / ↑m) ^ (2 * m) / (4 / π)

case convert_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + 1 / ↑m) ^ (2 * m)
⊢ 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a m * (1 + 1 / ↑m) ^ (2 * m) / (4 / π)
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
C : Type u_9
inst✝⁹ : CommRing C
inst✝⁸ : IsDomain C
inst✝⁷ : IsIntegrallyClosed C
inst✝⁶ : Algebra A C
inst✝⁵ : Algebra B C
inst✝⁴ : IsScalarTower A B C
inst✝³ : Algebra.IsIntegral A C
inst✝² : Algebra.IsIntegral B C
inst✝¹ : IsTorsionFree A C
inst✝ : IsTorsionFree B C
x : C
⊢ (intNorm A B) ((intNorm B C) x) = (intNorm A C) x

Tactic:
apply FaithfulSMul.algebraMap_injective A (FractionRing A)

Goal state after:
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
C : Type u_9
inst✝⁹ : CommRing C
inst✝⁸ : IsDomain C
inst✝⁷ : IsIntegrallyClosed C
inst✝⁶ : Algebra A C
inst✝⁵ : Algebra B C
inst✝⁴ : IsScalarTower A B C
inst✝³ : Algebra.IsIntegral A C
inst✝² : Algebra.IsIntegral B C
inst✝¹ : IsTorsionFree A C
inst✝ : IsTorsionFree B C
x : C
⊢ (algebraMap A (FractionRing A)) ((intNorm A B) ((intNorm B C) x)) = (algebraMap A (FractionRing A)) ((intNorm A C) x)
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
B : Type u_6
B₂ : Type u_7
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : CommRing B₂
inst✝¹³ : Algebra A 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✝⁵ : IsDomain B₂
inst✝⁴ : IsIntegrallyClosed B₂
inst✝³ : Algebra.IsIntegral A B₂
inst✝² : IsTorsionFree A B₂
inst✝¹ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
inst✝ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B₂)
x : B
σ : B ≃ₐ[A] B₂
⊢ (intNorm A B₂) (σ x) = (intNorm A B) x

Tactic:
apply FaithfulSMul.algebraMap_injective A (FractionRing A)

Goal state after:
A : Type u_1
B : Type u_6
B₂ : Type u_7
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : CommRing B₂
inst✝¹³ : Algebra A 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✝⁵ : IsDomain B₂
inst✝⁴ : IsIntegrallyClosed B₂
inst✝³ : Algebra.IsIntegral A B₂
inst✝² : IsTorsionFree A B₂
inst✝¹ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
inst✝ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B₂)
x : B
σ : B ≃ₐ[A] B₂
⊢ (algebraMap A (FractionRing A)) ((intNorm A B₂) (σ x)) = (algebraMap A (FractionRing A)) ((intNorm A B) x)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ 2 < |discr K|

Tactic:
rify

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ 2 < |↑(discr K)|
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ 4 / 9 * (3 * π / 4) ^ 2 ≤ 4 / 9 * (3 * π / 4) ^ finrank ℚ K

Tactic:
gcongr

Goal state after:
case ha
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ 1 ≤ 3 * π / 4
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
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K ≤ 1 * ↑(sqrt ↑N) * 2 ^ rankOfDiscrBdd N

Tactic:
gcongr

Goal state after:
case h₁
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ 2⁻¹ ^ nrComplexPlaces K ≤ 1

case _a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ ‖discr K‖₊ ≤ ↑N

case ha
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ 1 ≤ 2

case hmn
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ finrank ℚ K ≤ rankOfDiscrBdd N
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case refine_2.refine_2
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 : ℕ
⊢ max (↑B) 1 ^ finrank ℚ ↥K * ↑((finrank ℚ ↥K).choose (finrank ℚ ↥K / 2)) ≤ max (↑B) 1 ^ D * ↑(D.choose (D / 2))

Tactic:
gcongr

Goal state after:
case ha
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
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 : ℕ
⊢ 1 ≤ max (↑B) 1

case hmn
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
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 : ℕ
⊢ finrank ℚ ↥K ≤ D

case a
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
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 : ℕ
⊢ (finrank ℚ ↥K).choose (finrank ℚ ↥K / 2) ≤ D.choose (D / 2)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: 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}
⊢ 1 * ↑B ≤ ↑(convexBodyLTFactor ↥K) * ↑B

Tactic:
gcongr

Goal state after:
case h₁
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
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}
⊢ 1 ≤ ↑(convexBodyLTFactor ↥K)
Module: Mathlib.RingTheory.Ideal.Quotient.Index

Goal state before:
pp: case intro
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)
⊢ (I • N).toAddSubgroup.relIndex N.toAddSubgroup * N.toAddSubgroup.index ≤
    (toAddSubgroup I).index ^ s.card * N.toAddSubgroup.index

Tactic:
gcongr

Goal state after:
case h₁
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)
⊢ (I • N).toAddSubgroup.relIndex N.toAddSubgroup ≤ (toAddSubgroup I).index ^ s.card
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
f : (↥s →₀ R) →ₗ[R] ↥N := LinearMap.codRestrict N (Finsupp.linearCombination R Subtype.val) ⋯
x : ↥N
⊢ ∃ a, f a = x

Tactic:
obtain ⟨y, hy⟩ := H.ge x.2

Goal state after:
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
f : (↥s →₀ R) →ₗ[R] ↥N := LinearMap.codRestrict N (Finsupp.linearCombination R Subtype.val) ⋯
x : ↥N
y : ↥s →₀ R
hy : (Finsupp.linearCombination R Subtype.val) y = ↑x
⊢ ∃ a, f a = x
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
hI : I ≤ 1
⊢ extended L hf I ≤ 1

Tactic:
obtain ⟨J, rfl⟩ := le_one_iff_exists_coeIdeal.mp hI
  intro x hx
  simp only [mem_extended_iff, mem_span_image_iff_exists_fun] at hx
  obtain ⟨s, hs, c, rfl⟩ := hx
  refine Submodule.sum_smul_mem _ _ fun ⟨x, hx⟩ h ↦ ?_
  obtain ⟨a, ha, rfl⟩ := hI (hs hx)
  exact ⟨f a, by simp [map_eq]⟩

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
⊢ extended L hf (I * J) = extended L hf I * extended L hf J

Tactic:
apply coeToSubmodule_injective
  simp only [coe_extended_eq_span, coe_mul, span_mul_span]
  refine Submodule.span_eq_span (fun _ h ↦ ?_) (fun _ h ↦ ?_)
  · rcases h with ⟨x, hx, rfl⟩
    replace hx : x ∈ (I : Submodule A K) * (J : Submodule A K) := coe_mul I J ▸ hx
    rw [Submodule.mul_eq_span_mul_set] at hx
    refine span_induction (fun y hy ↦ ?_) (by simp) (fun y z _ _ hy hz ↦ ?_)
      (fun a y _ hy ↦ ?_) hx
    · rcases Set.mem_mul.mp hy with ⟨i, hi, j, hj, rfl⟩
      exact subset_span <| Set.mem_mul.mpr
        ⟨map_f i, ⟨i, hi, by simp⟩, map_f j, ⟨j, hj, by simp⟩, by simp⟩
    · exact map_add map_f y z ▸ Submodule.add_mem _ hy hz
    · rw [Algebra.smul_def, map_mul, map_eq, ← Algebra.smul_def]
      exact smul_mem _ (f a) hy
  · rcases Set.mem_mul.mp h with ⟨y, ⟨i, hi, rfl⟩, z, ⟨j, hj, rfl⟩, rfl⟩
    exact Submodule.subset_span ⟨i * j, mul_mem_mul hi hj, by simp⟩

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

Goal state before:
pp: case refine_2.refine_2
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 : ℕ
⊢ max (√(1 + ↑(boundOfDiscBdd N) ^ 2)) 1 ^ finrank ℚ ↥K * ↑((finrank ℚ ↥K).choose (finrank ℚ ↥K / 2)) ≤
    max (√(1 + ↑B ^ 2)) 1 ^ D * ↑↑(D.choose (D / 2))

Tactic:
gcongr

Goal state after:
case ha
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
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 : ℕ
⊢ 1 ≤ max (√(1 + ↑(boundOfDiscBdd N) ^ 2)) 1

case hmn
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
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 : ℕ
⊢ finrank ℚ ↥K ≤ D

case h₂
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
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 : ℕ
⊢ ↑((finrank ℚ ↥K).choose (finrank ℚ ↥K / 2)) ≤ ↑↑(D.choose (D / 2))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: 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}
⊢ 1 * ↑B ≤ ↑(convexBodyLT'Factor ↥K) * ↑B

Tactic:
gcongr

Goal state after:
case h₁
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := ⋯
B : ℝ≥0 := ⋯
C : ℕ := ⋯
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}
⊢ 1 ≤ ↑(convexBodyLT'Factor ↥K)
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
⊢ P = span {x}

Tactic:
← associated_iff_eq,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
⊢ Associated P (span {x})
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) ≤ ⊤

Tactic:
exact le_top

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
hn : (Int.castRingHom (ZMod p)) (((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).coeff k) = 0
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff k = 0

Tactic:
← coeff_map

Goal state after:
case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
hn : (Polynomial.map (Int.castRingHom (ZMod p)) ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1))).coeff k = 0
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff k = 0