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
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:
by

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)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I := Fintype.equivOfCardEq ⋯
this : IsUnit ((latticeBasis K).det (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e))
⊢ Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)

Tactic:
by

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| < ↑(NNReal.sqrt B ^ 2)

Tactic:
exact h_le₀.2

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)ˣ
⊢ Basis (ChooseBasisIndex ℤ ↥↑↑I) ℝ (mixedSpace K)

Tactic:
by

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)ˣ
i : ChooseBasisIndex ℤ ↥↑↑I
⊢ (fractionalIdealLatticeBasis K I) i = (mixedEmbedding K) ((basisOfFractionalIdeal K I) i)

Tactic:
by

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 *
      (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹ =
    ↑(FractionalIdeal.absNorm ↑I) *
            2 ^ (↑(finrank ℚ K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π⁻¹ ^ nrComplexPlaces K

Tactic:
by

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)ˣ
x : mixedSpace K
⊢ x ∈ Submodule.span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I)) ↔ x ∈ ⇑(mixedEmbedding K) '' ↑↑I

Tactic:
by

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)ˣ
⊢ Submodule.span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I)) = idealLattice K I

Tactic:
by

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 ^ (↑(finrank ℚ K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π⁻¹ ^ nrComplexPlaces K =
    ↑(FractionalIdeal.absNorm ↑I) * 2 ^ (2 * ↑(nrComplexPlaces K)) * √‖discr K‖ * ↑(finrank ℚ K).factorial *
      π⁻¹ ^ nrComplexPlaces K

Tactic:
by

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)ˣ
⊢ DiscreteTopology ↥(idealLattice K I)

Tactic:
by

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 ℝ (idealLattice K I)

Tactic:
by

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)ˣ
⊢ MeasureTheory.IsAddFundamentalDomain (↥(idealLattice K I)) (ZSpan.fundamentalDomain (fractionalIdealLatticeBasis K I))
    MeasureTheory.volume

Tactic:
by

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

Goal state before:
pp: 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
⊢ ∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < √(1 + ↑B ^ 2)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℝ (euclidean.mixedSpace K) = finrank ℚ K

Tactic:
by

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)
⊢ 0 ≤ B

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (stdOrthonormalBasis K).toBasis.map ↑(toMixed K) = stdBasis K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measure.map (⇑(toMixed K)) volume = volume

Tactic:
by

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))).toAddSubgroup

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasurePreserving (⇑(toMixed K).symm) volume volume

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ DiscreteTopology ↥(euclidean.integerLattice K)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ IsZLattice ℝ (euclidean.integerLattice K)

Tactic:
by

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

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

Tactic:
by

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 ^ (2 * ↑(nrComplexPlaces K)) * √‖discr K‖ * ↑(finrank ℚ K).factorial *
      π⁻¹ ^ nrComplexPlaces K =
    ↑(FractionalIdeal.absNorm ↑I) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial * √|↑(discr K)|

Tactic:
by

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

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

Tactic:
by

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)ˣ
⊢ ∃ a ∈ ↑I,
    a ≠ 0 ∧
      ↑|(Algebra.norm ℚ) a| ≤
        ↑(FractionalIdeal.absNorm ↑I) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial /
            ↑(finrank ℚ K) ^ finrank ℚ K *
          √|↑(discr K)|

Tactic:
by

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

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

Tactic:
by

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
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
⊢ a ≠ 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
⊢ MeasurePreserving (⇑(negAt s)) volume volume

Tactic:
by

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
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 ≤ ↑|(Algebra.norm ℚ) a|

