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 y : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = (normAtPlace w) y
x✝ : { w // w ≠ w₀ }
⊢ logMap x x✝ = logMap y x✝

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = (normAtPlace w) y
x✝ : { w // w ≠ w₀ }
⊢ logMap x x✝ = logMap y x✝
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
x : mixedSpace K
⊢ A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
x : mixedSpace K
⊢ A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
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)
⊢ ∫⁻ (x : InfinitePlace K → ℝ) in Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
      ∫⁻ (y : { w // w.IsComplex } → ℝ) in Set.univ.pi fun x ↦ Set.Ioo (-π) π,
        (∏ x_1, ENNReal.ofReal (x ↑x_1)) * A.indicator 1 (↑(polarSpaceCoord K).symm (x, y)) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)

Tactic:
[

Goal state after:
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)
⊢ ∫⁻ (x : InfinitePlace K → ℝ) in Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
      ∫⁻ (y : { w // w.IsComplex } → ℝ) in Set.univ.pi fun x ↦ Set.Ioo (-π) π,
        (∏ x_1, ENNReal.ofReal (x ↑x_1)) * A.indicator 1 (↑(polarSpaceCoord K).symm (x, y)) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)
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 : ↑(integerSet K)
⊢ ⋯.choose ≠ 0

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a : ↑(integerSet K)
⊢ ⋯.choose ≠ 0
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:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
hx : (mixedEmbedding K) ↑x ∈ integerSet K
⊢ ↑(preimageOfMemIntegerSet ⟨(mixedEmbedding K) ↑x, hx⟩) = x
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:
[

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

Goal state after:
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✝)
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:
[

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

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

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
⊢ x ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ normAtAllPlaces ⁻¹' 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)
⊢ integerSetToAssociates K a = integerSetToAssociates K b ↔ ∃ ζ, ζ • a = b

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
⊢ integerSetToAssociates K a = integerSetToAssociates K b ↔ ∃ ζ, ζ • a = b
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case e'_3
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ 2 = (Subgroup.map (unitsMulComplexConjInv K) (torsion K)).index

Tactic:
· rw [map_unitsMulComplexConjInv_torsion, IsCyclic.index_powMonoidHom_range, Nat.gcd_eq_right]
    exact even_iff_two_dvd.mp (even_torsionOrder K)

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:
[

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

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

Goal state after:
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)}
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:
this

Goal state after:
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 ↔ (unitsMulComplexConjInv K).range.index = 1
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:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ mixedEmbedding.norm (mixedSpaceOfRealSpace (normAtAllPlaces x)) = mixedEmbedding.norm x
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:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ mixedSpaceOfRealSpace (normAtAllPlaces x) ∈ fundamentalCone K ↔ x ∈ fundamentalCone K
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:
[

Goal state after:
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
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)
left✝ : ↑a ∈ fundamentalCone K
x : 𝓞 K
hx₁ : x ∈ ↑↑J
hx₂ : (mixedEmbedding K) ↑x = ↑a
⊢ ↑(preimageOfMemIntegerSet (idealSetMap K J a)) ∈ ↑↑J

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
left✝ : ↑a ∈ fundamentalCone K
x : 𝓞 K
hx₁ : x ∈ ↑↑J
hx₂ : (mixedEmbedding K) ↑x = ↑a
⊢ ↑(preimageOfMemIntegerSet (idealSetMap K J a)) ∈ ↑↑J
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 : ⟨idealSetMap K J x✝¹, ⋯⟩ = ⟨idealSetMap K J x✝, ⋯⟩
⊢ x✝¹ = x✝

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
x✝¹ x✝ : ↑(idealSet K J)
h : ⟨idealSetMap K J x✝¹, ⋯⟩ = ⟨idealSetMap K J x✝, ⋯⟩
⊢ x✝¹ = x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s } * torsionOrder K =
    Nat.card { a // mixedEmbedding.norm ↑a ≤ s }

Tactic:
[

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s } * torsionOrder K =
    Nat.card { a // mixedEmbedding.norm ↑a ≤ s }
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w₁ w₂ : InfinitePlace K
e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)
e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)
g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm
h_col :
  |((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
          id).det| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
i✝ : Fin (rank K)
⊢ ∑ j, of (fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))) i✝ j = 0

Tactic:
[

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w₁ w₂ : InfinitePlace K
e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)
e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)
g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm
h_col :
  |((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
          id).det| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
i✝ : Fin (rank K)
⊢ ∑ j, of (fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))) i✝ j = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝ : ↥(Finset.Iic ⌊s⌋₊)
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a // ⟨absNorm ↑↑a.1, ⋯⟩ = ⟨i, hi⟩ } ≃ { b // ⟨intNorm ↑((idealSetEquiv K J) ↑b), ⋯⟩ = ⟨i, hi⟩ }

Tactic:
[

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝ : ↥(Finset.Iic ⌊s⌋₊)
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a // ⟨absNorm ↑↑a.1, ⋯⟩ = ⟨i, hi⟩ } ≃ { b // ⟨intNorm ↑((idealSetEquiv K J) ↑b), ⋯⟩ = ⟨i, hi⟩ }
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝ : ↥(Finset.Iic ⌊s⌋₊)
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a // mixedEmbedding.norm ↑a = ↑i } ≃ { a // intNorm ↑((idealSetEquiv K J) a) = i }

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝ : ↥(Finset.Iic ⌊s⌋₊)
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a // mixedEmbedding.norm ↑a = ↑i } ≃ { a // intNorm ↑((idealSetEquiv K J) a) = i }
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : s < 0
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s } * torsionOrder K =
    Nat.card { a // mixedEmbedding.norm ↑a ≤ s }

Tactic:
[

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : s < 0
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s } * torsionOrder K =
    Nat.card { a // mixedEmbedding.norm ↑a ≤ s }
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ expMap.source = Set.univ

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ expMap.source = Set.univ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ expMap.target = Set.univ.pi fun x ↦ Set.Ioi 0

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ expMap.target = Set.univ.pi fun x ↦ Set.Ioi 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
⊢ ∑ w, ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) x)) w = Real.log ↑|(Algebra.norm ℚ) x|

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
⊢ ∑ w, ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) x)) w = Real.log ↑|(Algebra.norm ℚ) x|
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: case inl
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
hv : v = w.comap (algebraMap K L)
h : IsUnramified K w
⊢ v.mult * Module.finrank v.Completion w.Completion = w.mult

Tactic:
h.finrank_eq_one v,

Goal state after:
case inl
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
hv : v = w.comap (algebraMap K L)
h : IsUnramified K w
⊢ v.mult * 1 = w.mult
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
w : { w // w ≠ w₀ }
⊢ realSpaceToLogSpace (↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) x))) w = logMap ((mixedEmbedding K) x) w

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
w : { w // w ≠ w₀ }
⊢ realSpaceToLogSpace (↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) x))) w = logMap ((mixedEmbedding K) x) w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case mem
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : { w // w ≠ w₀ }
⊢ ∑ x, completeFamily K (↑w) x = 0

Tactic:
[

Goal state after:
case mem
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : { w // w ≠ w₀ }
⊢ ∑ x, completeFamily K (↑w) x = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ LinearIndependent ℝ (⇑realSpaceToLogSpace ∘ fun w ↦ completeFamily K ↑w)

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ LinearIndependent ℝ (⇑realSpaceToLogSpace ∘ fun w ↦ completeFamily K ↑w)
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)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ↑(finrank ℚ K) * regOfFamily u =
    |∑ j,
          (reindex f.symm f.symm)
            (of fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))
            (f.symm w') j| *
      |(((reindex f.symm f.symm)
                (of fun i w ↦
                  if h : i = w' then ↑w.mult
                  else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))).submatrix
            (f.symm w').succAbove (f.symm w').succAbove).det|

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ↑(finrank ℚ K) * regOfFamily u =
    |∑ j,
          (reindex f.symm f.symm)
            (of fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))
            (f.symm w') j| *
      |(((reindex f.symm f.symm)
                (of fun i w ↦
                  if h : i = w' then ↑w.mult
                  else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))).submatrix
            (f.symm w').succAbove (f.symm w').succAbove).det|
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : InfinitePlace K
⊢ ↑expMap ((completeBasis K) w₀) x✝ = Real.exp 1

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : InfinitePlace K
⊢ ↑expMap ((completeBasis K) w₀) x✝ = Real.exp 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w i : InfinitePlace K
hw : ¬w = w₀
⊢ (completeBasis K) w i = ↑i.mult * Real.log (i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w, hw⟩))))

Tactic:
[

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w i : InfinitePlace K
hw : ¬w = w₀
⊢ (completeBasis K) w i = ↑i.mult * Real.log (i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w, hw⟩))))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ↑expMapBasis x = Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ↑expMapBasis x = Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i
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)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ∀ (i : Fin (rank K + 1)),
    i ≠ f.symm w' →
      ∑ j,
          (reindex f.symm f.symm)
            (of fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))
            i j =
        0

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ∀ (i : Fin (rank K + 1)),
    i ≠ f.symm w' →
      ∑ j,
          (reindex f.symm f.symm)
            (of fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))
            i j =
        0
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
h₀ : Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0
h_eq₁ :
  span {Polynomial.map (Int.castRingHom (ZMod p)) Q} =
    span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} ⊔ span {Polynomial.map (Int.castRingHom (ZMod p)) Q}
⊢ span {↑p} ⊔ span {(aeval θ) Q} = span {↑p, (aeval θ) Q}

Tactic:
by
    rw [span_insert]

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

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

Tactic:
[

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