awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' :
  ∀ {x : mixedSpace K},
    Eq (α := ℝ≥0∞) (A.indicator 1 x) ((normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x))
⊢ (ENNReal.ofReal (2 * π) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex } *
      ∫⁻ (a : InfinitePlace K → ℝ) in
        Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ioi 0,
        Set.indicator
          ((⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹'
            normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A)
          (fun (x : InfinitePlace K → ℝ) ↦
            ∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a (↑x : InfinitePlace K)))
          a ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A,
        ∏ w : { w : InfinitePlace K // w.IsComplex },
          ENNReal.ofReal
            (x
              (↑w :
                InfinitePlace K)) ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume
have erw : (ENNReal.ofReal (2 * π) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex } *
    ∫⁻ (a : InfinitePlace K → ℝ) in
      (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A ∩
        Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ioi 0,
      (fun (x : InfinitePlace K → ℝ) ↦
          (∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a (↑x : InfinitePlace K)) : ℝ≥0∞))
        a ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume) =
  ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
    ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A,
      ∏ w : { w : InfinitePlace K // w.IsComplex },
        ENNReal.ofReal
          (x (↑w : InfinitePlace K)) ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume
Tactic: erw [setLIntegral_indicator (by convert! hm.preimage mixedSpaceOfRealSpace.measurable)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' :
  ∀ {x : mixedSpace K},
    Eq (α := ℝ≥0∞) (A.indicator 1 x) ((normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x))
⊢ (ENNReal.ofReal (2 * π) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex } *
      ∫⁻ (a : InfinitePlace K → ℝ) in
        (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹'
            normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A ∩
          Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
            if w.IsReal then Set.univ else Set.Ioi 0,
        (fun (x : InfinitePlace K → ℝ) ↦
            (∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a (↑x : InfinitePlace K)) : ℝ≥0∞))
          a ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A,
        ∏ w : { w : InfinitePlace K // w.IsComplex },
          ENNReal.ofReal
            (x
              (↑w :
                InfinitePlace K)) ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume
have rw : (ENNReal.ofReal (2 * π) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex } *
    ∫⁻ (a : InfinitePlace K → ℝ) in
      (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
        Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ioi 0,
      (fun (x : InfinitePlace K → ℝ) ↦
          (∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a (↑x : InfinitePlace K)) : ℝ≥0∞))
        a ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume) =
  ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
    ∫⁻ (x : realSpace K) in
      (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
        Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ici 0,
      ∏ w : { w : InfinitePlace K // w.IsComplex },
        ENNReal.ofReal
          (x (↑w : InfinitePlace K)) ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume
Tactic: rw [hA, volume_eq_two_pi_pow_mul_integral_aux hA]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' :
  ∀ {x : mixedSpace K},
    Eq (α := ℝ≥0∞) (A.indicator 1 x) ((normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x))
⊢ (ENNReal.ofReal (2 * π) ^ Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex } *
      ∫⁻ (a : InfinitePlace K → ℝ) in
        (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
          Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
            if w.IsReal then Set.univ else Set.Ioi 0,
        (fun (x : InfinitePlace K → ℝ) ↦
            (∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a (↑x : InfinitePlace K)) : ℝ≥0∞))
          a ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in
        (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
          Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
            if w.IsReal then Set.univ else Set.Ici 0,
        ∏ w : { w : InfinitePlace K // w.IsComplex },
          ENNReal.ofReal
            (x
              (↑w :
                InfinitePlace K)) ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume
have e_a : (∫⁻ (a : InfinitePlace K → ℝ) in
    (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
      Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w.IsReal then Set.univ else Set.Ioi 0,
    (fun (x : InfinitePlace K → ℝ) ↦
        (∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a (↑x : InfinitePlace K)) : ℝ≥0∞))
      a ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume) =
  ∫⁻ (x : realSpace K) in
    (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
      Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w.IsReal then Set.univ else Set.Ici 0,
    ∏ w : { w : InfinitePlace K // w.IsComplex },
      ENNReal.ofReal
        (x (↑w : InfinitePlace K)) ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' :
  ∀ {x : mixedSpace K},
    Eq (α := ℝ≥0∞) (A.indicator 1 x) ((normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x))
⊢ (∫⁻ (a : InfinitePlace K → ℝ) in
      (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
        Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ioi 0,
      (fun (x : InfinitePlace K → ℝ) ↦
          (∏ x : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (a (↑x : InfinitePlace K)) : ℝ≥0∞))
        a ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume) =
    ∫⁻ (x : realSpace K) in
      (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) ⁻¹' A ∩
        Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w.IsReal then Set.univ else Set.Ici 0,
      ∏ w : { w : InfinitePlace K // w.IsComplex },
        ENNReal.ofReal
          (x (↑w : InfinitePlace K)) ∂Measure.pi (α := fun (i : InfinitePlace K) ↦ ℝ) fun (x : InfinitePlace K) ↦ volume
have e_a : ∀ (w : InfinitePlace K),
  Membership.mem (γ := Set (InfinitePlace K)) Set.univ w →
    (if w.IsReal then Set.univ else Set.Ioi 0) =ᶠ[ae (F := Measure ℝ) volume] if w.IsReal then Set.univ else Set.Ici 0
Tactic: refine setLIntegral_congr (ae_eq_set_inter (by rfl) (Measure.ae_eq_set_pi fun w _ ↦ ?_))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' :
  ∀ {x : mixedSpace K},
    Eq (α := ℝ≥0∞) (A.indicator 1 x) ((normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x))
w : InfinitePlace K
h : Membership.mem (γ := Set (InfinitePlace K)) Set.univ w
⊢ (if w.IsReal then Set.univ else Set.Ioi 0) =ᶠ[ae (F := Measure ℝ) volume] if w.IsReal then Set.univ else Set.Ici 0
have pos : w.IsReal → Set.univ =ᶠ[ae (F := Measure ℝ) volume] Set.univ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' :
  ∀ {x : mixedSpace K},
    Eq (α := ℝ≥0∞) (A.indicator 1 x) ((normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x))
w : InfinitePlace K
h : Membership.mem (γ := Set (InfinitePlace K)) Set.univ w
pos : w.IsReal → Set.univ =ᶠ[ae (F := Measure ℝ) volume] Set.univ
⊢ (if w.IsReal then Set.univ else Set.Ioi 0) =ᶠ[ae (F := Measure ℝ) volume] if w.IsReal then Set.univ else Set.Ici 0
have neg : ¬w.IsReal → Set.Ioi 0 =ᶠ[ae (F := Measure ℝ) volume] Set.Ici 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
⊢ normAtAllPlaces '' A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} =
    normAtComplexPlaces '' plusPart A
have h : ∀ (x : realSpace K),
  x ∈
      normAtAllPlaces '' A ∩
        ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} ↔
    x ∈ normAtComplexPlaces '' plusPart A
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
x : realSpace K
⊢ x ∈
      normAtAllPlaces '' A ∩
        ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} ↔
    x ∈ normAtComplexPlaces '' plusPart A
have h : x ∈
    normAtAllPlaces '' A ∩
      ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} →
  x ∈ normAtComplexPlaces '' plusPart A
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
x : realSpace K
h :
  x ∈
      normAtAllPlaces '' A ∩
        ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} →
    x ∈ normAtComplexPlaces '' plusPart A
⊢ x ∈
      normAtAllPlaces '' A ∩
        ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} ↔
    x ∈ normAtComplexPlaces '' plusPart A
have h₁ : x ∈ normAtComplexPlaces '' plusPart A →
  x ∈
    normAtAllPlaces '' A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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)
⊢ normAtAllPlaces a ∈ normAtComplexPlaces '' plusPart A
have h : Membership.mem (α := mixedSpace K) A
  ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces a) : mixedSpace K)
Tactic: refine ⟨mixedSpaceOfRealSpace (normAtAllPlaces a), ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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 :
  Membership.mem (α := mixedSpace K) A
    ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces a) : mixedSpace K)
⊢ normAtAllPlaces a ∈ normAtComplexPlaces '' plusPart A
have h₁ : Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K))
  {x : mixedSpace K | ∀ (w : { w : InfinitePlace K // w.IsReal }), 0 < x.1 w}
  ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces a) : mixedSpace K)
Tactic: refine ⟨mixedSpaceOfRealSpace (normAtAllPlaces a), ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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 :
  Membership.mem (α := mixedSpace K) A
    ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces a) : mixedSpace K)
h₁ :
  Membership.mem (α := mixedSpace K) (γ := Set (mixedSpace K))
    {x : mixedSpace K | ∀ (w : { w : InfinitePlace K // w.IsReal }), 0 < x.1 w}
    ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces a) : mixedSpace K)
⊢ normAtAllPlaces a ∈ normAtComplexPlaces '' plusPart A
have h₂ : normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces a)) = normAtAllPlaces a
Tactic: refine ⟨mixedSpaceOfRealSpace (normAtAllPlaces a), ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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)
⊢ Membership.mem (α := mixedSpace K) A
    ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces a) : mixedSpace K)
have h : normAtAllPlaces a ∈ normAtAllPlaces '' A
Tactic: rw [← hA, Set.mem_preimage, normAtAllPlaces_normAtAllPlaces]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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)
⊢ normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces a)) =
    normAtAllPlaces a
