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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
h✝ : ¬w.IsReal
⊢ ‖(c • x).2 ⟨w, ⋯⟩‖ = |c| * ‖x.2 ⟨w, ⋯⟩‖

Tactic:
simp

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

Goal state before:
pp: case fst
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
c : ℝ
x✝ : { w // w.IsReal }
⊢ (fun x ↦ c, fun x ↦ ↑c).1 x✝ = (c • 1).1 x✝

Tactic:
simp

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

Goal state before:
pp: case snd
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
c : ℝ
x✝ : { w // w.IsComplex }
⊢ (fun x ↦ c, fun x ↦ ↑c).2 x✝ = (c • 1).2 x✝

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ (∀ i ∈ Finset.univ, ↑i.mult * (normAtPlace i) x = 0) ↔ ∀ (w : InfinitePlace K), (normAtPlace w) x = 0

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ convexBodySumFactor K ≠ 0

Tactic:
refine div_ne_zero ?_ <| Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (NNReal.pi / 2) ^ nrComplexPlaces K ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ univ.sup' ⋯ (Subtype.val ∘ fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯) = univ.sup' ⋯ fun w ↦ (normAtPlace w) x

Tactic:
simp

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

Goal state before:
pp: case pos
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
σ : Gal(K/k)
hσ : ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑{1, σ} = 1 ∨ Nat.card ↑{1, σ} = 2

Tactic:
simp

Goal state after:
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
h : ∀ (σ : Gal(K/k)), ¬ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑{1} = 1

Tactic:
simp

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

Goal state before:
pp: case fst
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w.IsReal }
⊢ (fun x ↦ c, fun x ↦ ↑c).1 x✝ = (c • 1).1 x✝

Tactic:
simp

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

Goal state before:
pp: case snd
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w.IsComplex }
⊢ (fun x ↦ c, fun x ↦ ↑c).2 x✝ = (c • 1).2 x✝

Tactic:
simp

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

Goal state before:
pp: case isTrue
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
h✝ : IsUnramified k w
⊢ Nat.card ↥(Stab w) = 1

pp: case isFalse
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
h✝ : ¬IsUnramified k w
⊢ Nat.card ↥(Stab w) = 2

Tactic:
· rwa [← isUnramified_iff_card_stabilizer_eq_one]

Goal state after:
case isFalse
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
h✝ : ¬IsUnramified k w
⊢ Nat.card ↥(Stab w) = 2
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 ℂ)
this✝ : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
this : ‖I‖₊ = 1
⊢ ↑‖2‖.toNNReal⁻¹ ^ nrComplexPlaces K * ↑‖N.det‖₊ = 2⁻¹ ^ Fintype.card { w // w.IsComplex } * ↑(sqrt ‖N.det ^ 2‖₊)

Tactic:
RCLike.norm_two,

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 ℂ)
this✝ : M.map ⇑ofRealHom = matrixToStdBasis K * ((reindex (indexEquiv K).symm (indexEquiv K).symm) N)ᵀ
this : ‖I‖₊ = 1
⊢ ↑(Real.toNNReal 2)⁻¹ ^ nrComplexPlaces K * ↑‖N.det‖₊ = 2⁻¹ ^ Fintype.card { w // w.IsComplex } * ↑(sqrt ‖N.det ^ 2‖₊)
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
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : ¬IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
⊢ #(MulAction.orbit Gal(K/k) w).toFinset = Nat.card Gal(K/k) / 2

Tactic:
rw [Nat.card_eq_fintype_card,
        ← MulAction.card_orbit_mul_card_stabilizer_eq_card_group _ w,
        ← Nat.card_eq_fintype_card (α := Stab w), InfinitePlace.card_stabilizer, if_neg,
        Nat.mul_div_cancel _ zero_lt_two, Set.toFinset_card]

Goal state after:
case hnc
k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : ¬IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
⊢ ¬IsUnramified k w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT K fun w ↦ if w = w₀ then B else 1)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ↑a < ↑(if w = w₀ then B else 1)
w : InfinitePlace K
h✝ : w = w₀
⊢ ↑B ≤ ↑(max B 1)

Tactic:
simp

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

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT K fun w ↦ if w = w₀ then B else 1)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ↑a < ↑(if w = w₀ then B else 1)
w : InfinitePlace K
h✝ : ¬w = w₀
⊢ ↑1 ≤ ↑(max B 1)

Tactic:
simp

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
this : Algebra K ℂ := v.embedding.toAlgebra
ψ : L →+* ℂ
hψ : ComplexEmbedding.LiesOver ψ v.embedding
⊢ { toRingHom := ψ, commutes' := ⋯ } ∈ ↑univ ∧ { toRingHom := ψ, commutes' := ⋯ }.toRingHom = ψ

Tactic:
simp

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
⊢ |(latticeBasis K).det (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e)| = ↑(FractionalIdeal.absNorm ↑I)

