awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ :
  Membership.mem (γ := Set (realSpace K))
    (⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}) (normAtAllPlaces a)
w : { w : InfinitePlace K // w.IsReal }
⊢ LT.lt (α := ℝ) 0 (((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces a)).1 w)

Tactic:
refine lt_of_le_of_ne' (normAtPlace_nonneg _ _) (Set.mem_iInter.mp ha₂ w)

Premises used: Set.mem_iInter, lt_of_le_of_ne', NumberField.mixedEmbedding.normAtPlace_nonneg, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ :
  Membership.mem (γ := Set (realSpace K))
    (⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}) (normAtAllPlaces a)
h h₁ : normAtAllPlaces a = normAtAllPlaces a
⊢ normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces a)) =
    normAtAllPlaces a

Tactic:
rw [normAtComplexPlaces_normAtAllPlaces]

Premises used: NumberField.mixedEmbedding.normAtComplexPlaces_normAtAllPlaces
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha₁ : a ∈ A
ha₂ :
  Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | ∀ (w : { w : InfinitePlace K // w.IsReal }), 0 < x.1 w} a
⊢ normAtComplexPlaces a ∈
    normAtAllPlaces '' A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}

Tactic:
⟨⟨a, ha₁, funext fun w ↦ ?_⟩, Set.mem_iInter.mpr fun w ↦ ?_⟩

Premises used: Iff.mpr, Set.Mem, setOf, Set.inter, Set.mem_iInter, funext, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha₁ : a ∈ A
ha₂ :
  Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | ∀ (w : { w : InfinitePlace K // w.IsReal }), 0 < x.1 w} a
h : ∀ (w : InfinitePlace K), normAtAllPlaces a w = normAtComplexPlaces a w
h₁ :
  ∀ (w : { w : InfinitePlace K // w.IsReal }),
    Membership.mem (γ := Set (realSpace K)) {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} (normAtComplexPlaces a)
⊢ normAtComplexPlaces a ∈
    normAtAllPlaces '' A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}

Tactic:
refine ⟨⟨a, ha₁, funext fun w ↦ ?_⟩, Set.mem_iInter.mpr fun w ↦ ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha₁ : a ∈ A
ha₂ :
  Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | ∀ (w : { w : InfinitePlace K // w.IsReal }), 0 < x.1 w} a
w : InfinitePlace K
h : ∀ (hw : w.IsReal), normAtAllPlaces a w = normAtComplexPlaces a w
h₁ : ∀ (hw : w.IsComplex), normAtAllPlaces a w = normAtComplexPlaces a w
⊢ normAtAllPlaces a w = normAtComplexPlaces a w

Tactic:
obtain hw | hw := isReal_or_isComplex w

Premises used: NumberField.InfinitePlace.isReal_or_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha₁ : a ∈ A
ha₂ :
  Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | ∀ (w : { w : InfinitePlace K // w.IsReal }), 0 < x.1 w} a
w : InfinitePlace K
hw : w.IsReal
⊢ normAtAllPlaces a w = normAtComplexPlaces a w

Tactic:
simpa [normAtComplexPlaces_apply_isReal ⟨w, hw⟩, normAtPlace_apply_of_isReal hw]
          using (ha₂ ⟨w, hw⟩).le

Premises used: NumberField.mixedEmbedding.normAtPlace_apply_of_isReal, LT.lt.le, Subtype.mk, NumberField.mixedEmbedding.normAtComplexPlaces_apply_isReal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha₁ : a ∈ A
ha₂ :
  Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | ∀ (w : { w : InfinitePlace K // w.IsReal }), 0 < x.1 w} a
w : InfinitePlace K
hw : w.IsComplex
h : (normAtPlace w : (a : mixedSpace K) → ℝ) a = normAtComplexPlaces a w
h₁ : ‖a.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖ = normAtComplexPlaces a w
h₂ h₃ :
  ‖a.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖ =
    ‖a.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖
⊢ normAtAllPlaces a w = normAtComplexPlaces a w

Tactic:
rw [normAtAllPlaces_apply, normAtPlace_apply_of_isComplex hw,
          normAtComplexPlaces_apply_isComplex ⟨w, hw⟩]

Premises used: NumberField.mixedEmbedding.normAtAllPlaces_apply, Subtype.mk, NumberField.mixedEmbedding.normAtPlace_apply_of_isComplex, NumberField.mixedEmbedding.normAtComplexPlaces_apply_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha₁ : a ∈ A
ha₂ :
  Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | ∀ (w : { w : InfinitePlace K // w.IsReal }), 0 < x.1 w} a
w : { w : InfinitePlace K // w.IsReal }
⊢ Membership.mem (γ := Set (realSpace K)) {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} (normAtComplexPlaces a)

Tactic:
simpa [Set.mem_setOf_eq, normAtComplexPlaces_apply_isReal] using (ha₂ w).ne'

Premises used: Set.mem_setOf_eq, LT.lt.ne', NumberField.mixedEmbedding.normAtComplexPlaces_apply_isReal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
x : mixedSpace K
rw :
  x ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A ↔
    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A
⊢ x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A

Tactic:
rw [← hA]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
x : mixedSpace K
simp_rw :
  normAtAllPlaces x ∈ normAtAllPlaces '' A ↔
    normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ normAtAllPlaces '' A
simp_rw₁ :
  (∃ x_1 ∈ A, normAtAllPlaces x_1 = normAtAllPlaces x) ↔
    ∃ x_1 ∈ A, normAtAllPlaces x_1 = normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2)
⊢ x ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A ↔
    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A

Tactic:
simp_rw [Set.mem_preimage, Set.mem_image, normAtAllPlaces_norm_at_real_places]

Premises used: Set.mem_image, NumberField.mixedEmbedding.normAtAllPlaces_norm_at_real_places, Set.mem_preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
⊢ ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A

Tactic:
have hA₁ (x : mixedSpace K) : x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A := by
    rw [← hA]
    simp_rw [Set.mem_preimage, Set.mem_image, normAtAllPlaces_norm_at_real_places]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
⊢ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A

Tactic:
subset_antisymm (fun x ⟨a, ha₁, ha₂⟩ ↦ ⟨?_, fun w ↦ ?_⟩) (Set.subset_preimage_image _ _)

Premises used: subset_antisymm, Set.subset_preimage_image
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
refine_1 :
  ∀ x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A,
    ∀ (a : mixedSpace K) (ha₁ : a ∈ plusPart A) (ha₂ : normAtComplexPlaces a = normAtComplexPlaces x), x ∈ A
refine_2 :
  ∀ x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A,
    ∀ (a : mixedSpace K) (ha₁ : a ∈ plusPart A) (ha₂ : normAtComplexPlaces a = normAtComplexPlaces x)
      (w : { w : InfinitePlace K // w.IsReal }), 0 < x.1 w
⊢ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A

Tactic:
refine subset_antisymm (fun x ⟨a, ha₁, ha₂⟩ ↦ ⟨?_, fun w ↦ ?_⟩) (Set.subset_preimage_image _ _)

Premises used: subset_antisymm, Set.subset_preimage_image
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
refine_1 : normAtAllPlaces a ∈ normAtAllPlaces '' A
⊢ x ∈ A

Tactic:
rw [← hA, Set.mem_preimage, ← normAtAllPlaces_eq_of_normAtComplexPlaces_eq ha₂]

Premises used: NumberField.mixedEmbedding.normAtAllPlaces_eq_of_normAtComplexPlaces_eq, Set.mem_preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
⊢ normAtAllPlaces a ∈ normAtAllPlaces '' A

Tactic:
Set.mem_image_of_mem normAtAllPlaces (Set.inter_subset_left ha₁)

Premises used: Set.inter_subset_left, NumberField.mixedEmbedding.normAtAllPlaces, Set.mem_image_of_mem
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
⊢ normAtAllPlaces a ∈ normAtAllPlaces '' A

Tactic:
exact Set.mem_image_of_mem normAtAllPlaces (Set.inter_subset_left ha₁)

Premises used: Set.inter_subset_left, NumberField.mixedEmbedding.normAtAllPlaces, Set.mem_image_of_mem
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
w : { w : InfinitePlace K // w.IsReal }
⊢ normAtComplexPlaces a (↑w : InfinitePlace K) = normAtComplexPlaces x (↑w : InfinitePlace K)

Tactic:
have := funext_iff.mp ha₂ w
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
w : { w : InfinitePlace K // w.IsReal }
this : normAtComplexPlaces a (↑w : InfinitePlace K) = normAtComplexPlaces x (↑w : InfinitePlace K)
⊢ a.1 w = x.1 w

Tactic:
rw [normAtComplexPlaces_apply_isReal, normAtComplexPlaces_apply_isReal] at this

Premises used: NumberField.mixedEmbedding.normAtComplexPlaces_apply_isReal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
w : { w : InfinitePlace K // w.IsReal }
this : a.1 w = x.1 w
refine_2 : 0 < a.1 w
⊢ 0 < x.1 w

Tactic:
rw [← this]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
w : { w : InfinitePlace K // w.IsReal }
this : a.1 w = x.1 w
⊢ 0 < a.1 w

Tactic:
ha₁.2 w

Premises used: And.right
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
w : { w : InfinitePlace K // w.IsReal }
this : a.1 w = x.1 w
⊢ 0 < a.1 w

Tactic:
exact ha₁.2 w

Premises used: And.right
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
⊢ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A

Tactic:
have hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A := by
    refine subset_antisymm (fun x ⟨a, ha₁, ha₂⟩ ↦ ⟨?_, fun w ↦ ?_⟩) (Set.subset_preimage_image _ _)
    · rw [← hA, Set.mem_preimage, ← normAtAllPlaces_eq_of_normAtComplexPlaces_eq ha₂]
      exact Set.mem_image_of_mem normAtAllPlaces (Set.inter_subset_left ha₁)
    · have := funext_iff.mp ha₂ w
      rw [normAtComplexPlaces_apply_isReal, normAtComplexPlaces_apply_isReal] at this
      rw [← this]
      exact ha₁.2 w
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
rw :
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' plusPart A,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' A,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) A =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' A,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))

Tactic:
rw [volume_eq_two_pow_mul_volume_plusPart hA₁ hm, volume_eq_two_pi_pow_mul_integral hA₃
    (measurableSet_plusPart hm), ← mul_assoc]

Premises used: NumberField.mixedEmbedding.measurableSet_plusPart, mul_assoc, NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral, NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_plusPart
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
⊢ HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' plusPart A,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' A,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))

Tactic:
congr_arg (_ * _ * ·) <| setLIntegral_congr ?_

Premises used: HMul.hMul, congr_arg, MeasureTheory.setLIntegral_congr
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
refine : normAtComplexPlaces '' plusPart A =ᶠ[ae (F := Measure (realSpace K)) volume] normAtAllPlaces '' A
⊢ HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' plusPart A,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' A,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))

Tactic:
refine congr_arg (_ * _ * ·) <| setLIntegral_congr ?_

Premises used: HMul.hMul, congr_arg, MeasureTheory.setLIntegral_congr
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
rw :
  normAtAllPlaces '' A ∩
      ⋂ (w : { w : InfinitePlace K // w.IsReal }),
        {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} =ᶠ[ae (F := Measure (realSpace K)) volume]
    normAtAllPlaces '' A
⊢ normAtComplexPlaces '' plusPart A =ᶠ[ae (F := Measure (realSpace K)) volume] normAtAllPlaces '' A

Tactic:
rw [← volume_eq_two_pow_mul_two_pi_pow_mul_integral_aux hA]

Premises used: _private.0.NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral_aux
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
⊢ normAtAllPlaces '' A ∩
      ⋂ (w : { w : InfinitePlace K // w.IsReal }),
        {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} =ᶠ[ae (F := Measure (realSpace K)) volume]
    normAtAllPlaces '' A

Tactic:
inter_ae_eq_left_of_ae_eq_univ <| ae_eq_univ.mpr
    <| Set.compl_iInter _ ▸ measure_iUnion_null_iff.mpr fun w ↦ ?_

Premises used: Iff.mpr, Set.compl_iInter, MeasureTheory.inter_ae_eq_left_of_ae_eq_univ, MeasureTheory.measure_iUnion_null_iff, Eq.rec, MeasureTheory.ae_eq_univ, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
refine :
  ∀ (w : { w : InfinitePlace K // w.IsReal }),
    Eq (α := ℝ≥0∞)
      (((volume : Measure (realSpace K)) : (a : Set (realSpace K)) → ℝ≥0∞)
          {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ normAtAllPlaces '' A ∩
      ⋂ (w : { w : InfinitePlace K // w.IsReal }),
        {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} =ᶠ[ae (F := Measure (realSpace K)) volume]
    normAtAllPlaces '' A

Tactic:
refine inter_ae_eq_left_of_ae_eq_univ <| ae_eq_univ.mpr
    <| Set.compl_iInter _ ▸ measure_iUnion_null_iff.mpr fun w ↦ ?_

Premises used: Iff.mpr, MeasureTheory.inter_ae_eq_left_of_ae_eq_univ, MeasureTheory.ae_eq_univ
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
w : { w : InfinitePlace K // w.IsReal }
h :
  ∀ (x : realSpace K),
    Membership.mem (γ := Set (realSpace K)) {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}ᶜ x ↔
      Membership.mem (γ := Set (realSpace K)) {x : realSpace K | x (↑w : InfinitePlace K) = 0} x
⊢ Eq.{u_1 + 1} (α := Set (realSpace K)) {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}ᶜ
    {x : realSpace K | x (↑w : InfinitePlace K) = 0}

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
w : { w : InfinitePlace K // w.IsReal }
x : realSpace K
⊢ Membership.mem (γ := Set (realSpace K)) {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}ᶜ x ↔
    Membership.mem (γ := Set (realSpace K)) {x : realSpace K | x (↑w : InfinitePlace K) = 0} x

Tactic:
simp