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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
⊢ (span ℤ (Set.range ⇑(basisOfIsMaxRank hu))).toAddSubgroup =
    AddSubgroup.map (logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u)))

Tactic:
rw [Subgroup.toAddSubgroup_closure, AddMonoidHom.map_closure, ← span_int_eq_addSubgroupClosure]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
⊢ (span ℤ (Set.range ⇑(basisOfIsMaxRank hu))).toAddSubgroup =
    (span ℤ (⇑(logEmbedding K) '' ⇑Additive.toMul ⁻¹' Set.range u)).toAddSubgroup
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : polarSpace K
⊢ (x✝ ∈ ⇑(homeoRealMixedSpacePolarSpace K).symm ⁻¹' Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target) ↔
    x✝ ∈ (Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ Set.univ.pi fun x ↦ Set.Ioo (-π) π

Tactic:
Set.mem_preimage,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : polarSpace K
⊢ ((homeoRealMixedSpacePolarSpace K).symm x✝ ∈ Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target) ↔
    x✝ ∈ (Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ Set.univ.pi fun x ↦ Set.Ioo (-π) π
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
x : realSpace K
⊢ x ∈ normAtComplexPlaces '' A ↔
    x ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0

Tactic:
refine ⟨?_, fun ⟨hx₁, hx₂⟩ ↦ ?_⟩

Goal state after:
case refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
x : realSpace K
⊢ x ∈ normAtComplexPlaces '' A →
    x ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0

case refine_2
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
x : realSpace K
x✝ : x ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
hx₁ : x ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A
hx₂ : x ∈ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
⊢ x ∈ normAtComplexPlaces '' A
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
a : mixedSpace K
ha : a ∈ A
⊢ normAtComplexPlaces a ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A

Tactic:
Set.mem_preimage,

Goal state after:
case refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
a : mixedSpace K
ha : a ∈ A
⊢ mixedSpaceOfRealSpace (normAtComplexPlaces a) ∈ A
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
a : mixedSpace K
ha : a ∈ A
⊢ mixedSpaceOfRealSpace (normAtComplexPlaces a) ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A

Tactic:
Set.mem_preimage,

Goal state after:
case refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
a : mixedSpace K
ha : a ∈ A
⊢ normAtComplexPlaces (mixedSpaceOfRealSpace (normAtComplexPlaces a)) ∈ normAtComplexPlaces '' A
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
x : realSpace K
x✝ : x ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
hx₁ : x ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A
hx₂ : x ∈ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
⊢ x ∈ normAtComplexPlaces '' A

Tactic:
Set.mem_preimage,

Goal state after:
case refine_2
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
x : realSpace K
x✝ : x ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
hx₁ : mixedSpaceOfRealSpace x ∈ A
hx₂ : x ∈ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
⊢ x ∈ normAtComplexPlaces '' A
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
x : realSpace K
x✝ : x ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
hx₁ : mixedSpaceOfRealSpace x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A
hx₂ : x ∈ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
⊢ x ∈ normAtComplexPlaces '' A

Tactic:
Set.mem_preimage,

Goal state after:
case refine_2
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
x : realSpace K
x✝ : x ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
hx₁ : normAtComplexPlaces (mixedSpaceOfRealSpace x) ∈ normAtComplexPlaces '' A
hx₂ : x ∈ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
⊢ x ∈ normAtComplexPlaces '' A
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasurableSet {x | mixedEmbedding.norm x = 0}

Tactic:
exact measurableSet_eq_fun (mixedEmbedding.continuous_norm K).measurable measurable_const

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
hx : x ∈ fundamentalCone K
hy : ∀ (w : InfinitePlace K), (normAtPlace w) y = (normAtPlace w) x
⊢ y ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
Set.mem_preimage,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : x ∈ fundamentalCone K
hy : ∀ (w : InfinitePlace K), (normAtPlace w) y = (normAtPlace w) x
⊢ logMap y ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ c • x ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
Set.mem_preimage,

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ logMap (c • x) ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
u : Additive (𝓞 K)ˣ
left✝ : u ∈ ↑⊤
hu : ↑⟨(logEmbedding K).toIntLinearMap u, ⋯⟩ + logMap x ∈ ZSpan.fundamentalDomain B
⊢ u • x ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
Set.mem_preimage,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
u : Additive (𝓞 K)ˣ
left✝ : u ∈ ↑⊤
hu : ↑⟨(logEmbedding K).toIntLinearMap u, ⋯⟩ + logMap x ∈ ZSpan.fundamentalDomain B
⊢ logMap (u • x) ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
⊢ ∃ u, u • x ∈ fundamentalCone K

Tactic:
classical
  let B := (basisUnitLattice K).ofZLatticeBasis ℝ
  rsuffices ⟨⟨_, ⟨u, _, rfl⟩⟩, hu⟩ : ∃ e : unitLattice K, e + logMap x ∈ ZSpan.fundamentalDomain B
  · exact ⟨u, by rwa [Set.mem_preimage, logMap_unit_smul u hx], by simp [hx]⟩
  · obtain ⟨⟨e, h₁⟩, h₂, -⟩ := ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)
    exact ⟨⟨e, by rwa [← Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]⟩, h₂⟩

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

Goal state before:
pp: case left
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ ζ • x ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
Set.mem_preimage,

Goal state after:
case left
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ logMap (ζ • x) ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_1.refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ : normAtAllPlaces a ∈ ⋂ w, {x | x ↑w ≠ 0}
⊢ mixedSpaceOfRealSpace (normAtAllPlaces a) ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A

Tactic:
Set.mem_preimage,

Goal state after:
case refine_1.refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ : normAtAllPlaces a ∈ ⋂ w, {x | x ↑w ≠ 0}
⊢ normAtAllPlaces (mixedSpaceOfRealSpace (normAtAllPlaces a)) ∈ normAtAllPlaces '' A
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 ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A

Tactic:
Set.mem_preimage,

Goal state after:
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
⊢ normAtAllPlaces x ∈ normAtAllPlaces '' A ↔ normAtAllPlaces (fun w ↦ ‖x.1 w‖, x.2) ∈ normAtAllPlaces '' A
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_1
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
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
⊢ x ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A

Tactic:
Set.mem_preimage,

Goal state after:
case refine_1
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
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
⊢ normAtAllPlaces x ∈ normAtAllPlaces '' A
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 h

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

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)) ∧
      mixedSpaceOfRealSpace (normAtAllPlaces x) ∉ {x | mixedEmbedding.norm x = 0} ↔
    x ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ∧
      x ∉ {x | mixedEmbedding.norm x = 0}

Tactic:
Set.mem_preimage,

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

Goal state before:
pp: case refine_1.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : mixedSpace K
h₃ : y ∈ {x | mixedEmbedding.norm x ≤ 1}
h₁ : y ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
h₂ : y ∉ {x | mixedEmbedding.norm x = 0}
⊢ normAtAllPlaces y ∈
    ⇑mixedSpaceOfRealSpace ⁻¹'
      logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
Set.mem_preimage,

Goal state after:
case refine_1.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : mixedSpace K
h₃ : y ∈ {x | mixedEmbedding.norm x ≤ 1}
h₁ : logMap y ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
h₂ : y ∉ {x | mixedEmbedding.norm x = 0}
⊢ normAtAllPlaces y ∈
    ⇑mixedSpaceOfRealSpace ⁻¹'
      logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ x ∈ normAtAllPlaces '' normLeOne K →
    x ∈
      ⇑mixedSpaceOfRealSpace ⁻¹'
              logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ∩
            {x | ∀ (w : InfinitePlace K), 0 ≤ x w} ∩
          {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≠ 0} ∩
        {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≤ 1}

Tactic:
rintro ⟨y, ⟨⟨h₁, h₂⟩, h₃⟩, rfl⟩
    refine ⟨⟨⟨?_, ?_⟩, ?_⟩, ?_⟩
    · rwa [Set.mem_preimage, ← logMap_normAtAllPlaces] at h₁
    · exact fun w ↦ normAtPlace_nonneg w y
    · rwa [Set.mem_ofPred_eq, ← norm_normAtAllPlaces] at h₂
    · rwa [Set.mem_ofPred_eq, ← norm_normAtAllPlaces] at h₃

Goal state after:
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
⊢ ∑ w ∈ (ramifiedPlacesOver L v ∪ unramifiedPlacesOver L v).toFinset, v.inertiaDeg w = Module.finrank K L

Tactic:
toFinset_union,

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
⊢ ∑ w ∈ (ramifiedPlacesOver L v).toFinset ∪ (unramifiedPlacesOver L v).toFinset, v.inertiaDeg w = Module.finrank K L
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 h

Goal state after:
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 h

Goal state after:
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
σ : Gal(K/ℚ)
x : 𝓞 K
hx : x ^ n = 1
⊢ (algebraMap (𝓞 K) K) (σ • x) = (algebraMap (𝓞 K) K) (x ^ (↑((galEquivZMod n K) σ)).val)

Tactic:
apply galEquivZMod_apply_of_pow_eq n K σ <| by rw [← Subalgebra.coe_pow, hx, OneMemClass.coe_one]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1) =ᵐ[volume]
    Set.univ.pi fun w ↦ if w = w₀ then Set.Iio 0 else Set.Ioo 0 1

Tactic:
volume_pi

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1) =ᵐ[Measure.pi fun x ↦ volume]
    Set.univ.pi fun w ↦ if w = w₀ then Set.Iio 0 else Set.Ioo 0 1
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
⊢ (fun x ↦ ZMod.unitOfCoprime p hn ^ x) ↑i = (galEquivZMod n K) σ

