mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I J : FractionalIdeal R⁰ K
⊢ ↑(Ideal.absNorm I.num) * ↑(Ideal.absNorm J.num) / |↑((Algebra.norm ℤ) ↑I.den * (Algebra.norm ℤ) ↑J.den)| =
    ↑(Ideal.absNorm I.num) * ↑(Ideal.absNorm J.num) / (|↑((Algebra.norm ℤ) ↑I.den)| * ↑|(Algebra.norm ℤ) ↑J.den|)

Tactic:
Int.cast_abs,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I J : FractionalIdeal R⁰ K
⊢ ↑(Ideal.absNorm I.num) * ↑(Ideal.absNorm J.num) / |↑((Algebra.norm ℤ) ↑I.den * (Algebra.norm ℤ) ↑J.den)| =
    ↑(Ideal.absNorm I.num) * ↑(Ideal.absNorm J.num) / (|↑((Algebra.norm ℤ) ↑I.den)| * |↑((Algebra.norm ℤ) ↑J.den)|)
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| =
    ↑|b.det (Subtype.val ∘ ⇑bI.num)| / ↑|(Algebra.norm ℤ) ↑I.den|

Tactic:
Int.cast_abs,

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| =
    |↑(b.det (Subtype.val ∘ ⇑bI.num))| / ↑|(Algebra.norm ℤ) ↑I.den|
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| =
    |↑(b.det (Subtype.val ∘ ⇑bI.num))| / ↑|(Algebra.norm ℤ) ↑I.den|

Tactic:
Int.cast_abs,

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| =
    |↑(b.det (Subtype.val ∘ ⇑bI.num))| / |↑((Algebra.norm ℤ) ↑I.den)|
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ ↑|(Algebra.norm ℤ) r| / ↑|(Algebra.norm ℤ) ↑d| = |(Algebra.norm ℚ) x|

Tactic:
Int.cast_abs,

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ |↑((Algebra.norm ℤ) r)| / |↑((Algebra.norm ℤ) ↑d)| = |(Algebra.norm ℚ) x|
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
hz : z = w
⊢ z ↑a < 1

Tactic:
hz

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
hz : z = w
⊢ w ↑a < 1
Module: Mathlib.NumberTheory.NumberField.EquivReindex

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ (Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑(equivReindex K)) (RingHom.equivRatAlgHom K ℂ)).det ^ 2 =
    (algebraMap ℚ ℂ) (Algebra.discr ℚ (⇑(integralBasis K) ∘ ⇑(equivReindex K).symm.symm))

Tactic:
exact (Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two ℚ ℂ
    (integralBasis K ∘ (equivReindex K)) (RingHom.equivRatAlgHom K ℂ)).symm

Goal state after:
Module: Mathlib.NumberTheory.NumberField.EquivReindex

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
i : K →+* ℂ
⊢ (∑ i, ((latticeBasis K).repr ((canonicalEmbedding K) α)) ((equivReindex K) i) • (latticeBasis K) ((equivReindex K) i))
      i =
    ((basisMatrix K)ᵀ *ᵥ fun i ↦ ↑((((integralBasis K).reindex (equivReindex K).symm).repr α) i)) i

Tactic:
simp only [canonicalEmbedding.integralBasis_repr_apply, mulVec, dotProduct,
    transpose_apply, of_apply, Fintype.sum_apply, mul_comm, Basis.repr_reindex,
    Finsupp.mapDomain_equiv_apply, Equiv.symm_symm, Pi.smul_apply, smul_eq_mul]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ (ENNReal.ofReal 2 ^ card { w // w.IsReal } * ∏ x, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ card { w // w.IsComplex }) =
    (↑2 ^ nrRealPlaces K * ∏ x, ENNReal.ofReal ↑(f ↑x)) * ((∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ nrComplexPlaces K)

Tactic:
ofReal_ofNat,

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ (2 ^ card { w // w.IsReal } * ∏ x, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ card { w // w.IsComplex }) =
    (↑2 ^ nrRealPlaces K * ∏ x, ENNReal.ofReal ↑(f ↑x)) * ((∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ nrComplexPlaces K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : NNReal
⊢ ↑(Finset.univ.sup fun φ ↦ ‖φ x‖₊) ≤ ↑r ↔ ∀ (φ : K →+* ℂ), ↑‖φ x‖₊ ≤ ↑r

Tactic:
NNReal.coe_le_coe,

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : NNReal
⊢ (Finset.univ.sup fun φ ↦ ‖φ x‖₊) ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖₊ ≤ r
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ ENNReal.ofReal 2 * (ENNReal.ofReal 2 * ENNReal.ofReal ↑B ^ 2) = 4 * ↑B ^ 2

Tactic:
ofReal_ofNat,

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ 2 * (2 * ENNReal.ofReal ↑B ^ 2) = 4 * ↑B ^ 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈
      ↑(Submodule.map (canonicalEmbedding K).toIntAlgHom.toLinearMap
          (Submodule.span ℤ (Set.range ⇑(integralBasis K)))) ↔
    x ∈ ((canonicalEmbedding K).comp (algebraMap (𝓞 K) K)).range

Tactic:
Submodule.map_coe

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈ ⇑(canonicalEmbedding K).toIntAlgHom.toLinearMap '' ↑(Submodule.span ℤ (Set.range ⇑(integralBasis K))) ↔
    x ∈ ((canonicalEmbedding K).comp (algebraMap (𝓞 K) K)).range
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ ↑(((Basis.restrictScalars ℚ (latticeBasis K)).repr ⟨(canonicalEmbedding K) x, ⋯⟩) i) = ↑(((integralBasis K).repr x) i)

Tactic:
Rat.cast_inj

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ ((Basis.restrictScalars ℚ (latticeBasis K)).repr ⟨(canonicalEmbedding K) x, ⋯⟩) i = ((integralBasis K).repr x) i
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (ENNReal.ofReal 2 ^ Fintype.card { w // w.IsReal } * ∏ x, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ (Fintype.card { w // w.IsComplex } - 1) *
        (4 * ↑(f ↑w₀) ^ 2)) =
    (↑2 ^ nrRealPlaces K * ∏ x, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ (nrComplexPlaces K - 1) * (4 * ↑(f ↑w₀) ^ 2))

Tactic:
ofReal_ofNat,

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (2 ^ Fintype.card { w // w.IsReal } * ∏ x, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ (Fintype.card { w // w.IsComplex } - 1) *
        (4 * ↑(f ↑w₀) ^ 2)) =
    (↑2 ^ nrRealPlaces K * ∏ x, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ (nrComplexPlaces K - 1) * (4 * ↑(f ↑w₀) ^ 2))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (↑2 ^ nrRealPlaces K * ∏ x, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ (nrComplexPlaces K - 1) * (4 * ↑(f ↑w₀) ^ 2)) =
    (↑(convexBodyLT'Factor K) * ∏ x, ENNReal.ofReal ↑(f ↑x)) * ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2

Tactic:
by
      rw [show (4 : ℝ≥0∞) = (2 : ℝ≥0) ^ 2 by norm_num, convexBodyLT'Factor, pow_add,
        ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀), ofReal_coe_nnreal]
      simp_rw [coe_mul, ENNReal.coe_pow]
      ring

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
⊢ ∑ w, ↑w.mult * (normAtPlace w) x = ∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖

Tactic:
sum_eq_sum_add_sum,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ∑ w, ↑(↑w).mult * (normAtPlace ↑w) x + ∑ w, ↑(↑w).mult * (normAtPlace ↑w) x = ∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = (normAtPlace w) y
⊢ mixedEmbedding.norm x = mixedEmbedding.norm y

Tactic:
simp_rw [mixedEmbedding.norm_apply, h]

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 : ∫ (x : mixedSpace K), rexp (-convexBodySumFun x) = 2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K
⊢ ENNReal.ofReal 2 ^ nrRealPlaces K * (ENNReal.ofReal π / ENNReal.ofReal 2) ^ nrComplexPlaces K /
      ↑(finrank ℚ K).factorial =
    ↑(2 ^ nrRealPlaces K * (NNReal.pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)

Tactic:
ofReal_ofNat,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : ∫ (x : mixedSpace K), rexp (-convexBodySumFun x) = 2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K
⊢ 2 ^ nrRealPlaces K * (ENNReal.ofReal π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial =
    ↑(2 ^ nrRealPlaces K * (NNReal.pi / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)
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₀.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, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(max B 1)

Tactic:
obtain ⟨a, h_nz, h_le⟩ := exists_ne_zero_mem_ringOfIntegers_lt K this

Goal state after:
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)
⊢ ∃ a, ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(max B 1)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ x ∈ ↑(Submodule.map (mixedEmbedding K).toIntAlgHom.toLinearMap (Submodule.span ℤ (Set.range ⇑(integralBasis K)))) ↔
    x ∈ mixedEmbedding.integerLattice K

Tactic:
Submodule.map_coe

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ x ∈ ⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' ↑(Submodule.span ℤ (Set.range ⇑(integralBasis K))) ↔
    x ∈ mixedEmbedding.integerLattice K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
⊢ ↑(((Basis.restrictScalars ℚ (latticeBasis K)).repr ⟨(mixedEmbedding K) x, ⋯⟩) i) = ↑(((integralBasis K).repr x) i)

Tactic:
Rat.cast_inj

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
⊢ ((Basis.restrictScalars ℚ (latticeBasis K)).repr ⟨(mixedEmbedding K) x, ⋯⟩) i = ((integralBasis K).repr x) i
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.map (mixedEmbedding K).toIntAlgHom.toLinearMap
          (Submodule.span ℤ (Set.range ⇑(basisOfFractionalIdeal K I)))) ↔
    x ∈ ⇑(mixedEmbedding K) '' ↑↑I

Tactic:
Submodule.map_coe

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ x ∈ ⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' ↑(Submodule.span ℤ (Set.range ⇑(basisOfFractionalIdeal K I))) ↔
    x ∈ ⇑(mixedEmbedding K) '' ↑↑I
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
⊢ ⇑(negAt s) ⁻¹' A = ⇑(negAt s) '' A

Tactic:
by
  rw [ContinuousLinearEquiv.image_eq_preimage_symm, negAt_symm]

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
Aₘ : Type u_9
Bₘ : Type u_10
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✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
⊢ (algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)

Tactic:
by_cases hM : 0 ∈ M

Goal state after:
case pos
A : Type u_1
B : Type u_6
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
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✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : 0 ∈ M
⊢ (algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)

case neg
A : Type u_1
B : Type u_6
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
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✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : 0 ∉ M
⊢ (algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

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

Tactic:
inv_mul_cancel₀ h.ne',

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsTotallyComplex K
h : 0 < ↑(finrank ℚ K)
⊢ (↑(finrank ℚ K) ^ 2) ^ ↑(finrank ℚ K) /
      (4 / π * ↑(finrank ℚ K).factorial ^ (2 * (↑(finrank ℚ K))⁻¹)) ^ ↑(finrank ℚ K) ≤
    ↑|discr K| ^ 1
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
Aₘ : Type u_9
Bₘ : Type u_10
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
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsDomain B
inst✝⁹ : IsIntegrallyClosed B
inst✝⁸ : Algebra.IsIntegral A B
inst✝⁷ : IsTorsionFree A B
inst✝⁶ : IsDomain Aₘ
inst✝⁵ : IsIntegrallyClosed Aₘ
inst✝⁴ : IsDomain Bₘ
inst✝³ : IsIntegrallyClosed Bₘ
inst✝² : IsTorsionFree Aₘ Bₘ
inst✝¹ : Algebra.IsIntegral Aₘ Bₘ
inst✝ : FiniteDimensional (FractionRing A) (FractionRing B)
x : B
⊢ (algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)

Tactic:
by_cases hM : 0 ∈ M

Goal state after:
case pos
A : Type u_1
B : Type u_6
inst✝²⁵ : CommRing A
inst✝²⁴ : CommRing B
inst✝²³ : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
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
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsDomain B
inst✝⁹ : IsIntegrallyClosed B
inst✝⁸ : Algebra.IsIntegral A B
inst✝⁷ : IsTorsionFree A B
inst✝⁶ : IsDomain Aₘ
inst✝⁵ : IsIntegrallyClosed Aₘ
inst✝⁴ : IsDomain Bₘ
inst✝³ : IsIntegrallyClosed Bₘ
inst✝² : IsTorsionFree Aₘ Bₘ
inst✝¹ : Algebra.IsIntegral Aₘ Bₘ
inst✝ : FiniteDimensional (FractionRing A) (FractionRing B)
x : B
hM : 0 ∈ M
⊢ (algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)

case neg
A : Type u_1
B : Type u_6
inst✝²⁵ : CommRing A
inst✝²⁴ : CommRing B
inst✝²³ : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
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
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsDomain B
inst✝⁹ : IsIntegrallyClosed B
inst✝⁸ : Algebra.IsIntegral A B
inst✝⁷ : IsTorsionFree A B
inst✝⁶ : IsDomain Aₘ
inst✝⁵ : IsIntegrallyClosed Aₘ
inst✝⁴ : IsDomain Bₘ
inst✝³ : IsIntegrallyClosed Bₘ
inst✝² : IsTorsionFree Aₘ Bₘ
inst✝¹ : Algebra.IsIntegral Aₘ Bₘ
inst✝ : FiniteDimensional (FractionRing A) (FractionRing B)
x : B
hM : 0 ∉ M
⊢ (algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x y : mixedSpace K
h : normAtComplexPlaces x = normAtComplexPlaces y
⊢ normAtAllPlaces x = normAtAllPlaces y

Tactic:
ext w
  obtain hw | hw := isReal_or_isComplex w
  · simpa [normAtAllPlaces_apply, normAtPlace_apply_of_isReal hw,
      normAtComplexPlaces_apply_isReal ⟨w, hw⟩] using congr_arg (|·|) (congr_fun h w)
  · simpa [normAtAllPlaces_apply, normAtPlace_apply_of_isComplex hw,
      normAtComplexPlaces_apply_isComplex ⟨w, hw⟩] using congr_fun h w

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

Goal state before:
pp: case neg
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
this : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ IsIntegral A (((algebraMap B L) x)⁻¹ * (algebraMap A L) ((intNorm A B) x))

Tactic:
← isIntegral_algHom_iff (toAlgHom A L E)
    (FaithfulSMul.algebraMap_injective L E),

Goal state after:
case neg
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
this : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ IsIntegral A ((toAlgHom A L E) (((algebraMap B L) x)⁻¹ * (algebraMap A L) ((intNorm A B) x)))