Tactic:
suffices Basis.det (latticeBasis K) ((mixedEmbedding K ∘ (basisOfFractionalIdeal K I) ∘ e)) =
      (algebraMap ℚ ℝ) ((Basis.det (integralBasis K)) ((basisOfFractionalIdeal K I) ∘ e)) by
    rw [this, eq_ratCast, ← Rat.cast_abs, ← Equiv.symm_symm e, ← Basis.coe_reindex,
      det_basisOfFractionalIdeal_eq_absNorm K I e]
  rw [Basis.det_apply, Basis.det_apply, RingHom.map_det]
  congr
  ext i j
  simp_rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply, Function.comp_apply]
  exact latticeBasis_repr_apply K _ i

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
x✝ : B
⊢ (algebraMap B L) ((galRestrict' A B B (AlgHom.id K L)) x✝) = (algebraMap B L) ((AlgHom.id A B) x✝)

Tactic:
simp

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

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

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✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
⊢ (algebraMap A (FractionRing A)) ((intTrace A B) x) =
    (trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x)

Tactic:
by
  have : IsIntegralClosure B A (FractionRing B) :=
    IsIntegralClosure.of_isIntegrallyClosed _ _ _
  -- TODO: How is this even supposed to fire? `R` and `S` cannot be inferred.
  have : Algebra.IsAlgebraic (FractionRing A) (FractionRing B) :=
    isAlgebraic_of_isFractionRing A B ..
  have : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
    IsIntegralClosure.isLocalization _ (FractionRing A) _ _
  have : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
  exact Algebra.map_intTraceAux x

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✝¹¹ : FiniteDimensional K L
Aₘ : Type ?u.109
Bₘ : Type ?u.111
inst✝¹⁰ : CommRing Aₘ
inst✝⁹ : CommRing Bₘ
inst✝⁸ : Algebra Aₘ Bₘ
inst✝⁷ : Algebra A Aₘ
inst✝⁶ : Algebra B Bₘ
inst✝⁵ : Algebra A Bₘ
inst✝⁴ : IsScalarTower A Aₘ Bₘ
inst✝³ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝² : IsLocalization M Aₘ
inst✝¹ : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝ : IsIntegrallyClosed A
⊢ IsIntegralClosure.mk' A ((norm K) ((algebraMap B L) 1)) ⋯ = 1

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hm : MeasurableSet A
x✝ : mixedSpace K
⊢ x✝ ∈ plusPart A ↔ x✝ ∈ A ∩ ⋂ w, {x | 0 < x.1 w}

Tactic:
simp

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

Tactic:
algebraMap_intNorm_fractionRing,

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
⊢ (norm (FractionRing A)) ((algebraMap B (FractionRing 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
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
⊢ (norm (FractionRing A)) ((algebraMap B (FractionRing B)) ((intNorm B C) x)) =
    (algebraMap A (FractionRing A)) ((intNorm A C) x)

Tactic:
algebraMap_intNorm_fractionRing,

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
⊢ (norm (FractionRing A)) ((norm (FractionRing B)) ((algebraMap C (FractionRing 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
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
⊢ (norm (FractionRing A)) ((norm (FractionRing B)) ((algebraMap C (FractionRing C)) x)) =
    (algebraMap A (FractionRing A)) ((intNorm A C) x)

Tactic:
algebraMap_intNorm_fractionRing,

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
⊢ (norm (FractionRing A)) ((norm (FractionRing B)) ((algebraMap C (FractionRing C)) x)) =
    (norm (FractionRing A)) ((algebraMap C (FractionRing C)) x)
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✝ : FiniteDimensional (FractionRing A) (FractionRing B)
this : IsIntegralClosure B A (FractionRing B)
⊢ (algebraMap A (FractionRing A)) ((intNorm A B) 0) = (algebraMap A (FractionRing A)) 0

Tactic:
simp

Goal state after:
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₂
⊢ (algebraMap A (FractionRing A)) ((intNorm A B₂) (σ x)) = (algebraMap A (FractionRing A)) ((intNorm A B) x)

Tactic:
algebraMap_intNorm_fractionRing,

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₂
⊢ (norm (FractionRing A)) ((algebraMap B₂ (FractionRing B₂)) (σ x)) = (algebraMap A (FractionRing A)) ((intNorm A B) 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₂
⊢ (norm (FractionRing A)) ((algebraMap B₂ (FractionRing B₂)) (σ x)) = (algebraMap A (FractionRing A)) ((intNorm A B) x)

Tactic:
algebraMap_intNorm_fractionRing,

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₂
⊢ (norm (FractionRing A)) ((algebraMap B₂ (FractionRing B₂)) (σ x)) =
    (norm (FractionRing A)) ((algebraMap B (FractionRing B)) x)
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✝ : FiniteDimensional (FractionRing A) (FractionRing B)
x : B
⊢ (intNorm A B) x ≠ 0 ↔ x ≠ 0

Tactic:
simp

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
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h✝ : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * ↑N) < ↑(finrank ℚ K)
⊢ 9 / 4 ≠ 0

Tactic:
simp

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
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ 2⁻¹ ≤ 1

Tactic:
simp

Goal state after:
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
k : ℕ
hk : φ n = k + k
key : 2 * nrComplexPlaces K = 2 * k
⊢ 2 ≠ 0

Tactic:
simp

Goal state after:
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}
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 (↑(max B 1)) 1 = max (↑B) 1

Tactic:
simp

Goal state after: