mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ nrRealPlaces ↥K⁺ + nrComplexPlaces ↥K⁺ = nrRealPlaces K + nrComplexPlaces K

Tactic:
IsTotallyComplex.nrRealPlaces_eq_zero K,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ nrRealPlaces ↥K⁺ + nrComplexPlaces ↥K⁺ = 0 + nrComplexPlaces 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 : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ ζ • x ∈ fundamentalCone K

Tactic:
constructor

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
⊢ ζ • x ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

case right
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ ζ • x ∉ {x | mixedEmbedding.norm x = 0}
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
⊢ complexConj K ^ 2 = 1

Tactic:
ext

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
a✝ : K
⊢ (complexConj K ^ 2) a✝ = 1 a✝
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 ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
⊢ u ∈ torsion K

Tactic:
← logEmbedding_eq_zero_iff

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
⊢ (logEmbedding K) (Additive.ofMul u) = 0
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)
⊢ (ENNReal.ofReal (2 * π) ^ Fintype.card { w // w.IsComplex } *
      ∫⁻ (a : InfinitePlace K → ℝ) in
        ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
        (fun x ↦ ∏ x, ENNReal.ofReal (a ↑x)) a ∂Measure.pi fun x ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w) ∂Measure.pi fun x ↦ volume

Tactic:
volume_eq_two_pi_pow_mul_integral_aux hA

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)
⊢ (ENNReal.ofReal (2 * π) ^ Fintype.card { w // w.IsComplex } *
      ∫⁻ (a : InfinitePlace K → ℝ) in
        ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
        (fun x ↦ ∏ x, ENNReal.ofReal (a ↑x)) a ∂Measure.pi fun x ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in
        ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0,
        ∏ w, ENNReal.ofReal (x ↑w) ∂Measure.pi fun x ↦ volume
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case refine_2
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|
h :
  |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (Fin.succAbove 0)).det| =
    |(↑↑0 - ↑↑(f.symm w₂)).negOnePow •
        ((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id
            (f.symm w₂).succAbove).det|
⊢ |((reindex e₁ e₁) (of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i)))))).det| =
    |((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
          id).det|

Tactic:
← det_reindex_self g

Goal state after:
case refine_2
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|
h :
  |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (Fin.succAbove 0)).det| =
    |(↑↑0 - ↑↑(f.symm w₂)).negOnePow •
        ((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id
            (f.symm w₂).succAbove).det|
⊢ |((reindex e₁ e₁) (of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i)))))).det| =
    |((reindex g g)
          ((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
            id)).det|
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) ↑↑u = ↑↑u ↔ ∃ v, ↑((algebraMap (𝓞 ↥K⁺) (𝓞 K)) ↑v) = ↑↑u

Tactic:
Units.complexConj_eq_self_iff,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
⊢ (∃ v, (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u) ↔ ∃ v, ↑((algebraMap (𝓞 ↥K⁺) (𝓞 K)) ↑v) = ↑↑u
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:
ext

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
x✝ : (𝓞 K)ˣ
⊢ x✝ ∈ (unitsMulComplexConjInv K).ker ↔ x✝ ∈ realUnits K
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case e'_2
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|
h :
  |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (Fin.succAbove 0)).det| =
    |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id
          (f.symm w₂).succAbove).det|
⊢ (reindex e₁ e₁) (of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i))))) =
    (of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (Fin.succAbove 0)

Tactic:
ext

Goal state after:
case e'_2
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|
h :
  |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (Fin.succAbove 0)).det| =
    |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id
          (f.symm w₂).succAbove).det|
