mathlib-initiative/mathlib-tactics huggingface dataset:
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
  have hA' {x} : (A.indicator 1 x : ℝ≥0∞) =
      (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x) := by
    simp_rw [← Set.indicator_comp_right, Function.comp_def, Pi.one_def, hA]
  rw [← lintegral_indicator_one hm, ← lintegral_comp_polarSpaceCoord_symm, polarSpaceCoord_target',
    Measure.volume_eq_prod, setLIntegral_prod]
  · simp_rw [hA', normAtComplexPlaces_polarSpaceCoord_symm, lintegral_const, restrict_apply
      MeasurableSet.univ, Set.univ_inter, volume_pi, Measure.pi_pi, volume_Ioo, sub_neg_eq_add,
      ← two_mul, Finset.prod_const, Finset.card_univ, ← Set.indicator_const_mul,
      ← Set.indicator_comp_right, Function.comp_def, Pi.one_apply, mul_one]
    rw [lintegral_mul_const' _ _ (ne_of_beq_false rfl).symm, mul_comm]
    erw [setLIntegral_indicator (by convert! hm.preimage mixedSpaceOfRealSpace.measurable)]
    rw [hA, volume_eq_two_pi_pow_mul_integral_aux hA]
    congr 1
    refine setLIntegral_congr (ae_eq_set_inter (by rfl) (Measure.ae_eq_set_pi fun w _ ↦ ?_))
    split_ifs
    exacts [ae_eq_rfl, Ioi_ae_eq_Ici]
  · exact (Measurable.mul (by fun_prop)
      <| measurable_const.indicator <| hm.preimage (measurable_polarSpaceCoord_symm K)).aemeasurable

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

Goal state before:
pp: case refine_2.refine_1.inl
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha₁ : a ∈ A
ha₂ : a ∈ {x | ∀ (w : { w // w.IsReal }), 0 < x.1 w}
w : InfinitePlace K
hw : w.IsReal
⊢ normAtAllPlaces a w = normAtComplexPlaces a w

Tactic:
simpa using

Goal state after:
case refine_2.refine_1.inl
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha₁ : a ∈ A
ha₂ : a ∈ {x | ∀ (w : { w // w.IsReal }), 0 < x.1 w}
w : InfinitePlace K
hw : w.IsReal
⊢ 0 ≤ a.1 ⟨w, hw⟩
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_2.refine_2
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha₁ : a ∈ A
ha₂ : a ∈ {x | ∀ (w : { w // w.IsReal }), 0 < x.1 w}
w : { w // w.IsReal }
⊢ normAtComplexPlaces a ∈ {x | x ↑w ≠ 0}

Tactic:
simpa using

Goal state after:
case refine_2.refine_2
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha₁ : a ∈ A
ha₂ : a ∈ {x | ∀ (w : { w // w.IsReal }), 0 < x.1 w}
w : { w // w.IsReal }
⊢ ¬a.1 w = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_2.refine_2
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha₁ : a ∈ A
ha₂ : a ∈ {x | ∀ (w : { w // w.IsReal }), 0 < x.1 w}
w : { w // w.IsReal }
⊢ normAtComplexPlaces a ∈ {x | x ↑w ≠ 0}

Tactic:
· simpa [Set.mem_ofPred_eq, normAtComplexPlaces_apply_isReal] using (ha₂ w).ne'

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:
simpa using

Goal state after:
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
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
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:
simpa using

Goal state after:
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) ↑u) * ↑a = ↑b
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:
simpa using

Goal state after:
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
⊢ ↑b ∈ fundamentalCone K
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
x✝ : InfinitePlace L
h : x✝ ∈ (ramifiedPlacesOver L v).toFinset
⊢ x✝ ∈ ramifiedPlacesOver L v

Tactic:
simpa using

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
x✝ : InfinitePlace L
h : x✝ ∈ (ramifiedPlacesOver L v).toFinset
⊢ x✝ ∈ ramifiedPlacesOver L v
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case refine_2
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
this : L = ⊤
⊢ E ⊔ maximalRealSubfield K = ⊤

Tactic:
simpa using

Goal state after:
case refine_2
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
this : L = ⊤
⊢ E ⊔ maximalRealSubfield K = ⊤
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
x✝ : InfinitePlace L
h : x✝ ∈ (unramifiedPlacesOver L v).toFinset
⊢ x✝ ∈ unramifiedPlacesOver L v

Tactic:
simpa using

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
x✝ : InfinitePlace L
h : x✝ ∈ (unramifiedPlacesOver L v).toFinset
⊢ x✝ ∈ unramifiedPlacesOver L v
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
inst✝ : IsCyclotomicExtension S ℚ K
this✝² : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this✝¹ : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
this✝ : IsCyclotomicExtension {n} ℚ ↥ℚ⟮ζ⟯
this : IsTotallyComplex ↥ℚ⟮ζ⟯
⊢ IsTotallyComplex K

Tactic:
exact isTotallyComplex_of_algebra ℚ⟮ζ⟯ K

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f : ℕ
hK : Fintype.card K = p ^ f
h0 : f = 0
⊢ Fintype.card K ≤ 1

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f : ℕ
hK : Fintype.card K = p ^ f
h0 : f = 0
⊢ Fintype.card K ≤ 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ mixedEmbedding.norm (mixedSpaceOfRealSpace (↑expMapBasis x)) = Real.exp (x w₀) ^ finrank ℚ K

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ∏ x_1, ↑expMapBasis x x_1 ^ x_1.mult = Real.exp (x w₀) ^ finrank ℚ K
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hPirr : Irreducible P
A : K[X]
hA : cyclotomic n K = P * A
hQ : P * C P.leadingCoeff⁻¹ ∣ cyclotomic n K
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hPirr : Irreducible P
A : K[X]
hA : cyclotomic n K = P * A
hQ : P * C P.leadingCoeff⁻¹ ∣ cyclotomic n K
⊢ (P * C P.leadingCoeff⁻¹).natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
P : (ZMod p)[X]
hpn : ¬p ∣ n
hP : P ∣ cyclotomic n (ZMod p)
hPdeg : P.natDegree = orderOf (unitOfCoprime p ⋯)
⊢ p.Coprime n

Tactic:
simpa using

Goal state after:
p n : ℕ
hp : Fact (Nat.Prime p)
P : (ZMod p)[X]
hpn : ¬p ∣ n
hP : P ∣ cyclotomic n (ZMod p)
hPdeg : P.natDegree = orderOf (unitOfCoprime p ⋯)
⊢ p.Coprime n
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : ζ ^ n = 1
hζ1 : ζ ≠ 1
key : ↑n = ∑ i ∈ range n, (1 - ζ ^ i)
i : ℕ
x✝ : i ∈ range n
⊢ ζ - 1 ∣ ζ ^ i - 1

Tactic:
simpa using

Goal state after:
n : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : ζ ^ n = 1
hζ1 : ζ ≠ 1
key : ↑n = ∑ i ∈ range n, (1 - ζ ^ i)
i : ℕ
x✝ : i ∈ range n
⊢ ζ - 1 ∣ ζ ^ i - 1
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: case inr
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this✝ : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ ↑(nthRootsFinset p 1)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ ↑(nthRootsFinset p 1)
e : ζ ^ i ≠ ζ ^ j
this :
  ∀ {p : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [inst_1 : IsDomain A],
    IsPrimitiveRoot ζ p →
      Nat.Prime p →
        NeZero p →
          ∀ i < p,
            ζ ^ i ∈ ↑(nthRootsFinset p 1) →
              ∀ j < p, ζ ^ j ∈ ↑(nthRootsFinset p 1) → ζ ^ i ≠ ζ ^ j → j ≤ i → Associated (ζ - 1) (ζ ^ i - ζ ^ j)
hij : ¬j ≤ i
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)

Tactic:
simpa using

Goal state after:
case inr
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this✝ : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ ↑(nthRootsFinset p 1)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ ↑(nthRootsFinset p 1)
e : ζ ^ i ≠ ζ ^ j
this :
  ∀ {p : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [inst_1 : IsDomain A],
    IsPrimitiveRoot ζ p →
      Nat.Prime p →
        NeZero p →
          ∀ i < p,
            ζ ^ i ∈ ↑(nthRootsFinset p 1) →
              ∀ j < p, ζ ^ j ∈ ↑(nthRootsFinset p 1) → ζ ^ i ≠ ζ ^ j → j ≤ i → Associated (ζ - 1) (ζ ^ i - ζ ^ j)
hij : ¬j ≤ i
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)
Module: Mathlib.NumberTheory.NumberField.Ideal.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
I : Ideal (𝓞 K)
inst✝¹ : NumberField K
n : ℕ
inst✝ : NeZero n
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime n
x✝ : ↥(rootsOfUnity n (𝓞 K))
ζ : (𝓞 K)ˣ
hζ✝ : ζ ∈ rootsOfUnity n (𝓞 K)
h : (I.rootsOfUnityMapQuot n) ⟨ζ, hζ✝⟩ = 1
t : ℕ
ht₀ : t ≠ 0
ht : t ∣ n
hζ : IsPrimitiveRoot ζ t
this : ¬2 ≤ t
⊢ ⟨ζ, hζ✝⟩ = 1

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝² : Field K
I : Ideal (𝓞 K)
inst✝¹ : NumberField K
n : ℕ
inst✝ : NeZero n
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime n
x✝ : ↥(rootsOfUnity n (𝓞 K))
ζ : (𝓞 K)ˣ
hζ✝ : ζ ∈ rootsOfUnity n (𝓞 K)
h : (I.rootsOfUnityMapQuot n) ⟨ζ, hζ✝⟩ = 1
t : ℕ
ht₀ : t ≠ 0
ht : t ∣ n
hζ : IsPrimitiveRoot ζ t
this : ¬2 ≤ t
⊢ ζ = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 < x w
h : ∀ (i : InfinitePlace K), ↑expMapBasis.symm x i ∈ if i = w₀ then Set.Iic 0 else Set.Ico 0 1
w : InfinitePlace K
hw : ¬w = w₀
⊢ ↑expMapBasis.symm x w ∈ Set.Ico 0 1

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 < x w
h : ∀ (i : InfinitePlace K), ↑expMapBasis.symm x i ∈ if i = w₀ then Set.Iic 0 else Set.Ico 0 1
w : InfinitePlace K
hw : ¬w = w₀
⊢ 0 ≤ ↑expMapBasis.symm x w ∧ ↑expMapBasis.symm x w < 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 < x w
h : ∀ (i : InfinitePlace K), ↑expMapBasis.symm x i ∈ if i = w₀ then Set.Iic 0 else Set.Ico 0 1
⊢ ↑expMapBasis.symm x w₀ ≤ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 < x w
h : ∀ (i : InfinitePlace K), ↑expMapBasis.symm x i ∈ if i = w₀ then Set.Iic 0 else Set.Ico 0 1
⊢ ↑expMapBasis.symm x w₀ ≤ 0
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ absNorm (span {hζ.toInteger - 1}) = p

Tactic:
simpa using

Goal state after:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ ((Algebra.norm ℤ) (hζ.toInteger - 1)).natAbs = p
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: case e'_5
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ p = absNorm (span {hζ.toInteger - 1})

pp: case convert_3
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ IsDedekindDomain (𝓞 K)

pp: case convert_4
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ Module.Free ℤ (𝓞 K)

Tactic:
exact (absNorm_span_zeta_sub_one ..).symm

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
h : (span {hζ.toInteger - 1}).IsPrime
⊢ 𝒑 ≠ ⊥

Tactic:
simpa using

Goal state after:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
h : (span {hζ.toInteger - 1}).IsPrime
⊢ ¬p = 0
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
σ : Gal(K/ℚ)
hσ : σ ∈ stabilizer Gal(K/ℚ) P
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/ℤ ⧸ span {↑p}) :=
  (IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩
this✝ : CharP (ℤ ⧸ span {↑p}) p
this : Finite (𝓞 K ⧸ P)
i : ℕ
hi : ∀ (x : 𝓞 K ⧸ P), τ x = x ^ Nat.card (ℤ ⧸ span {↑p}) ^ i
⊢ absNorm P ≠ 1

Tactic:
simpa using

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
σ : Gal(K/ℚ)
hσ : σ ∈ stabilizer Gal(K/ℚ) P
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/ℤ ⧸ span {↑p}) :=
  (IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩
this✝ : CharP (ℤ ⧸ span {↑p}) p
this : Finite (𝓞 K ⧸ P)
i : ℕ
hi : ∀ (x : 𝓞 K ⧸ P), τ x = x ^ Nat.card (ℤ ⧸ span {↑p}) ^ i
⊢ ¬P = ⊤
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
σ : Gal(K/ℚ)
hσ : σ ∈ stabilizer Gal(K/ℚ) P
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/ℤ ⧸ span {↑p}) :=
  (IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩
this✝ : CharP (ℤ ⧸ span {↑p}) p
this : Finite (𝓞 K ⧸ P)
i : ℕ
hi : ∀ (x : 𝓞 K ⧸ P), τ x = x ^ Nat.card (ℤ ⧸ span {↑p}) ^ i
⊢ IsPrimitiveRoot ((Ideal.Quotient.mk P) hζ.toInteger) n

Tactic:
refine hζ.toInteger_isPrimitiveRoot.idealQuotient_mk
      (by simpa using IsMaximal.ne_top inferInstance) ?_

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
σ : Gal(K/ℚ)
hσ : σ ∈ stabilizer Gal(K/ℚ) P
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/ℤ ⧸ span {↑p}) :=
  (IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩
this✝ : CharP (ℤ ⧸ span {↑p}) p
this : Finite (𝓞 K ⧸ P)
i : ℕ
hi : ∀ (x : 𝓞 K ⧸ P), τ x = x ^ Nat.card (ℤ ⧸ span {↑p}) ^ i
⊢ (absNorm P).Coprime n
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
w : InfinitePlace K
h : ¬w = w₀
⊢ y w ∈ Set.Icc 0 1

Tactic:
simpa using

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
w : InfinitePlace K
h : ¬w = w₀
⊢ 0 ≤ y w ∧ y w ≤ 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
hc' : 0 < c
w : InfinitePlace K
h : w = w₀
⊢ 0 = y w

Tactic:
simpa using

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
hc' : 0 < c
w : InfinitePlace K
h : w = w₀
⊢ 0 = y w₀
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
inst✝ : NeZero p
η : K
hη : IsPrimitiveRoot η p
i : ℕ
hi : i.Coprime p
hζη : ζ ^ i = η
⊢ Associated (hζ.toInteger - 1) (hζ.toInteger ^ i - 1)

Tactic:
exact hζ.toInteger_isPrimitiveRoot.associated_sub_one_pow_sub_one_of_coprime hi

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
η : 𝓞 K
hη : η ∈ primitiveRoots p (𝓞 K)
hη' : IsPrimitiveRoot (↑η) p
⊢ Associated (hζ.toInteger - 1) (1 - η)

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
η : 𝓞 K
hη : η ∈ primitiveRoots p (𝓞 K)
hη' : IsPrimitiveRoot (↑η) p
⊢ Associated (hζ.toInteger - 1) (1 - η)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1
hx₀ : ↑expMapBasis y ≠ 0
⊢ y w₀ ≤ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1
hx₀ : ↑expMapBasis y ≠ 0
⊢ y w₀ ≤ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1
hx₀ : ↑expMapBasis y ≠ 0
w : InfinitePlace K
h : ¬w = w₀
⊢ y w ∈ Set.Icc 0 1

Tactic:
simpa using

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1
hx₀ : ↑expMapBasis y ≠ 0
w : InfinitePlace K
h : ¬w = w₀
⊢ 0 ≤ y w ∧ y w ≤ 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1
hx₀ : ↑expMapBasis y ≠ 0
w : InfinitePlace K
⊢ (if w = w₀ then 0 else y w) ∈ if w = w₀ then {0} else Set.Icc 0 1

Tactic:
split_ifs with h
    · rfl
    · simpa [h] using hy w (Set.mem_univ _)

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx₀ : x = 0
⊢ x ∈ compactSet K ↔ x ∈ ↑expMapBasis '' closure (paramSet K) ∪ {0}

Tactic:
simpa using

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx₀ : x = 0
⊢ 0 ∈ compactSet K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx₀ : ¬x = 0
hx : x ∈ ↑expMapBasis '' closure (paramSet K)
⊢ x ∈ compactSet K

Tactic:
exact compactSet_eq_union_aux₂ hx₀ hx

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : IsBounded (↑expMapBasis '' paramSet K)
C : ℝ
hC : ∀ x ∈ ↑expMapBasis '' paramSet K, ‖x‖ ≤ C
x : mixedSpace K
hx : x ∈ normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K
⊢ ‖x‖ ≤ C

Tactic:
norm_eq_sup'_normAtPlace

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : IsBounded (↑expMapBasis '' paramSet K)
C : ℝ
hC : ∀ x ∈ ↑expMapBasis '' paramSet K, ‖x‖ ≤ C
x : mixedSpace K
hx : x ∈ normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K
⊢ (univ.sup' ⋯ fun w ↦ (normAtPlace w) x) ≤ C
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : IsBounded (↑expMapBasis '' paramSet K)
C : ℝ
hC : ∀ x ∈ ↑expMapBasis '' paramSet K, ‖x‖ ≤ C
x : mixedSpace K
hx : x ∈ normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K
w : InfinitePlace K
x✝ : w ∈ univ
⊢ (normAtPlace w) x ≤ C

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : IsBounded (↑expMapBasis '' paramSet K)
C : ℝ
hC : ∀ x ∈ ↑expMapBasis '' paramSet K, ‖x‖ ≤ C
x : mixedSpace K
hx : x ∈ normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K
w : InfinitePlace K
x✝ : w ∈ univ
⊢ (normAtPlace w) x ≤ C