mathlib-initiative/mathlib-tactics huggingface dataset:
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)
hBopen : Fact (∀ (i : ι), IsOpen[inst✝⁴ i] ↑(B i))
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : (i : ι) → SMul G (R i)
inst✝¹ : ∀ (i : ι), SMulMemClass (S i) G (R i)
inst✝ : ∀ (i : ι), ContinuousSMul G (R i)
⊢ ∀ (S_1 : Set ι) (hS : cofinite ≤ 𝓟 S_1),
    Continuous[instTopologicalSpaceProd, topologicalSpace R (fun i ↦ ↑(B i)) cofinite]
      ((fun p ↦ p.1 • p.2) ∘ Prod.map id (inclusion R (fun i ↦ ↑(B i)) hS))

Tactic:
]

Goal state after:
ι : 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)
hBopen : Fact (∀ (i : ι), IsOpen[inst✝⁴ i] ↑(B i))
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : (i : ι) → SMul G (R i)
inst✝¹ : ∀ (i : ι), SMulMemClass (S i) G (R i)
inst✝ : ∀ (i : ι), ContinuousSMul G (R i)
⊢ ∀ (S_1 : Set ι) (hS : cofinite ≤ 𝓟 S_1),
    Continuous[instTopologicalSpaceProd, topologicalSpace R (fun i ↦ ↑(B i)) cofinite]
      ((fun p ↦ p.1 • p.2) ∘ Prod.map id (inclusion R (fun i ↦ ↑(B i)) hS))
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst✝¹ (f j), inst✝ j] (φ j)
⊢ ∀ (S : Set ι₁) (hS : 𝓕₁ ≤ 𝓟 S),
    Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂] (mapAlong R₁ R₂ f hf φ hφ ∘ inclusion R₁ A₁ hS)

Tactic:
]

Goal state after:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst✝¹ (f j), inst✝ j] (φ j)
⊢ ∀ (S : Set ι₁) (hS : 𝓕₁ ≤ 𝓟 S),
    Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂] (mapAlong R₁ R₂ f hf φ hφ ∘ inclusion R₁ A₁ hS)
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card (InfinitePlace K) - 1 = Fintype.card (InfinitePlace K) - 1

Tactic:
]

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

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst✝¹ (f j), inst✝ j] (φ j)
S : Set ι₁
hS : S ∈ 𝓕₁
T : Set ι₂ := f ⁻¹' S ∩ {j | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
⊢ T ∈ 𝓕₂

Tactic:
]

Goal state after:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst✝¹ (f j), inst✝ j] (φ j)
S : Set ι₁
hS : S ∈ 𝓕₁
T : Set ι₂ := f ⁻¹' S ∩ {j | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
⊢ T ∈ 𝓕₂
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

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

Tactic:
]

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

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst✝¹ (f j), inst✝ j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
T : Set ι₂ := f ⁻¹' S ∩ {j | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
hT : 𝓕₂ ≤ 𝓟 T
hf' : Tendsto f (𝓟 T) (𝓟 S)
hφ' : ∀ᶠ (j : ι₂) in 𝓟 T, MapsTo (φ j) (A₁ (f j)) (A₂ j)
key : mapAlong R₁ R₂ f hf φ hφ ∘ inclusion R₁ A₁ hS = inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ f hf' φ hφ'
⊢ Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂] (inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ f hf' φ hφ')

Tactic:
]

Goal state after:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst✝¹ (f j), inst✝ j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
T : Set ι₂ := f ⁻¹' S ∩ {j | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
hT : 𝓕₂ ≤ 𝓟 T
hf' : Tendsto f (𝓟 T) (𝓟 S)
hφ' : ∀ᶠ (j : ι₂) in 𝓟 T, MapsTo (φ j) (A₁ (f j)) (A₂ j)
key : mapAlong R₁ R₂ f hf φ hφ ∘ inclusion R₁ A₁ hS = inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ f hf' φ hφ'
⊢ Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂] (inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ f hf' φ hφ')
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Subgroup (𝓞 K)ˣ
h : (s ⊔ torsion K).FiniteIndex
⊢ s.relIndex (s ⊔ torsion K) * (s ⊔ torsion K).index ≠ 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Subgroup (𝓞 K)ˣ
h : (s ⊔ torsion K).FiniteIndex
⊢ s.relIndex (s ⊔ torsion K) * (s ⊔ torsion K).index ≠ 0
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Subgroup (𝓞 K)ˣ
h : (s ⊔ torsion K).FiniteIndex
⊢ s.relIndex (torsion K) ≠ 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Subgroup (𝓞 K)ˣ
h : (s ⊔ torsion K).FiniteIndex
⊢ s.relIndex (torsion K) ≠ 0
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)ˣ
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    (span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))).toAddSubgroup.index ≠ 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    (span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))).toAddSubgroup.index ≠ 0
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)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    (span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))).toAddSubgroup.index ≠ 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    (span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))).toAddSubgroup.index ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realMixedSpace K
this : ↑(FDerivPolarCoordRealSymm K x) = LinearMap.id.prodMap ↑(fderivPiPolarCoordSymm x.2)
⊢ ∏ i, (x.2 i).1 = ∏ w, (x.2 w).1

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Set.univ ×ˢ ((Pi.map fun x ↦ ↑polarCoord.symm) '' Set.univ.pi fun x ↦ polarCoord.target) =ᵐ[volume.prod volume]
    Set.univ ×ˢ Set.univ

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Set.univ ×ˢ ((Pi.map fun x ↦ ↑polarCoord.symm) '' Set.univ.pi fun x ↦ polarCoord.target) =ᵐ[volume.prod volume]
    Set.univ ×ˢ Set.univ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : realMixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in (polarCoordReal K).target, (∏ w, (x.2 w).1) • f (↑(polarCoordReal K).symm x) =
    ∫ (x : realMixedSpace K) in (polarCoordReal K).target,
      |(FDerivPolarCoordRealSymm K x).det| • f (↑(polarCoordReal K).symm x)

Tactic:
]

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : realMixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in (polarCoordReal K).target, (∏ w, (x.2 w).1) • f (↑(polarCoordReal K).symm x) =
    ∫ (x : realMixedSpace K) in (polarCoordReal K).target,
      |(FDerivPolarCoordRealSymm K x).det| • f (↑(polarCoordReal K).symm x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : realMixedSpace K → ℝ≥0∞
⊢ ∫⁻ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(polarCoordReal K).symm x) =
    ∫⁻ (x : realMixedSpace K) in (polarCoordReal K).target,
      ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| * f (↑(polarCoordReal K).symm x)

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : realMixedSpace K → ℝ≥0∞
⊢ ∫⁻ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(polarCoordReal K).symm x) =
    ∫⁻ (x : realMixedSpace K) in (polarCoordReal K).target,
      ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| * f (↑(polarCoordReal K).symm x)
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)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (AddSubgroup.map (↑(logEmbeddingEquiv K).toAddEquiv)
          (AddSubgroup.closure (⇑Additive.toMul.symm '' QuotientGroup.mk '' Set.range u))).index ≠
      0 ↔
    (AddSubgroup.map (↑↑(logEmbeddingEquiv K))
          (AddSubgroup.closure (⇑Additive.toMul.symm '' QuotientGroup.mk '' Set.range u))).index ≠
      0

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (AddSubgroup.map (↑(logEmbeddingEquiv K).toAddEquiv)
          (AddSubgroup.closure (⇑Additive.toMul.symm '' QuotientGroup.mk '' Set.range u))).index ≠
      0 ↔
    (AddSubgroup.map (↑↑(logEmbeddingEquiv K))
          (AddSubgroup.closure (⇑Additive.toMul.symm '' QuotientGroup.mk '' Set.range u))).index ≠
      0
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
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable (⇑(mixedSpaceToRealMixedSpace K).symm ∘ ↑(polarCoordReal K).symm)

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable (⇑(mixedSpaceToRealMixedSpace K).symm ∘ ↑(polarCoordReal K).symm)
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)) * (normAtPlace w) x ≠ 0

Tactic:
]

Goal state after:
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)) * (normAtPlace w) x ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, (x.2 w).1) • f ((fun x ↦ (mixedSpaceToRealMixedSpace K).symm (↑(polarCoordReal K).symm x)) x) =
    ∫ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, (x.2 w).1) • f ((mixedSpaceToRealMixedSpace K).symm (↑(polarCoordReal K).symm x))

Tactic:
]

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 : 𝓞 K
u : (𝓞 K)ˣ
⊢ ↑u * x = y ↔ ↑u * x = y

pp: case I
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ Function.Injective ⇑(mixedEmbedding K)

Tactic:
]

Goal state after:
case I
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ Function.Injective ⇑(mixedEmbedding K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : mixedSpace K
⊢ mixedEmbedding.norm x = mixedEmbedding.norm x

Tactic:
]

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)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite
      (↥(unitLattice K) ⧸ span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))
⊢ IsDiscrete ↑(span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i))))

Tactic:
]

Goal state after:
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)))
⊢ IsDiscrete ↑(span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i))))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) *
        f ((fun x ↦ (mixedSpaceToRealMixedSpace K).symm (↑(polarCoordReal K).symm x)) x) =
    ∫⁻ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f ((mixedSpaceToRealMixedSpace K).symm (↑(polarCoordReal K).symm x))

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable (↑(mixedEmbedding.polarCoord K).symm ∘ ⇑(homeoRealMixedSpacePolarSpace K).symm)

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable (↑(mixedEmbedding.polarCoord K).symm ∘ ⇑(homeoRealMixedSpacePolarSpace K).symm)
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)))
⊢ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i))) ⊆ ↑(unitLattice K)

Tactic:
]

Goal state after:
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)))
⊢ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i))) ⊆ ↑(unitLattice 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
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ ↑(↑w).mult *
      (Real.log ((normAtPlace ↑w) x) + Real.log ((normAtPlace ↑w) y) -
        (Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹ +
          Real.log (mixedEmbedding.norm y) * (↑(finrank ℚ K))⁻¹)) =
    ↑(↑w).mult * (Real.log ((normAtPlace ↑w) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) +
      ↑(↑w).mult * (Real.log ((normAtPlace ↑w) y) - Real.log (mixedEmbedding.norm y) * (↑(finrank ℚ K))⁻¹)

pp: case hx
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ (normAtPlace ↑w) x ≠ 0

pp: case hy
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ (normAtPlace ↑w) y ≠ 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ ↑(↑w).mult *
      (Real.log ((normAtPlace ↑w) x) + Real.log ((normAtPlace ↑w) y) -
        (Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹ +
          Real.log (mixedEmbedding.norm y) * (↑(finrank ℚ K))⁻¹)) =
    ↑(↑w).mult * (Real.log ((normAtPlace ↑w) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) +
      ↑(↑w).mult * (Real.log ((normAtPlace ↑w) y) - Real.log (mixedEmbedding.norm y) * (↑(finrank ℚ K))⁻¹)

case hx
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ (normAtPlace ↑w) x ≠ 0

case hy
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ (normAtPlace ↑w) y ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x = 1
w : { w // w ≠ w₀ }
⊢ ↑(↑w).mult * Real.log ((normAtPlace ↑w) x) = ↑(↑w).mult * Real.log ((normAtPlace ↑w) x)

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x = 1
w : { w // w ≠ w₀ }
⊢ logMap x w = ↑(↑w).mult * Real.log ((normAtPlace ↑w) x)

Tactic:
rw [logMap_apply, hx, Real.log_one, zero_mul, sub_zero]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ 1 ≠ 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ 1 ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ (logEmbedding K) (Additive.ofMul u) + logMap x = (logEmbedding K) (Additive.ofMul u) + logMap x

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ((homeoRealMixedSpacePolarSpace K) x).1 ↑w) •
        f (↑(polarSpaceCoord K).symm ((homeoRealMixedSpacePolarSpace K) x)) ∂volume =
    ∫ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, (x.2 w).1) • f (↑(mixedEmbedding.polarCoord K).symm x)

Tactic:
]

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ((homeoRealMixedSpacePolarSpace K) x).1 ↑w) •
        f (↑(polarSpaceCoord K).symm ((homeoRealMixedSpacePolarSpace K) x)) ∂volume =
    ∫ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, (x.2 w).1) • f (↑(mixedEmbedding.polarCoord K).symm x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (a : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ENNReal.ofReal (((homeoRealMixedSpacePolarSpace K) a).1 ↑w)) *
        f (↑(polarSpaceCoord K).symm ((homeoRealMixedSpacePolarSpace K) a)) ∂volume =
    ∫⁻ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(mixedEmbedding.polarCoord K).symm x)

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (a : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ENNReal.ofReal (((homeoRealMixedSpacePolarSpace K) a).1 ↑w)) *
        f (↑(polarSpaceCoord K).symm ((homeoRealMixedSpacePolarSpace K) a)) ∂volume =
    ∫⁻ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(mixedEmbedding.polarCoord K).symm x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

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

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
c : ℝ
hc : c ≠ 0
⊢ |c| ^ finrank ℚ K ≠ 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
c : ℝ
hc : c ≠ 0
⊢ |c| ^ finrank ℚ K ≠ 0