i✝ j✝ : Fin (rank K)
⊢ (reindex e₁ e₁) (of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i))))) i✝ j✝ =
    (of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (Fin.succAbove 0) i✝ j✝
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:
refine (Subgroup.eq_bot_iff_forall _).mpr fun ζ hζ ↦ ?_
  rwa [MulAction.mem_stabilizer_iff, Subtype.ext_iff, integerSetTorsionSMul_smul_coe,
    unitSMul_smul, ← mixedEmbedding_preimageOfMemIntegerSet, ← map_mul,
    (mixedEmbedding_injective K).eq_iff, ← map_mul, ← RingOfIntegers.ext_iff, mul_eq_right₀,
    Units.val_eq_one, OneMemClass.coe_eq_one] at hζ
  exact nonZeroDivisors.coe_ne_zero _

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
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
w : { w // w.IsReal }
⊢ {x | x ↑w ≠ 0}ᶜ = {x | x ↑w = 0}

Tactic:
ext

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
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
w : { w // w.IsReal }
x✝ : realSpace K
⊢ x✝ ∈ {x | x ↑w ≠ 0}ᶜ ↔ x✝ ∈ {x | x ↑w = 0}
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case e'_3.e'_4
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|
h :
  |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (Fin.succAbove 0)).det| =
    |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id
          (f.symm w₂).succAbove).det|
⊢ (reindex g g)
      ((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm)) id) =
    (of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (f.symm w₂).succAbove

Tactic:
ext

Goal state after:
case e'_3.e'_4
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|
h :
  |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (Fin.succAbove 0)).det| =
    |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id
          (f.symm w₂).succAbove).det|