have h : normAtAllPlaces a = normAtAllPlaces a
Tactic: rw [normAtComplexPlaces_normAtAllPlaces]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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}
have h : ∀ (w : InfinitePlace K), normAtAllPlaces a w = normAtComplexPlaces a w
Tactic: refine ⟨⟨a, ha₁, funext fun w ↦ ?_⟩, Set.mem_iInter.mpr fun w ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ normAtComplexPlaces a ∈
    normAtAllPlaces '' A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}
have h₁ : ∀ (w : { w : InfinitePlace K // w.IsReal }),
  Membership.mem (γ := Set (realSpace K)) {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} (normAtComplexPlaces a)
Tactic: refine ⟨⟨a, ha₁, funext fun w ↦ ?_⟩, Set.mem_iInter.mpr fun w ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ normAtAllPlaces a w = normAtComplexPlaces a w
have h : ∀ (hw : w.IsReal), normAtAllPlaces a w = normAtComplexPlaces a w
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ normAtAllPlaces a w = normAtComplexPlaces a w
have h₁ : ∀ (hw : w.IsComplex), normAtAllPlaces a w = normAtComplexPlaces a w
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ normAtAllPlaces a w = normAtComplexPlaces a w
have h : (normAtPlace w : (a : mixedSpace K) → ℝ) a = normAtComplexPlaces a w
Tactic: rw [normAtAllPlaces_apply, normAtPlace_apply_of_isComplex hw,
          normAtComplexPlaces_apply_isComplex ⟨w, hw⟩]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ normAtAllPlaces a w = normAtComplexPlaces a w
have h₁ : ‖a.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖ = normAtComplexPlaces a w
Tactic: rw [normAtAllPlaces_apply, normAtPlace_apply_of_isComplex hw,
          normAtComplexPlaces_apply_isComplex ⟨w, hw⟩]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ normAtAllPlaces a w = normAtComplexPlaces a w
have 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)‖
Tactic: rw [normAtAllPlaces_apply, normAtPlace_apply_of_isComplex hw,
          normAtComplexPlaces_apply_isComplex ⟨w, hw⟩]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
have rw : x ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A ↔
  (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A
Tactic: rw [← hA]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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 ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A ↔
    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A
have simp_rw : normAtAllPlaces x ∈ normAtAllPlaces '' A ↔
  normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ normAtAllPlaces '' A
Tactic: simp_rw [Set.mem_preimage, Set.mem_image, normAtAllPlaces_norm_at_real_places]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
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
⊢ x ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A ↔
    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ normAtAllPlaces ⁻¹' normAtAllPlaces '' A
have 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)
Tactic: simp_rw [Set.mem_preimage, Set.mem_image, normAtAllPlaces_norm_at_real_places]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (hypothesis)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
⊢ ((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))
have hA₁ : ∀ (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]