Tactic:
by

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
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✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Field L₂
inst✝¹² : Algebra A K
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra K L₂
inst✝⁷ : Algebra A L₂
inst✝⁶ : IsScalarTower A K L₂
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsIntegralClosure B A L
inst✝² : Algebra B₂ L₂
inst✝¹ : IsScalarTower A B₂ L₂
inst✝ : IsIntegralClosure B₂ A L₂
σ : L →ₐ[K] L₂
x : B
⊢ (algebraMap B₂ L₂) ((galRestrict' A B B₂ σ) x) = σ ((algebraMap B L) x)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A K L
inst✝² : Algebra B L
inst✝¹ : IsScalarTower A B L
inst✝ : IsIntegralClosure B A L
⊢ galRestrict' A B B (AlgHom.id K L) = AlgHom.id A B

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝²⁹ : CommRing A
inst✝²⁸ : CommRing B
inst✝²⁷ : CommRing B₂
inst✝²⁶ : CommRing B₃
inst✝²⁵ : Algebra A B
inst✝²⁴ : Algebra A B₂
inst✝²³ : Algebra A B₃
inst✝²² : Field K
inst✝²¹ : Field L
inst✝²⁰ : Field L₂
inst✝¹⁹ : Field L₃
inst✝¹⁸ : Algebra A K
inst✝¹⁷ : Algebra K L
inst✝¹⁶ : Algebra A L
inst✝¹⁵ : IsScalarTower A K L
inst✝¹⁴ : Algebra K L₂
inst✝¹³ : Algebra A L₂
inst✝¹² : IsScalarTower A K L₂
inst✝¹¹ : Algebra K L₃
inst✝¹⁰ : Algebra A L₃
inst✝⁹ : IsScalarTower A K L₃
inst✝⁸ : Algebra B L
inst✝⁷ : IsScalarTower A B L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : Algebra B₂ L₂
inst✝⁴ : IsScalarTower A B₂ L₂
inst✝³ : IsIntegralClosure B₂ A L₂
inst✝² : Algebra B₃ L₃
inst✝¹ : IsScalarTower A B₃ L₃
inst✝ : IsIntegralClosure B₃ A L₃
σ : L →ₐ[K] L₂
σ' : L₂ →ₐ[K] L₃
⊢ galRestrict' A B B₃ (σ'.comp σ) = (galRestrict' A B₂ B₃ σ').comp (galRestrict' A B B₂ σ)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝³¹ : CommRing A
inst✝³⁰ : CommRing B
inst✝²⁹ : CommRing B₂
inst✝²⁸ : CommRing B₃
inst✝²⁷ : Algebra A B
inst✝²⁶ : Algebra A B₂
inst✝²⁵ : Algebra A B₃
inst✝²⁴ : Field K
inst✝²³ : Field L
inst✝²² : Field L₂
inst✝²¹ : Field L₃
inst✝²⁰ : Algebra A K
inst✝¹⁹ : IsFractionRing A K
inst✝¹⁸ : Algebra K L
inst✝¹⁷ : Algebra A L
inst✝¹⁶ : IsScalarTower A K L
inst✝¹⁵ : Algebra K L₂
inst✝¹⁴ : Algebra A L₂
inst✝¹³ : IsScalarTower A K L₂
inst✝¹² : Algebra K L₃
inst✝¹¹ : Algebra A L₃
inst✝¹⁰ : IsScalarTower A K L₃
inst✝⁹ : Algebra B L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : Algebra B₂ L₂
inst✝⁵ : IsScalarTower A B₂ L₂
inst✝⁴ : IsIntegralClosure B₂ A L₂
inst✝³ : Algebra B₃ L₃
inst✝² : IsScalarTower A B₃ L₃
inst✝¹ : IsIntegralClosure B₃ A L₃
inst✝ : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B₂
this✝¹ : IsDomain A
this✝ : IsTorsionFree A L₂
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
⊢ ∀ (y : ↥(Algebra.algebraMapSubmonoid B A⁰)), IsUnit (((algebraMap B₂ L₂).comp ↑σ) ↑y)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝³¹ : CommRing A
inst✝³⁰ : CommRing B
inst✝²⁹ : CommRing B₂
inst✝²⁸ : CommRing B₃
inst✝²⁷ : Algebra A B
inst✝²⁶ : Algebra A B₂
inst✝²⁵ : Algebra A B₃
inst✝²⁴ : Field K
inst✝²³ : Field L
inst✝²² : Field L₂
inst✝²¹ : Field L₃
inst✝²⁰ : Algebra A K
inst✝¹⁹ : IsFractionRing A K
inst✝¹⁸ : Algebra K L
inst✝¹⁷ : Algebra A L
inst✝¹⁶ : IsScalarTower A K L
inst✝¹⁵ : Algebra K L₂
inst✝¹⁴ : Algebra A L₂
inst✝¹³ : IsScalarTower A K L₂
inst✝¹² : Algebra K L₃
inst✝¹¹ : Algebra A L₃
inst✝¹⁰ : IsScalarTower A K L₃
inst✝⁹ : Algebra B L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : Algebra B₂ L₂
inst✝⁵ : IsScalarTower A B₂ L₂
inst✝⁴ : IsIntegralClosure B₂ A L₂
inst✝³ : Algebra B₃ L₃
inst✝² : IsScalarTower A B₃ L₃
inst✝¹ : IsIntegralClosure B₃ A L₃
inst✝ : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B₂
this✝¹ : IsDomain A
this✝ : IsTorsionFree A L₂
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
H : ∀ (y : ↥(Algebra.algebraMapSubmonoid B A⁰)), IsUnit (((algebraMap B₂ L₂).comp ↑σ) ↑y)
⊢ (IsLocalization.lift H).comp (algebraMap K L) = algebraMap K L₂

Tactic:
by

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
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✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Field L₂
inst✝¹³ : Algebra A K
inst✝¹² : IsFractionRing A K
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra K L₂
inst✝⁷ : Algebra A L₂
inst✝⁶ : IsScalarTower A K L₂
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsIntegralClosure B A L
inst✝² : Algebra B₂ L₂
inst✝¹ : IsScalarTower A B₂ L₂
inst✝ : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B₂
x : B
⊢ (galLift K L L₂ σ) ((algebraMap B L) x) = (algebraMap B₂ L₂) (σ x)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsScalarTower A B L
inst✝¹ : IsIntegralClosure B A L
inst✝ : Algebra.IsAlgebraic K L
⊢ galLift K L L (AlgHom.id A B) = AlgHom.id K L

Tactic:
by

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝³¹ : CommRing A
inst✝³⁰ : CommRing B
inst✝²⁹ : CommRing B₂
inst✝²⁸ : CommRing B₃
inst✝²⁷ : Algebra A B
inst✝²⁶ : Algebra A B₂
inst✝²⁵ : Algebra A B₃
inst✝²⁴ : Field K
inst✝²³ : Field L
inst✝²² : Field L₂
inst✝²¹ : Field L₃
inst✝²⁰ : Algebra A K
inst✝¹⁹ : IsFractionRing A K
inst✝¹⁸ : Algebra K L
inst✝¹⁷ : Algebra A L
inst✝¹⁶ : IsScalarTower A K L
inst✝¹⁵ : Algebra K L₂
inst✝¹⁴ : Algebra A L₂
inst✝¹³ : IsScalarTower A K L₂
inst✝¹² : Algebra K L₃
inst✝¹¹ : Algebra A L₃
inst✝¹⁰ : IsScalarTower A K L₃
inst✝⁹ : Algebra B L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : Algebra B₂ L₂
inst✝⁵ : IsScalarTower A B₂ L₂
inst✝⁴ : IsIntegralClosure B₂ A L₂
inst✝³ : Algebra B₃ L₃
inst✝² : IsScalarTower A B₃ L₃
inst✝¹ : Algebra.IsAlgebraic K L
inst✝ : Algebra.IsAlgebraic K L₂
σ : B →ₐ[A] B₂
σ' : B₂ →ₐ[A] B₃
this✝ : IsDomain A
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
x : B
⊢ ((↑(galLift K L L₃ (σ'.comp σ))).comp (algebraMap B L)) x =
    ((↑((galLift K L₂ L₃ σ').comp (galLift K L L₂ σ))).comp (algebraMap B L)) x

Tactic:
by

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
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✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : Field L₂
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : Algebra K L₂
inst✝⁸ : Algebra A L₂
inst✝⁷ : IsScalarTower A K L₂
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsIntegralClosure B A L
inst✝³ : Algebra B₂ L₂
inst✝² : IsScalarTower A B₂ L₂
inst✝¹ : IsIntegralClosure B₂ A L₂
inst✝ : Algebra.IsAlgebraic K L
σ : L →ₐ[K] L₂
this✝ : IsDomain A
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
x : B
⊢ ((↑(galLift K L L₂ (galRestrict' A B B₂ σ))).comp (algebraMap B L)) x = ((↑σ).comp (algebraMap B L)) x

Tactic:
by

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
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✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : Field L₂
inst✝¹⁴ : Algebra A K
inst✝¹³ : IsFractionRing A K
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : Algebra K L₂
inst✝⁸ : Algebra A L₂
inst✝⁷ : IsScalarTower A K L₂
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsIntegralClosure B A L
inst✝³ : Algebra B₂ L₂
inst✝² : IsScalarTower A B₂ L₂
inst✝¹ : IsIntegralClosure B₂ A L₂
inst✝ : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B₂
this✝ : IsDomain A
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
x : B
⊢ (algebraMap B₂ L₂) ((galRestrict' A B B₂ (galLift K L L₂ σ)) x) = (algebraMap B₂ L₂) (σ x)

Tactic:
by

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

Goal state before:
pp: 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)|
⊢ 1 ≤ ↑|(Algebra.norm ℚ) ↑x|

Tactic:
by

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝³² : CommRing A
inst✝³¹ : CommRing B
inst✝³⁰ : CommRing B₂
inst✝²⁹ : CommRing B₃
inst✝²⁸ : Algebra A B
inst✝²⁷ : Algebra A B₂
inst✝²⁶ : Algebra A B₃
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Field L₂
inst✝²² : Field L₃
inst✝²¹ : Algebra A K
inst✝²⁰ : IsFractionRing A K
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : Algebra A L
inst✝¹⁷ : IsScalarTower A K L
inst✝¹⁶ : Algebra K L₂
inst✝¹⁵ : Algebra A L₂
inst✝¹⁴ : IsScalarTower A K L₂
inst✝¹³ : Algebra K L₃
inst✝¹² : Algebra A L₃
inst✝¹¹ : IsScalarTower A K L₃
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsIntegralClosure B A L
inst✝⁷ : Algebra B₂ L₂
inst✝⁶ : IsScalarTower A B₂ L₂
inst✝⁵ : IsIntegralClosure B₂ A L₂
inst✝⁴ : Algebra B₃ L₃
inst✝³ : IsScalarTower A B₃ L₃
inst✝² : IsIntegralClosure B₃ A L₃
inst✝¹ : Algebra.IsAlgebraic K L
inst✝ : Algebra.IsAlgebraic K L₂
σ : B ≃ₐ[A] B₂
⊢ (galLift K L L₂ ↑σ).comp (galLift K L₂ L ↑σ.symm) = AlgHom.id K L₂

Tactic:
by

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝³² : CommRing A
inst✝³¹ : CommRing B
inst✝³⁰ : CommRing B₂
inst✝²⁹ : CommRing B₃
inst✝²⁸ : Algebra A B
inst✝²⁷ : Algebra A B₂
inst✝²⁶ : Algebra A B₃
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Field L₂
inst✝²² : Field L₃
inst✝²¹ : Algebra A K
inst✝²⁰ : IsFractionRing A K
inst✝¹⁹ : Algebra K L
inst✝¹⁸ : Algebra A L
inst✝¹⁷ : IsScalarTower A K L
inst✝¹⁶ : Algebra K L₂
inst✝¹⁵ : Algebra A L₂
inst✝¹⁴ : IsScalarTower A K L₂
inst✝¹³ : Algebra K L₃
inst✝¹² : Algebra A L₃
inst✝¹¹ : IsScalarTower A K L₃
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsIntegralClosure B A L
inst✝⁷ : Algebra B₂ L₂
inst✝⁶ : IsScalarTower A B₂ L₂
inst✝⁵ : IsIntegralClosure B₂ A L₂
inst✝⁴ : Algebra B₃ L₃
inst✝³ : IsScalarTower A B₃ L₃
inst✝² : IsIntegralClosure B₃ A L₃
inst✝¹ : Algebra.IsAlgebraic K L
inst✝ : Algebra.IsAlgebraic K L₂
σ : B ≃ₐ[A] B₂
⊢ (galLift K L₂ L ↑σ.symm).comp (galLift K L L₂ ↑σ) = AlgHom.id K L

Tactic:
by

Goal state after: