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
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
w : InfinitePlace K
⊢ w ≠ W₀ ↔ (equivInfinitePlace K) w ≠ w₀

Tactic:
by

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

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
x✝ :
  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}
h₁ :
  x ∈
    ⇑mixedSpaceOfRealSpace ⁻¹'
      logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
h₂ : x ∈ {x | ∀ (w : InfinitePlace K), 0 ≤ x w}
h₃ : x ∈ {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≠ 0}
h₄ : x ∈ {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≤ 1}
⊢ x ∈ normAtAllPlaces '' normLeOne K

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:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
x✝ :
  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}
h₁ :
  x ∈
    ⇑mixedSpaceOfRealSpace ⁻¹'
      logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
h₂ : x ∈ {x | ∀ (w : InfinitePlace K), 0 ≤ x w}
h₃ : x ∈ {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≠ 0}
h₄ : x ∈ {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≤ 1}
⊢ x ∈ normAtAllPlaces '' normLeOne K
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⌋₊
x✝¹ : ↥(Units.torsion K)
x✝ : ↥(Ideal (𝓞 K))⁰
⊢ (↑J ∣ ↑x✝ ∧ IsPrincipal ↑x✝ ∧ absNorm ↑x✝ ≤ ⌊s⌋₊) ∧ absNorm ↑x✝ = i ↔ ↑J ∣ ↑x✝ ∧ IsPrincipal ↑x✝ ∧ absNorm ↑x✝ = i

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ normAtAllPlaces '' normLeOne K =
    ⇑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:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
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:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.univ
⊢ ↑w.mult * Real.log (Real.exp ((↑w.mult)⁻¹ * x✝¹)) = x✝¹

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x✝ : ℝ
h : x✝ ∈ Set.Ioi 0
⊢ Real.exp ((↑w.mult)⁻¹ * (↑w.mult * Real.log x✝)) = x✝

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ Set.Ioi 0 ⊆ {0}ᶜ

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : ℝ
⊢ HasDerivAt (↑(expMap_single w)) (deriv_expMap_single w x) x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances

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
x : K
⊢ (algebraMap K w.Completion) x = (algebraMap v.Completion w.Completion) ((algebraMap K v.Completion) x)

Tactic:
by

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

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
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsRamified K w
⊢ Module.finrank v.Completion w.Completion = 2

Tactic:
by

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
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsUnramified K w
hv : v.IsReal
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
x✝ : v.Completion
⊢ ↑(((algebraMap ℝ ℝ).comp (ringEquivRealOfIsReal hv).toRingHom) x✝) =
    ↑(((ringEquivRealOfIsReal ⋯).toRingHom.comp (algebraMap v.Completion w.Completion)) x✝)

Tactic:
by

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

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

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

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ HasFDerivAt (↑expMap) (fderiv_expMap x) x

Tactic:
by

Goal state after:
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₁ w₂ : InfinitePlace K
e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)
e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)
⊢ |(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))))).det|

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card (Fin (rank K)) = Fintype.card { w // w ≠ w₀ }

Tactic:
by

Goal state after:
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)
⊢ regOfFamily u = |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e i))))).det|

Tactic:
by

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
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsUnramified K w
⊢ Module.finrank v.Completion w.Completion = 1

Tactic:
by

Goal state after:
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)
x✝ : InfinitePlace K
⊢ x✝ ≠ w' ↔ f.symm x✝ ≠ f.symm w'

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝² x✝¹ : realSpace K
x✝ : { w // w ≠ w₀ }
⊢ (x✝² + x✝¹) ↑x✝ - (↑(↑x✝).mult * ∑ w', (x✝² + x✝¹) w') * (↑(finrank ℚ K))⁻¹ =
    ((fun w ↦ x✝² ↑w - (↑(↑w).mult * ∑ w', x✝² w') * (↑(finrank ℚ K))⁻¹) + fun w ↦
        x✝¹ ↑w - (↑(↑w).mult * ∑ w', x✝¹ w') * (↑(finrank ℚ K))⁻¹)
      x✝

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ regOfFamily (realFundSystem K) = 2 ^ rank K * regulator ↥K⁺

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝² : ℝ
x✝¹ : realSpace K
x✝ : { w // w ≠ w₀ }
⊢ (x✝² • x✝¹) ↑x✝ - (↑(↑x✝).mult * ∑ w', (x✝² • x✝¹) w') * (↑(finrank ℚ K))⁻¹ =
    ((RingHom.id ℝ) x✝² • fun w ↦ x✝¹ ↑w - (↑(↑w).mult * ∑ w', x✝¹ w') * (↑(finrank ℚ K))⁻¹) x✝

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ 2 ^ rank K ≠ 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ regulator K / regulator ↥K⁺ = 2 ^ rank K * (↑(indexRealUnits K))⁻¹

Tactic:
by

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
w : InfinitePlace L
inst✝ : w.LiesOver v
⊢ v.mult * Module.finrank v.Completion w.Completion = w.mult

Tactic:
by

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
w : InfinitePlace L
inst✝ : w.LiesOver v
⊢ v.inertiaDeg w = ⊥.inertiaDeg v.Completion

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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
w : InfinitePlace L
inst✝ : w.LiesOver v
⊢ v.inertiaDeg w = Module.finrank v.Completion w.Completion

Tactic:
by

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

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

Tactic:
by

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✝ ∈ (ramifiedPlacesOver L v).toFinset
⊢ x✝ ∈ ramifiedPlacesOver L v

Tactic:
by

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

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : x ∈ Submodule.span ℝ (Set.range fun w ↦ completeFamily K ↑w)
⊢ ∑ w, x w = 0

Tactic:
by

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 ∈ (placesOver L v).toFinset, v.inertiaDeg w = Module.finrank K L

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
θ : 𝓞 K
⊢ exponent θ = 1 ↔ ℤ[θ] = ⊤

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ exponent θ ↔ Codisjoint (comap (algebraMap ℤ (𝓞 K)) (conductor ℤ θ)) (span {↑p})

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
θ : 𝓞 K
⊢ exponent θ = sInf {d | 0 < d ∧ ↑d ∈ conductor ℤ θ}

Tactic:
by

Goal state after:
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 θ
⊢ span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} =
    Ideal.map (↑(mapEquiv (Int.quotientSpanNatEquivZMod p)))
      (span {Polynomial.map (Ideal.Quotient.mk (span {↑p})) (minpoly ℤ θ)})

Tactic:
by

Goal state after:
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 θ
⊢ Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p}) = span {↑p}

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h₁ : LinearIndependent ℝ fun w ↦ completeFamily K ↑w
⊢ completeFamily K w₀ ∉ Submodule.span ℝ (Set.range fun w ↦ completeFamily K ↑w)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
⊢ Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p}) = span {↑p}

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
⊢ (ZModXQuotSpanEquivQuotSpan hp)
      ((Ideal.Quotient.mk (span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}))
        (Polynomial.map (Int.castRingHom (ZMod p)) Q)) =
    (Ideal.Quotient.mk (span {↑p})) ((aeval θ) Q)

Tactic:
by

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

Goal state before:
pp: 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
⊢ E ⊔ maximalRealSubfield K = ⊤

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ LinearIndependent ℝ (completeFamily K)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 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
⊢ E = maximalRealSubfield K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : { w // w ≠ w₀ }
⊢ (completeBasis K) ↑i =
    ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i)))))

Tactic:
by

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

Goal state after:
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
⊢ (algebraMap F K).fieldRange = maximalRealSubfield K

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
x : ↥(maximalRealSubfield K)
⊢ (algebraMap F K) ((equivMaximalRealSubfield F K).symm x) = (algebraMap (↥(maximalRealSubfield K)) K) x

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : { w // w ≠ w₀ }
⊢ normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i)))) ∈ expMap.target

Tactic:
by

Goal state after:
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
⊢ (algebraMap F K).comp (CMExtension.equivMaximalRealSubfield F K).symm.toRingHom =
    (RingEquiv.refl K).toRingHom.comp (algebraMap (↥(maximalRealSubfield K)) K)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : { w // w ≠ w₀ }
⊢ ↑expMap ((completeBasis K) ↑i) =
    normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))))

Tactic:
by

Goal state after: