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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
hx : (mixedEmbedding K) ↑x ∈ integerSet K
⊢ ↑(preimageOfMemIntegerSet ⟨(mixedEmbedding K) ↑x, hx⟩) = x

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : 𝓞 K
hx : mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) x)) ≠ 0
hu : u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x) ∈ fundamentalCone K
⊢ (mixedEmbedding K) ↑(↑u * x) = u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ Measurable fun x ↦ ∏ w, ENNReal.ofReal (x.1 ↑w)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ≠ 0
hx' : x ∈ ⇑(mixedEmbedding K) '' Set.range ⇑(algebraMap (𝓞 K) K)
⊢ ∃ u, u • x ∈ integerSet K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
a : 𝓞 K
hx : (mixedEmbedding K) ↑a ∈ integerSet K
⊢ (mixedEmbedding K) ↑(↑ζ * a) = ζ • (mixedEmbedding K) ↑a

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
hx : x ∈ integerSet K
⊢ ζ • x ∈ integerSet K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
⊢ volume A =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
⊢ (complexConj K) ↑x = ↑x ↔ ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = ↑x

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
x✝² x✝¹ : ↥(torsion K)
x✝ : ↑(integerSet K)
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
x✝ : ↑(integerSet K)
⊢ 1 • x✝ = x✝

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
x✝ : ∃ v, (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u
v : (𝓞 ↥K⁺)ˣ
hv : (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u
⊢ (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
⊢ ↑(intNorm a) = mixedEmbedding.norm ↑a

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
x✝ : ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
⊢ IsUnit y

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
x✝ : ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
this : IsUnit y
⊢ (algebraMap (𝓞 ↥K⁺) K) ↑this.unit = (algebraMap (𝓞 K) K) ↑u

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a b : ↑(integerSet K)
x✝ : a ≈ b
u : ↥(torsion K)
hu : (fun m ↦ m • b) u = a
⊢ intNorm a = intNorm b

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
⊢ (complexConj K) ((algebraMap (𝓞 K) K) ↑u) = (algebraMap (𝓞 K) K) ↑u ↔
    ∃ v, (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x✝¹ x✝ : K
⊢ (complexConj K) (x✝¹ * x✝) = (complexConj K) x✝ * (complexConj K) x✝¹

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x✝¹ x✝ : K
⊢ (complexConj K) (x✝¹ + x✝) = (complexConj K) x✝¹ + (complexConj K) x✝

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
⊢ ∃ u, u • (mixedEmbedding K) ↑↑x ∈ integerSet K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
⊢ (ringOfIntegersComplexConj K) x = x ↔ x ∈ Set.range ⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K))

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
⊢ u ∈ realUnits K ↔ ∃ v, (algebraMap (𝓞 ↥K⁺) (𝓞 K)) ↑v = ↑u

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
⊢ normAtAllPlaces '' A ∩ ⋂ w, {x | x ↑w ≠ 0} = normAtComplexPlaces '' plusPart A

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
⊢ (unitsComplexConj K) u = u ↔ u ∈ realUnits K

Tactic:
by

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

Goal state before:
pp: case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ preimageOfMemIntegerSet ⟨u • (mixedEmbedding K) ↑↑x, hu⟩ * ↑(unitsNonZeroDivisorsEquiv.symm u⁻¹) = x

Tactic:
simp_rw [Subtype.ext_iff, RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff,
    Submonoid.coe_mul, map_mul, mixedEmbedding_preimageOfMemIntegerSet,
    unitSMul_smul, ← map_mul, mul_comm, map_inv, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe,
    Units.mul_inv_cancel_right]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
x : mixedSpace K
⊢ x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Surjective (integerSetToAssociates K)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
ζ : ↥(torsion K)
⊢ (complexConj K) ((algebraMap (𝓞 K) K) ↑↑ζ) = ((algebraMap (𝓞 K) K) ↑↑ζ)⁻¹

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
ζ : ↥(torsion K)
⊢ (unitsComplexConj K) ↑ζ = ↑ζ⁻¹

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x✝ : InfinitePlace K
⊢ x✝ ((algebraMap (𝓞 K) K) ↑(u * ((unitsComplexConj K) u)⁻¹)) = 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ ⟨1 * ((unitsComplexConj K) 1)⁻¹, ⋯⟩ = 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ ∀ (x y : (𝓞 K)ˣ),
    ⟨x * y * ((unitsComplexConj K) (x * y))⁻¹, ⋯⟩ =
      ⟨x * ((unitsComplexConj K) x)⁻¹, ⋯⟩ * ⟨y * ((unitsComplexConj K) y)⁻¹, ⋯⟩

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
ζ : ↥(torsion K)
⊢ ↑((unitsMulComplexConjInv K) ↑ζ) = ↑(ζ ^ 2)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
x✝ : ∃ u, (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
u : (↥(𝓞 K)⁰)ˣ
h : (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
⊢ ↑⟨unitsNonZeroDivisorsEquiv u, ?m.50⟩ • ↑a = ↑b

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
ζ : ↥(torsion K)
⊢ ((unitsMulComplexConjInv K).domRestrict (torsion K)) ζ = (powMonoidHom 2) ζ

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ Subgroup.map (unitsMulComplexConjInv K) (torsion K) = (powMonoidHom 2).range

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
x✝ : ∃ ζ, ↑ζ • ↑a = ↑b
u : (𝓞 K)ˣ
property✝ : u ∈ torsion K
h : ↑⟨u, property✝⟩ • ↑a = ↑b
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑(unitsNonZeroDivisorsEquiv.symm u)) * ↑a = ↑b

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
x✝ : ∃ u, (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
u : (↥(𝓞 K)⁰)ˣ
h : (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
⊢ unitsNonZeroDivisorsEquiv u • ↑a ∈ fundamentalCone K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
⊢ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ (unitsMulComplexConjInv K).ker = realUnits K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
⊢ integerSetToAssociates K a = integerSetToAssociates K b ↔ ∃ ζ, ζ • a = b

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : (powMonoidHom 2).range.index = 2
ζ : ↥(torsion K)
⊢ ↑((unitsMulComplexConjInv K) ↑ζ) = ↑((powMonoidHom 2) ζ)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : (powMonoidHom 2).range.index = 2
⊢ (unitsMulComplexConjInv K).range.index ∣ 2

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
⊢ Setoid.ker (integerSetToAssociates K) = MulAction.orbitRel ↥(torsion K) ↑(integerSet K)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ (unitsMulComplexConjInv K).range.index ∣ 2

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
⊢ MulAction.stabilizer (↥(torsion K)) a = ⊥

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
⊢ (a : Quotient (MulAction.orbitRel ↥(Units.torsion K) ↑(integerSet K))) →
    ↥(Units.torsion K) ⧸ MulAction.stabilizer (↥(Units.torsion K)) a.out ≃ ↥(Units.torsion K)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
h₁ : indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2
h₂ : (unitsMulComplexConjInv K).range.index = 1
⊢ indexRealUnits K = 2

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
n : ℕ
x✝ : ↑(integerSet K)
⊢ mixedEmbedding.norm ↑x✝ = ↑n ↔ absNorm ↑↑((integerSetEquiv K) x✝).1 = n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
h₁ : indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2
h₂ : (unitsMulComplexConjInv K).range.index = 2
⊢ indexRealUnits K = 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ indexRealUnits K = 1 ∨ indexRealUnits K = 2

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
⊢ volume A =
    2 ^ nrRealPlaces K * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
⊢ (normAtPlace w) (mixedSpaceOfRealSpace (normAtAllPlaces x)) = (normAtPlace w) x

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ mixedEmbedding.norm (mixedSpaceOfRealSpace (normAtAllPlaces x)) = mixedEmbedding.norm x

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ mixedSpaceOfRealSpace (normAtAllPlaces x) ∈
      logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) \
        {x | mixedEmbedding.norm x = 0} ↔
    x ∈
      logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) \
        {x | mixedEmbedding.norm x = 0}

Tactic:
Set.mem_sdiff,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ mixedSpaceOfRealSpace (normAtAllPlaces x) ∈
        logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ∧
      mixedSpaceOfRealSpace (normAtAllPlaces x) ∉ {x | mixedEmbedding.norm x = 0} ↔
    x ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ∧
      x ∉ {x | mixedEmbedding.norm x = 0}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
a : { a // mixedEmbedding.norm ↑a = ↑n }
⊢ ↑↑((integerSetEquivNorm K n) a).1 = Ideal.span {↑(preimageOfMemIntegerSet ↑a)}

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
⊢ Nat.card ↑{I | IsPrincipal ↑I ∧ absNorm ↑I = n} * torsionOrder K = Nat.card ↑{a | mixedEmbedding.norm ↑a = ↑n}

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ mixedSpaceOfRealSpace (normAtAllPlaces x) ∈ fundamentalCone K ↔ x ∈ fundamentalCone K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : (∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤) ↔ (unitsMulComplexConjInv K).range.index = 1
⊢ indexRealUnits K = 2 ↔ ∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ normLeOne K = normAtAllPlaces ⁻¹' normAtAllPlaces '' normLeOne K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ (x ∈ fundamentalCone K ∧ ∃ a, ∃ (_ : ∃ x' ∈ ↑J, (algebraMap (𝓞 K) K) x' = a), (mixedEmbedding K) a = x) ↔
    x ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x

Tactic:
exists_prop',

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ (x ∈ fundamentalCone K ∧ ∃ a, Nonempty (∃ x' ∈ ↑J, (algebraMap (𝓞 K) K) x' = a) ∧ (mixedEmbedding K) a = x) ↔
    x ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ indexRealUnits K = 2 ↔ ∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (torsion ↥K⁺) ≤ torsion K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ x ∈ idealSet K J ↔ x ∈ fundamentalCone K ∧ ∃ a ∈ ↑↑J, (mixedEmbedding K) ↑a = x

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
⊢ ↑(preimageOfMemIntegerSet (idealSetMap K J a)) ∈ ↑↑J

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
x✝¹ x✝ : ↑(idealSet K J)
h : (fun a ↦ ⟨idealSetMap K J a, ⋯⟩) x✝¹ = (fun a ↦ ⟨idealSetMap K J a, ⋯⟩) x✝
⊢ x✝¹ = x✝

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : { a // ↑(preimageOfMemIntegerSet a) ∈ ↑↑J }
⊢ ↑((idealSetEquiv K J).symm a) = ↑↑a

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
⊢ ↑(intNorm ↑((idealSetEquiv K J) a)) = mixedEmbedding.norm ↑a

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
⊢ ↑(intNorm ↑((idealSetEquiv K J) a)) = mixedEmbedding.norm ↑a

Tactic:
by
  rw [intNorm_coe, idealSetEquiv_apply]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
⊢ { a // mixedEmbedding.norm ↑a = ↑n } ≃ { a // mixedEmbedding.norm ↑↑a = ↑n }

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
x✝ : ↑(integerSet K)
⊢ mixedEmbedding.norm ↑x✝ = ↑n ∧ ↑(preimageOfMemIntegerSet x✝) ∈ ↑J ↔
    ↑(preimageOfMemIntegerSet x✝) ∈ ↑J ∧ mixedEmbedding.norm ↑x✝ = ↑n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
⊢ { a // ↑(preimageOfMemIntegerSet ↑a) ∈ ↑J } ≃ { I // ↑J ∣ ↑↑I.1 }

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
x✝¹ : ↥(Units.torsion K)
x✝ : ↥(Ideal (𝓞 K))⁰
⊢ (IsPrincipal ↑x✝ ∧ absNorm ↑x✝ = n) ∧ ↑J ∣ ↑x✝ ↔ ↑J ∣ ↑x✝ ∧ IsPrincipal ↑x✝ ∧ absNorm ↑x✝ = n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ Subgroup.closure (Set.range (realFundSystem K)) ⊔ torsion K = realUnits K ⊔ torsion K

Tactic:
by

Goal state after: