mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case e'_5.inl
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
t : ℝ
ht : 0 < t
this :
  HasSum
    (fun m ↦ (PowerSeries.coeff m) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ m)
    (f (↑ofComplex (I * ↑t)))
⊢ (if 2 * ↑0 / h Γ = 0 then 0 else (PowerSeries.coeff 0) (qExpansion (h Γ) ⇑f) * ↑(rexp (-π * (2 * ↑0 / h Γ) * t))) =
    if 0 = 0 then 0
    else (PowerSeries.coeff 0) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ 0

Tactic:
simp

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

Goal state before:
pp: case fst
K : Type u_1
inst✝ : Field K
x : K
v : { w // w.IsReal }
⊢ ((mixedEmbedding K) x).1 v = ((ringEquiv_mixedSpace K) ((algebraMap K K∞) x)).1 v

Tactic:
simp

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

Goal state before:
pp: case snd
K : Type u_1
inst✝ : Field K
x : K
v : { w // w.IsComplex }
⊢ ((mixedEmbedding K) x).2 v = ((ringEquiv_mixedSpace K) ((algebraMap K K∞) x)).2 v

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
⊢ { toCompletion := ↑(WithAbs.toAbs (↑v) 0) }.toCompletion = toCompletion 0

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
⊢ { toCompletion := ↑(WithAbs.toAbs (↑v) 1) }.toCompletion = toCompletion 1

Tactic:
simp

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

Goal state before:
pp: case ih
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsReal
a : WithAbs ↑v
⊢ ↑((extensionEmbeddingOfIsReal hv) { toCompletion := ↑a }) = (extensionEmbedding v) { toCompletion := ↑a }

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A✝ : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i : ι), OneMemClass (S i) (G i)
i : ι
x : G i
⊢ {i}ᶜ ∈ cofinite

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i : ι), OneMemClass (S i) (G i)
i : ι
x✝¹ : G i
x✝ : ι
⊢ (DFunLike.coe ∘ mulSingle A i) x✝¹ x✝ = Pi.mulSingle i x✝¹ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i : ι), OneMemClass (S i) (G i)
i i✝ : ι
⊢ (mulSingle A i 1) i✝ = 1 i✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: case inl
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝⁴ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
⊢ (single A i (x i * r)) i = (x * single A i r) i

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: case inl
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝⁴ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
⊢ (single A i (r * x i)) i = (single A i r * x) i

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.Units

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst✝¹ : (i : ι) → SetLike (S i) (R i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : (i : ι) → (R i)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ (Submonoid.ofClass (B i)).units
i✝ : ι
⊢ (⟨fun i ↦ ↑(x i), ⋯⟩ * ⟨fun i ↦ ↑(x i)⁻¹, ⋯⟩) i✝ = 1 i✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.Units

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst✝¹ : (i : ι) → SetLike (S i) (R i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : (i : ι) → (R i)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ (Submonoid.ofClass (B i)).units
i✝ : ι
⊢ (⟨fun i ↦ ↑(x i)⁻¹, ⋯⟩ * ⟨fun i ↦ ↑(x i), ⋯⟩) i✝ = 1 i✝

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case inl
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ emultiplicity ↑p ↑(x ^ n - y ^ n) = emultiplicity ↑p ↑(x - y) + emultiplicity p n

Tactic:
Int.ofNat_sub (Nat.pow_le_pow_left hyx n)

Goal state after:
case inl
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ emultiplicity (↑p) (↑(x ^ n) - ↑(y ^ n)) = emultiplicity ↑p ↑(x - y) + emultiplicity p n
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this✝ : {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ Support R k
hk : (valuation K v) k * v.intValuation d = v.intValuation n
this : 1 ≤ v.intValuation d
⊢ 0 < 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this✝ : {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ Support R k
hk : (valuation K v) k * v.intValuation d = v.intValuation n
this : 1 ≤ v.intValuation d
⊢ 0 ≤ (valuation K v) k

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
S : Set ι
hS : cofinite ≤ 𝓟 S
x✝ : Πʳ (i : ι), [R i, A i]_[𝓟 S]
a✝ : ι
⊢ ↑x✝ a✝ ∈ A a✝ ↔ True → ↑x✝ a✝ ∈ A a✝

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
this : ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
⊢ 2 ^ (1 + 1) = 4

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
⊢ 2 ≠ 1

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ (1 - 1) % 4 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 ↑d + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + (emultiplicity 2 ↑2 + emultiplicity 2 ↑d)

pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ ¬2 ∣ x ^ 2

Tactic:
· suffices emultiplicity (2 : ℤ) ↑(2 : ℕ) = 1 by rw [this, add_comm 1, ← add_assoc]
    norm_cast
    rw [FiniteMultiplicity.emultiplicity_self]
    rw [Nat.finiteMultiplicity_iff]
    decide

Goal state after:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ ¬2 ∣ x ^ 2
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
inst✝² : (i : ι) → Inv (R i)
inst✝¹ : ∀ (i : ι), InvMemClass (S i) (R i)
inst✝ : ∀ (i : ι), ContinuousInv (R i)
⊢ Continuous[topologicalSpace R (fun i ↦ ↑(B i)) 𝓕, topologicalSpace R (fun i ↦ ↑(B i)) 𝓕] fun a ↦ a⁻¹

Tactic:
rw [continuous_dom]
    intro T hT
    have : ContinuousInv (Πʳ i, [R i, B i]_[𝓟 T]) :=
      isEmbedding_coe_of_principal.continuousInv fun _ ↦ rfl
    exact (continuous_inclusion hT).comp continuous_inv

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ x + (y + 1) ≠ 0

Tactic:
simp

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)ˣ
hu : IsMaxRank u
x✝ : logSpace K
⊢ x✝ ∈ Set.range ⇑(basisOfIsMaxRank hu) ↔ x✝ ∈ ⇑(logEmbedding K) '' ⇑Additive.toMul ⁻¹' Set.range u

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h✝ : x ≠ 0
w : InfinitePlace K
h : (normAtPlace w) x ≠ 0
⊢ (normAtPlace w) ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) ≠ 0

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ logMap 0 x✝ = 0 x✝

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ logMap 1 x✝ = 0 x✝

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x✝ : { w // w ≠ w₀ }
⊢ logMap ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) x✝ = (logEmbedding K) (Additive.ofMul u) x✝

Tactic:
simp

Goal state after:
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
x : mixedSpace K
w : InfinitePlace K
⊢ w.IsComplex → 0 ≤ normAtComplexPlaces x w

Tactic:
hw

Goal state after:
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
x : mixedSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ 0 ≤ normAtComplexPlaces x 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)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite
      (↥(unitLattice K) ⧸ span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))
h₂ : DiscreteTopology ↥(span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i))))
⊢ finrank ℤ ↥(span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i)))) = Fintype.card (Fin (rank K)) ↔
    finrank ℤ
        ↥(span ℤ
            (Set.range fun x ↦
              (unitLattice K).subtype ((⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u) x))) =
      rank K

Tactic:
simp

Goal state after:
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₁ : normAtComplexPlaces (mixedSpaceOfRealSpace x) ∈ normAtComplexPlaces '' A
hx₂ : x ∈ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
w : InfinitePlace K
⊢ w.IsComplex → 0 ≤ x w

Tactic:
hw

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
w : InfinitePlace K
hw : w.IsComplex
⊢ 0 ≤ x w
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
a✝ : K
⊢ (complexConj K ^ 2) a✝ = 1 a✝

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
⊢ (mixedEmbedding K) ↑↑(preimageOfMemIntegerSet a) = ↑a

Tactic:
rw [preimageOfMemIntegerSet, (mem_integerSet.mp a.prop).2.choose_spec]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
a : 𝓞 K
hx : (mixedEmbedding K) ↑a ∈ integerSet K
⊢ (mixedEmbedding K) ↑(↑ζ * a) = ζ • (mixedEmbedding K) ↑a

Tactic:
simp

Goal state after:
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✝ : Algebra.IsIntegral ℚ K
y : 𝓞 ↥K⁺
⊢ (ringOfIntegersComplexConj K) ((algebraMap (𝓞 ↥K⁺) (𝓞 K)) y) = (algebraMap (𝓞 ↥K⁺) (𝓞 K)) y

Tactic:
simp

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
ζ : ↥(torsion K)
⊢ (fun x ↦ (algebraMap (𝓞 K) K) ↑x) ((unitsComplexConj K) ↑ζ) = (fun x ↦ (algebraMap (𝓞 K) K) ↑x) ↑ζ⁻¹

Tactic:
simp

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
u : (𝓞 K)ˣ
x✝ : InfinitePlace K
⊢ x✝ ((algebraMap (𝓞 K) K) ↑(u * ((unitsComplexConj K) u)⁻¹)) = 1

Tactic:
simp

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
⊢ ⟨1 * ((unitsComplexConj K) 1)⁻¹, ⋯⟩ = 1

Tactic:
simp

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
ζ : ↥(torsion K)
⊢ ((unitsMulComplexConjInv K).domRestrict (torsion K)) ζ = (powMonoidHom 2) ζ

Tactic:
simp

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✝ : realSpace K
⊢ x✝ ∈ {x | x ↑w ≠ 0}ᶜ ↔ x✝ ∈ {x | x ↑w = 0}

Tactic:
simp

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))⁰
a : ↑(idealSet K J)
left✝ : ↑a ∈ fundamentalCone K
x : 𝓞 K
hx₁ : x ∈ ↑↑J
hx₂ : (mixedEmbedding K) ↑x = ↑a
⊢ x ∈ ↑↑J

Tactic:
exact hx₁

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
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
⊢ 2 ^ (Fintype.card (InfinitePlace ↥K⁺) - 1) = 2 ^ Finset.univ.card

Tactic:
simp

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

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)
x✝ : v.Completion
⊢ ((algebraMap ℝ ℂ).comp (ringEquivRealOfIsReal ⋯).toRingHom) x✝ =
    ((ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion)) x✝

Tactic:
simp

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

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)
x✝ : v.Completion
⊢ ((algebraMap ℂ ℂ).comp (ringEquivComplexOfIsComplex hv).toRingHom) x✝ =
    ((ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion)) x✝

Tactic:
simp

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

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

Tactic:
completeFamily,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ (if hi : w₀ = w₀ then fun w ↦ ↑w.mult
        else
          ↑expMap.symm
            (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w₀, hi⟩))))))
        ↑x✝ -
      (↑(↑x✝).mult *
          ∑ w',
            (if hi : w₀ = w₀ then fun w ↦ ↑w.mult
              else
                ↑expMap.symm
                  (normAtAllPlaces
                    ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w₀, hi⟩))))))
              w') *
        (↑(finrank ℚ K))⁻¹ =
    0 x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

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

Tactic:
completeFamily,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i x✝ : { w // w ≠ w₀ }
⊢ realSpaceToLogSpace
      (if hi : ↑i = w₀ then fun w ↦ ↑w.mult
      else
        ↑expMap.symm
          (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨↑i, hi⟩))))))
      x✝ =
    logMap ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i)))) x✝
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:
completeFamily,

Goal state after:
case mem
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : { w // w ≠ w₀ }
⊢ ∑ x,
      (if hi : ↑w = w₀ then fun w ↦ ↑w.mult
        else
          ↑expMap.symm
            (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨↑w, hi⟩))))))
        x =
    0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case zero
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ∑ w, 0 w = 0

Tactic:
simp

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

Goal state before:
pp: case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ ↑((basisUnitLattice K) (equivFinRank.symm x✝)) =
    ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).reindex equivFinRank) x✝

Tactic:
simp

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
h : completeFamily K w₀ ∈ Submodule.span ℝ (Set.range fun w ↦ completeFamily K ↑w)
this : ∑ w, completeFamily K w₀ w = 0
⊢ False

Tactic:
completeFamily,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h₁ : LinearIndependent ℝ fun w ↦ completeFamily K ↑w
h : completeFamily K w₀ ∈ Submodule.span ℝ (Set.range fun w ↦ completeFamily K ↑w)
this :
  ∑ w,
      (if hi : w₀ = w₀ then fun w ↦ ↑w.mult
        else
          ↑expMap.symm
            (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w₀, hi⟩))))))
        w =
    0
⊢ False
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

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

Tactic:
completeFamily,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (if hi : w₀ = w₀ then fun w ↦ ↑w.mult
    else
      ↑expMap.symm
        (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w₀, hi⟩)))))) =
    fun w ↦ ↑w.mult
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

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

Tactic:
completeFamily,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : { w // w ≠ w₀ }
⊢ (if hi : ↑i = w₀ then fun w ↦ ↑w.mult
    else
      ↑expMap.symm
        (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨↑i, hi⟩)))))) =
    ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i)))))