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

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
F : Type u_3
inst✝³ : Field F
inst✝² : Algebra K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this✝¹ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝ : FiniteDimensional F ↥L
this : IsGalois F ↥L
⊢ IsUnit ((norm K) x ^ finrank F ↥L) ↔ IsUnit ((norm K) (x ^ finrank F ↥L))

Tactic:
map_pow

Goal state after:
K : Type u_2
inst✝⁴ : Field K
F : Type u_3
inst✝³ : Field F
inst✝² : Algebra K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this✝¹ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝ : FiniteDimensional F ↥L
this : IsGalois F ↥L
⊢ IsUnit ((norm K) x ^ finrank F ↥L) ↔ IsUnit ((norm K) x ^ finrank F ↥L)
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 ⋯))
i✝ j✝ : ι
⊢ ((Basis.localizationLocalization ℚ ℤ⁰ K b).repr
        ((algebraMap R K) ↑((LinearEquiv.restrictScalars ℤ (equivNum ⋯)) (bI j✝))))
      i✝ =
    (b₀.repr (((algebraMap R K) ↑I.den • Subtype.val ∘ ⇑bI) j✝)) i✝

Tactic:
LinearEquiv.restrictScalars_apply,

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 ⋯))
i✝ j✝ : ι
⊢ ((Basis.localizationLocalization ℚ ℤ⁰ K b).repr ((algebraMap R K) ↑((equivNum ⋯) (bI j✝)))) i✝ =
    (b₀.repr (((algebraMap R K) ↑I.den • Subtype.val ∘ ⇑bI) j✝)) i✝
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_neg : z = -(m ^ 2 + n ^ 2)
⊢ 0 ≤ m ^ 2 + n ^ 2

Tactic:
by positivity

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

Goal state before:
pp: case mp.inl
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑φ.fieldRange.subtype
x : K
⊢ φ x = ψ (j (φ x))

Tactic:
exact (congrFun h (ι x)).symm

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

Goal state before:
pp: case mp.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑(starRingEnd ℂ) ∘ ⇑φ.fieldRange.subtype
x : K
⊢ (ComplexEmbedding.conjugate φ) x = ψ (j (φ x))

Tactic:
exact (congrFun h (ι x)).symm

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

Goal state before:
pp: case mpr.inl
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h : φ = ψ
⊢ mk φ = mk ψ

Tactic:
exact congr_arg mk h

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

Goal state before:
pp: case mpr.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h : ComplexEmbedding.conjugate φ = ψ
⊢ mk (ComplexEmbedding.conjugate φ) = mk ψ

Tactic:
exact congr_arg mk h

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ 1 ≤ ↑w.mult

Tactic:
← Nat.cast_one,

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ ↑1 ≤ ↑w.mult
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_neg : z = -(m ^ 2 + n ^ 2)
⊢ 0 ≤ m ^ 2 + n ^ 2

Tactic:
by positivity

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h
x y z : ℤ
h : PythagoreanTriple x y z
k m n : ℤ
H : (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧ m.gcd n = 1
⊢ (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Tactic:
rcases H with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)

Goal state after:
case h.inl
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
⊢ (k * (m ^ 2 - n ^ 2) = k * (m ^ 2 - n ^ 2) ∧ k * (2 * m * n) = k * (2 * m * n) ∨
      k * (m ^ 2 - n ^ 2) = k * (2 * m * n) ∧ k * (2 * m * n) = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

case h.inr
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
⊢ (k * (2 * m * n) = k * (m ^ 2 - n ^ 2) ∧ k * (m ^ 2 - n ^ 2) = k * (2 * m * n) ∨
      k * (2 * m * n) = k * (2 * m * n) ∧ k * (m ^ 2 - n ^ 2) = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ 2 = if w.IsReal then 1 else 2

Tactic:
not_isReal_iff_isComplex.mpr hw,

Goal state after:
case e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ 2 = if False then 1 else 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

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

Tactic:
ofReal_coe_nnreal

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

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
E : Subfield K
inst✝ : IsTotallyReal ↥E
x : K
hx : x ∈ E
φ : K →+* ℂ
⊢ star ((φ.comp E.subtype) ⟨x, hx⟩) = (φ.comp E.subtype) ⟨x, hx⟩

Tactic:
RCLike.star_def,

Goal state after:
K : Type u_2
inst✝¹ : Field K
E : Subfield K
inst✝ : IsTotallyReal ↥E
x : K
hx : x ∈ E
φ : K →+* ℂ
⊢ (starRingEnd ℂ) ((φ.comp E.subtype) ⟨x, hx⟩) = (φ.comp E.subtype) ⟨x, hx⟩
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Nontrivial (mixedSpace K)

Tactic:
obtain ⟨w⟩ := (inferInstance : Nonempty (InfinitePlace K))

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ Nontrivial (mixedSpace K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ NullSingletonClass volume

Tactic:
obtain ⟨w⟩ := (inferInstance : Nonempty (InfinitePlace K))

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ NullSingletonClass volume
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) *
        (↑2 ^ 2 * ↑(f ↑w₀) ^ 2)) =
    (↑(2 ^ nrRealPlaces K * 2 ^ 2 * pi ^ (nrComplexPlaces K - 1)) * ∏ x, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2) * ENNReal.ofReal ↑(f ↑w₀) ^ 2)

Tactic:
ofReal_coe_nnreal

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 ^ nrRealPlaces K * ∏ x, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ (nrComplexPlaces K - 1) *
        (↑2 ^ 2 * ↑(f ↑w₀) ^ 2)) =
    (↑(2 ^ nrRealPlaces K * 2 ^ 2 * pi ^ (nrComplexPlaces K - 1)) * ∏ x, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑(f ↑w₀) ^ 2)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case neg.inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
this : ((commMap K) x).2 ⟨InfinitePlace.mk φ, ⋯⟩ = 0.2 ⟨InfinitePlace.mk φ, ⋯⟩
h : (InfinitePlace.mk φ).embedding = ComplexEmbedding.conjugate φ
⊢ x (InfinitePlace.mk φ).embedding = (starRingEnd ℂ) 0

Tactic:
map_zero,

Goal state after:
case neg.inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
this : ((commMap K) x).2 ⟨InfinitePlace.mk φ, ⋯⟩ = 0.2 ⟨InfinitePlace.mk φ, ⋯⟩
h : (InfinitePlace.mk φ).embedding = ComplexEmbedding.conjugate φ
⊢ x (InfinitePlace.mk φ).embedding = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : x = 0
⊢ ∀ (w : InfinitePlace K), (normAtPlace w) 0 = 0

Tactic:
map_zero,

Goal state after:
case refine_2
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : x = 0
⊢ ∀ (w : InfinitePlace K), True
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
σ : Gal(K/k)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
⊢ IsUnramified k (mk φ) ↔ σ = 1

Tactic:
rw [h.ext_iff, ComplexEmbedding.isConj_one_iff, ← not_iff_not, not_isUnramified_iff,
    ← not_isReal_iff_isComplex, comap_mk, isReal_mk_iff, isReal_mk_iff, eq_true h.isReal_comp,
    and_true]

Goal state after:
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' ⋯ (⇑(OrderHom.Subtype.val fun r ↦ 0 ≤ r) ∘ fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯) =
    univ.sup' ⋯ fun w ↦ (normAtPlace w) x

Tactic:
OrderHom.Subtype.val_coe

Goal state after:
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
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
⊢ 0 ≤ 2 ^ nrRealPlaces K

Tactic:
by positivity

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
⊢ 0 ≤ π / 2

Tactic:
by positivity

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
hw : ¬(InfinitePlace.mk φ).embedding = φ
⊢ (fun c ↦
        Sum.casesOn (motive := fun t ↦ c = t → K →+* ℂ) c (fun w h ↦ (↑w).embedding)
          (fun wj h ↦
            Prod.casesOn wj fun w j ↦ if j = 0 then (↑w).embedding else ComplexEmbedding.conjugate (↑w).embedding)
          ⋯)
      (Sum.inr (mkComplex ⟨φ, hφ⟩, 1)) =
    φ

Tactic:
by simp [(embedding_mk_eq φ).resolve_left hw]

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

Tactic:
by positivity

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
⊢ 0 ≤ (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal

Tactic:
by positivity

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
⊢ {w | w.LiesOver v ∧ IsRamified K w} ∪ unramifiedPlacesOver L v = {w | w.LiesOver v}

Tactic:
unramifiedPlacesOver,

Goal state after:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
⊢ {w | w.LiesOver v ∧ IsRamified K w} ∪ {w | w.LiesOver v ∧ IsUnramified K w} = {w | w.LiesOver v}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case 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₀, hw₀⟩).embedding ↑a).re| < 1 ∧
    |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2
w : InfinitePlace K
⊢ w ↑a < √(1 + ↑B ^ 2)

Tactic:
by_cases h_eq : w = w₀

Goal state after:
case pos
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₀, hw₀⟩).embedding ↑a).re| < 1 ∧
    |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ w ↑a < √(1 + ↑B ^ 2)

case neg
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₀, hw₀⟩).embedding ↑a).re| < 1 ∧
    |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2
w : InfinitePlace K
h_eq : ¬w = w₀
⊢ w ↑a < √(1 + ↑B ^ 2)
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
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₀
⊢ 0 ≤ (w₀.embedding ↑a).re ^ 2 + (w₀.embedding ↑a).im ^ 2

Tactic:
by positivity

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_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd : ↑(finrank ℚ K) ^ finrank ℚ K / ((4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial) ≤ √|↑(discr K)|
⊢ 0 ≤ ↑(finrank ℚ K) ^ finrank ℚ K / ((4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial)

Tactic:
by positivity

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_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd : ↑(finrank ℚ K) ^ finrank ℚ K / ((4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial) ≤ √|↑(discr K)|
⊢ 0 ≤ |↑(discr K)|

Tactic:
by positivity

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_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd : 1 ≤ (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
⊢ 0 < (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial

Tactic:
by positivity

Goal state after:
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)
⊢ 0 ≤ ↑(finrank ℚ K) ^ 2 / (4 / π * ↑(finrank ℚ K).factorial ^ (2 * (↑(finrank ℚ K))⁻¹))

Tactic:
by positivity

Goal state after:
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)
⊢ 0 ≤ ↑|discr K| ^ (↑(finrank ℚ K))⁻¹

Tactic:
by positivity

Goal state after:
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)
⊢ 0 ≤ ↑(finrank ℚ K) ^ 2

Tactic:
by positivity

Goal state after:
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)
⊢ 0 ≤ 4 / π * ↑(finrank ℚ K).factorial ^ (2 * (↑(finrank ℚ K))⁻¹)

Tactic:
by positivity

Goal state after:
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)
⊢ 0 ≤ ↑|discr K|

Tactic:
by positivity

Goal state after:
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)
⊢ 0 ≤ 4 / π

Tactic:
by positivity

Goal state after:
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)
⊢ 0 ≤ ↑(finrank ℚ K).factorial ^ (2 * (↑(finrank ℚ K))⁻¹)

Tactic:
by positivity

Goal state after:
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)
⊢ 0 ≤ ↑(finrank ℚ K).factorial

Tactic:
by positivity

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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w // w.IsReal }), x.1 w ≠ 0
x✝ : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
w : { w // w.IsReal }
hw : w ∉ s
⊢ ((negAt s) (fun w ↦ ‖x.1 w‖, x.2)).1 w = x.1 w

Tactic:
· simp [negAt_apply_isReal_and_notMem _ hw, abs_of_pos (h₂ w hw)]

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
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this✝⁸ : IsIntegralClosure B A L
this✝⁷ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
this✝⁶ : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝⁵ : Algebra Aₘ K := f.toAlgebra
this✝⁴ : IsScalarTower A Aₘ K
this✝³ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯
this✝² : Algebra Bₘ L := g.toAlgebra
this✝¹ : IsScalarTower B Bₘ L
this✝ : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra
this : IsScalarTower Aₘ K L
⊢ algebraMap A L = (algebraMap B L).comp (algebraMap A B)

Tactic:
← IsScalarTower.algebraMap_eq

Goal state after:
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 : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this✝⁸ : IsIntegralClosure B A L
this✝⁷ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
this✝⁶ : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝⁵ : Algebra Aₘ K := f.toAlgebra
this✝⁴ : IsScalarTower A Aₘ K
this✝³ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯
this✝² : Algebra Bₘ L := g.toAlgebra
this✝¹ : IsScalarTower B Bₘ L
this✝ : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra
this : IsScalarTower Aₘ K L
⊢ algebraMap A L = algebraMap A L