Tactic:
have h₀ : IsPrimitiveRoot (Ideal.Quotient.mk P hζ.toInteger) n := by
    refine hζ.toInteger_isPrimitiveRoot.idealQuotient_mk
      (by simpa using IsMaximal.ne_top inferInstance) ?_
    rw [← pow_inertiaDeg p]
    exact Nat.Coprime.pow_left _ hn

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
h₀ : IsPrimitiveRoot ((Ideal.Quotient.mk P) hζ.toInteger) n
⊢ (fun x ↦ ZMod.unitOfCoprime p hn ^ x) ↑i = (galEquivZMod n K) σ
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : CommRing 𝒪
inst✝² : Algebra 𝒪 K
inst✝¹ : IsIntegralClosure 𝒪 ℤ K
inst✝ : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
⊢ ∃ p, Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
have := (IsIntegralClosure.algebraMap_injective 𝒪 ℤ K).isDomain
  have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪
  have := IsIntegralClosure.isFractionRing_of_finite_extension ℤ ℚ K 𝒪
  have := IsIntegralClosure.finite ℤ ℚ K 𝒪
  have := CharZero.of_module (R := 𝒪) K
  let : MulSemiringAction Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
  have := IsGaloisGroup.of_isFractionRing Gal(K/ℚ) ℤ 𝒪 ℚ K
  obtain ⟨P, _, hP'⟩ := NumberField.exists_not_isUnramifiedAt_int (𝒪 := 𝒪) H.ne'
  obtain ⟨p, hp : _ = Ideal.span _⟩ := IsPrincipalIdealRing.principal (P.under ℤ)
  have hp0 : p ≠ 0 := fun hp0 ↦ Ideal.IsMaximal.ne_bot_of_isIntegral_int _
    (Ideal.eq_bot_of_comap_eq_bot (hp.trans (by aesop)))
  have : Prime p := by rw [← Ideal.span_singleton_prime hp0, ← hp]; infer_instance
  refine ⟨p.natAbs, Int.prime_iff_natAbs_prime.mp this, fun Q _ hQ ↦ ?_⟩
  replace hQ : (p : 𝒪) ∈ Q := Q.mem_of_dvd
    (map_dvd (algebraMap _ _) p.associated_natAbs.symm.dvd) (by simpa using hQ)
  have : .span {p} = Ideal.under ℤ Q :=
    ((Ideal.liesOver_span_iff Ideal.IsPrime.ne_top' this).mpr hQ).1
  rwa [← Ideal.ramificationIdx_eq_one_iff,
    ← Ideal.ramificationIdxIn_eq_ramificationIdx (Q.under ℤ) _ Gal(K/ℚ), ← this, ← hp,
    Ideal.ramificationIdxIn_eq_ramificationIdx _ P Gal(K/ℚ), Ideal.ramificationIdx_eq_one_iff]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x✝ : mixedSpace K
⊢ (∃ x,
      (x ∈ {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∧
          x ∈ ⇑↑↑(toMixed K) ⁻¹' ↑(idealLattice K ((FractionalIdeal.mk0 K) J))) ∧
        (↑(toMixed K)).toEquiv x = x✝) ↔
    (x✝ ∈ fundamentalCone K ∧ ∃ a ∈ ↑↑J, (mixedEmbedding K) ↑a = x✝) ∧ mixedEmbedding.norm x✝ ≤ s

Tactic:
Set.mem_preimage,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x✝ : mixedSpace K
⊢ (∃ x,
      (x ∈ {x | (toMixed K) x ∈ fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∧
          ↑↑(toMixed K) x ∈ ↑(idealLattice K ((FractionalIdeal.mk0 K) J))) ∧
        (↑(toMixed K)).toEquiv x = x✝) ↔
    (x✝ ∈ fundamentalCone K ∧ ∃ a ∈ ↑↑J, (mixedEmbedding K) ↑a = x✝) ∧ mixedEmbedding.norm x✝ ≤ s