i✝ j✝ : Fin (rank K)
⊢ (reindex g g)
      ((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm)) id)
      i✝ j✝ =
    (of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (f.symm w₂).succAbove i✝ j✝
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case refine_1
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
h_eq : indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2
h : indexRealUnits K = 2
⊢ (unitsMulComplexConjInv K).range.index = 1

pp: case refine_2
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
h_eq : indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2
h : (unitsMulComplexConjInv K).range.index = 1
⊢ indexRealUnits K = 2

Tactic:
· rwa [h, Nat.mul_eq_left two_ne_zero] at h_eq

Goal state after:
case refine_2
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
h_eq : indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2
h : (unitsMulComplexConjInv K).range.index = 1
⊢ indexRealUnits K = 2
Module: Mathlib.NumberTheory.NumberField.CMField

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

Tactic:
obtain ⟨ζ, hζ⟩ := exists_zpow_surjective (torsion K)

Goal state after:
case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
h : (unitsMulComplexConjInv K).range.index = 1
ζ : ↥(torsion K)
hζ : Function.Surjective fun x ↦ ζ ^ x
⊢ ∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case e_a
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (torsion ↥K⁺) ≤ torsion K
⊢ Set.range (realFundSystem K) = ⇑(Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) '' Set.range (fundSystem ↥K⁺)

Tactic:
ext

Goal state after:
case e_a
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (torsion ↥K⁺) ≤ torsion K
x✝ : (𝓞 K)ˣ
⊢ x✝ ∈ Set.range (realFundSystem K) ↔ x✝ ∈ ⇑(Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) '' Set.range (fundSystem ↥K⁺)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : realSpace K
⊢ ↑expMap (c • x) = ↑expMap x ^ c

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : realSpace K
x✝ : InfinitePlace K
⊢ ↑expMap (c • x) x✝ = (↑expMap x ^ c) x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : realSpace K
⊢ ↑expMap (x + y) = ↑expMap x * ↑expMap y

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : realSpace K
x✝ : InfinitePlace K
⊢ ↑expMap (x + y) x✝ = (↑expMap x * ↑expMap y) x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
f : ι → realSpace K
⊢ ↑expMap (∑ i ∈ s, f i) = ∏ i ∈ s, ↑expMap (f i)

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
f : ι → realSpace K
x✝ : InfinitePlace K
⊢ ↑expMap (∑ i ∈ s, f i) x✝ = (∏ i ∈ s, ↑expMap (f i)) x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : mixedEmbedding.norm (mixedSpaceOfRealSpace (↑expMap x)) = 1
⊢ logMap (mixedSpaceOfRealSpace (↑expMap x)) = fun w ↦ x ↑w

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : mixedEmbedding.norm (mixedSpaceOfRealSpace (↑expMap x)) = 1
x✝ : { w // w ≠ w₀ }
⊢ logMap (mixedSpaceOfRealSpace (↑expMap x)) x✝ = x ↑x✝
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
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsRamified K w
H : w.IsComplex ∧ v.IsReal
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
⊢ (algebraMap ℝ ℂ).comp (ringEquivRealOfIsReal ⋯).toRingHom =
    (ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion)

Tactic:
ext

Goal state after:
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
h : IsRamified K w
H : w.IsComplex ∧ v.IsReal
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
x✝ : v.Completion
⊢ ((algebraMap ℝ ℂ).comp (ringEquivRealOfIsReal ⋯).toRingHom) x✝ =
    ((ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion)) x✝
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
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsUnramified K w
hv : v.IsComplex
hl : w.embedding.comp (algebraMap K L) = v.embedding
this✝ : ComplexEmbedding.LiesOver w.embedding v.embedding
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
⊢ (algebraMap ℂ ℂ).comp (ringEquivComplexOfIsComplex hv).toRingHom =
    (ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion)

Tactic:
ext

Goal state after:
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
h : IsUnramified K w
hv : v.IsComplex
hl : w.embedding.comp (algebraMap K L) = v.embedding
this✝ : ComplexEmbedding.LiesOver w.embedding v.embedding
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
x✝ : v.Completion
⊢ ((algebraMap ℂ ℂ).comp (ringEquivComplexOfIsComplex hv).toRingHom) x✝ =
    ((ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion)) x✝
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
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsUnramified K w
hv : v.IsComplex
hr : (conjugate w.embedding).comp (algebraMap K L) = v.embedding
this✝ : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
this : ComplexEmbedding.LiesOver (conjugate (extensionEmbedding w)) (extensionEmbedding v)
⊢ (algebraMap ℂ ℂ).comp (ringEquivComplexOfIsComplex hv).toRingHom =
    ((ringEquivComplexOfIsComplex ⋯).trans starRingAut).toRingHom.comp (algebraMap v.Completion w.Completion)

Tactic:
ext

Goal state after:
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
h : IsUnramified K w
hv : v.IsComplex
hr : (conjugate w.embedding).comp (algebraMap K L) = v.embedding
this✝ : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
this : ComplexEmbedding.LiesOver (conjugate (extensionEmbedding w)) (extensionEmbedding v)
x✝ : v.Completion
⊢ ((algebraMap ℂ ℂ).comp (ringEquivComplexOfIsComplex hv).toRingHom) x✝ =
    (((ringEquivComplexOfIsComplex ⋯).trans starRingAut).toRingHom.comp (algebraMap v.Completion w.Completion)) x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ realSpaceToLogSpace (completeFamily K w₀) = 0

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ realSpaceToLogSpace (completeFamily K w₀) x✝ = 0 x✝
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
w : InfinitePlace L
inst✝ : w.LiesOver v
⊢ (algebraMap v.Completion w.Completion).comp (RingEquiv.quotientBot v.Completion).toRingHom =
    (RingEquiv.quotientBot w.Completion).toRingHom.comp (algebraMap (v.Completion ⧸ ⊥) (w.Completion ⧸ ⊥))

Tactic:
ext

Goal state after:
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
x✝ : v.Completion
⊢ ((((algebraMap v.Completion w.Completion).comp (RingEquiv.quotientBot v.Completion).toRingHom).comp
          (Ideal.Quotient.mk ⊥))
        x✝).toCompletion =
    ((((RingEquiv.quotientBot w.Completion).toRingHom.comp (algebraMap (v.Completion ⧸ ⊥) (w.Completion ⧸ ⊥))).comp
          (Ideal.Quotient.mk ⊥))
        x✝).toCompletion
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : { w // w ≠ w₀ }
⊢ realSpaceToLogSpace (completeFamily K ↑i) = ↑((basisUnitLattice K) (equivFinRank.symm i))

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i x✝ : { w // w ≠ w₀ }
⊢ realSpaceToLogSpace (completeFamily K ↑i) x✝ = ↑((basisUnitLattice K) (equivFinRank.symm i)) x✝
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
this : IsTotallyReal ↥(algebraMap F K).fieldRange
⊢ (algebraMap F K).comp (algebraMap F K).rangeRestrictFieldEquiv.symm.toRingHom =
    (RingEquiv.refl K).toRingHom.comp (algebraMap (↥(algebraMap F K).fieldRange) K)

Tactic:
ext

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
this : IsTotallyReal ↥(algebraMap F K).fieldRange
x✝ : ↥(algebraMap F K).fieldRange
⊢ ((algebraMap F K).comp (algebraMap F K).rangeRestrictFieldEquiv.symm.toRingHom) x✝ =
    ((RingEquiv.refl K).toRingHom.comp (algebraMap (↥(algebraMap F K).fieldRange) K)) x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

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

Tactic:
ext

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