awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ MeasurePreserving (α := mixedSpace K) (β := euclidean.mixedSpace K)
    (⇑(ContinuousLinearEquiv.symm (toMixed K)) : (a : mixedSpace K) → euclidean.mixedSpace K)
    (volume : Measure (mixedSpace K)) (volume : Measure (euclidean.mixedSpace K))
have this : MeasurePreserving (α := euclidean.mixedSpace K) (β := mixedSpace K)
  (⇑(Homeomorph.toMeasurableEquiv (ContinuousLinearEquiv.toHomeomorph (toMixed K))) :
    (a : euclidean.mixedSpace K) → mixedSpace K)
  (volume : Measure (euclidean.mixedSpace K)) (volume : Measure (mixedSpace K))
Tactic: have : MeasurePreserving (toMixed K).toHomeomorph.toMeasurableEquiv := volumePreserving_toMixed K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ DiscreteTopology.{u_1} ↥(euclidean.integerLattice K)
have rw : DiscreteTopology.{u_1}
  ↥(ZLattice.comap ℝ (E := mixedSpace K) (mixedEmbedding.integerLattice K)
        (↑(↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) : euclidean.mixedSpace K →ₗ[ℝ] mixedSpace K) :
      Submodule ℤ (euclidean.mixedSpace K))
Tactic: classical
  rw [euclidean.integerLattice]
  infer_instance
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ s
⊢ ((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w = -x.1 w
have simp_rw : ((prodCongr
            (piCongrRight (M := fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) (N :=
              fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) fun (w : { w : InfinitePlace K // w.IsReal }) ↦
              if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ)
            (ContinuousLinearEquiv.refl ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ)) :
          (a : mixedSpace K) → mixedSpace K)
        x).1
    w =
  -x.1 w
Tactic: simp_rw [negAt, prodCongr_apply, piCongrRight_apply, if_pos hw,
    ContinuousLinearEquiv.neg_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ s
simp_rw :
  ((prodCongr
              (piCongrRight (M := fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) (N :=
                fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) fun (w : { w : InfinitePlace K // w.IsReal }) ↦
                if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ)
              (ContinuousLinearEquiv.refl ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ)) :
            (a : mixedSpace K) → mixedSpace K)
          x).1
      w =
    -x.1 w
⊢ ((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w = -x.1 w
have simp_rw₁ : (piCongrRight (M := fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) (N :=
        fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) fun (w : { w : InfinitePlace K // w.IsReal }) ↦
        if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ :
      (a : (i : { w : InfinitePlace K // w.IsReal }) → ℝ) → (i : { w : InfinitePlace K // w.IsReal }) → ℝ)
    x.1 w =
  -x.1 w
Tactic: simp_rw [negAt, prodCongr_apply, piCongrRight_apply, if_pos hw,
    ContinuousLinearEquiv.neg_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ s
simp_rw :
  ((prodCongr
              (piCongrRight (M := fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) (N :=
                fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) fun (w : { w : InfinitePlace K // w.IsReal }) ↦
                if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ)
              (ContinuousLinearEquiv.refl ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ)) :
            (a : mixedSpace K) → mixedSpace K)
          x).1
      w =
    -x.1 w
simp_rw₁ :
  (piCongrRight (M := fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) (N :=
          fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) fun (w : { w : InfinitePlace K // w.IsReal }) ↦
          if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ :
        (a : (i : { w : InfinitePlace K // w.IsReal }) → ℝ) → (i : { w : InfinitePlace K // w.IsReal }) → ℝ)
      x.1 w =
    -x.1 w
⊢ ((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w = -x.1 w
have simp_rw₂ : (if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ : (a : ℝ) → ℝ) (x.1 w) = -x.1 w
Tactic: simp_rw [negAt, prodCongr_apply, piCongrRight_apply, if_pos hw,
    ContinuousLinearEquiv.neg_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ s
simp_rw :
  ((prodCongr
              (piCongrRight (M := fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) (N :=
                fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) fun (w : { w : InfinitePlace K // w.IsReal }) ↦
                if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ)
              (ContinuousLinearEquiv.refl ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ)) :
            (a : mixedSpace K) → mixedSpace K)
          x).1
      w =
    -x.1 w
simp_rw₁ :
  (piCongrRight (M := fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) (N :=
          fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) fun (w : { w : InfinitePlace K // w.IsReal }) ↦
          if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ :
        (a : (i : { w : InfinitePlace K // w.IsReal }) → ℝ) → (i : { w : InfinitePlace K // w.IsReal }) → ℝ)
      x.1 w =
    -x.1 w
simp_rw₂ : (if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ : (a : ℝ) → ℝ) (x.1 w) = -x.1 w
⊢ ((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w = -x.1 w
have simp_rw₃ : (neg ℝ : (a : ℝ) → ℝ) (x.1 w) = -x.1 w
Tactic: simp_rw [negAt, prodCongr_apply, piCongrRight_apply, if_pos hw,
    ContinuousLinearEquiv.neg_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
hw : w ∉ s
⊢ ((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w = x.1 w
have simp_rw : ((prodCongr
            (piCongrRight (M := fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) (N :=
              fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) fun (w : { w : InfinitePlace K // w.IsReal }) ↦
              if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ)
            (ContinuousLinearEquiv.refl ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ)) :
          (a : mixedSpace K) → mixedSpace K)
        x).1
    w =
  x.1 w
Tactic: simp_rw [negAt, prodCongr_apply, piCongrRight_apply, if_neg hw,
    ContinuousLinearEquiv.refl_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
hw : w ∉ s
simp_rw :
  ((prodCongr
              (piCongrRight (M := fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) (N :=
                fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) fun (w : { w : InfinitePlace K // w.IsReal }) ↦
                if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ)
              (ContinuousLinearEquiv.refl ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ)) :
            (a : mixedSpace K) → mixedSpace K)
          x).1
      w =
    x.1 w
⊢ ((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w = x.1 w
have simp_rw₁ : (piCongrRight (M := fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) (N :=
        fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) fun (w : { w : InfinitePlace K // w.IsReal }) ↦
        if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ :
      (a : (i : { w : InfinitePlace K // w.IsReal }) → ℝ) → (i : { w : InfinitePlace K // w.IsReal }) → ℝ)
    x.1 w =
  x.1 w
Tactic: simp_rw [negAt, prodCongr_apply, piCongrRight_apply, if_neg hw,
    ContinuousLinearEquiv.refl_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
hw : w ∉ s
simp_rw :
  ((prodCongr
              (piCongrRight (M := fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) (N :=
                fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) fun (w : { w : InfinitePlace K // w.IsReal }) ↦
                if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ)
              (ContinuousLinearEquiv.refl ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ)) :
            (a : mixedSpace K) → mixedSpace K)
          x).1
      w =
    x.1 w
simp_rw₁ :
  (piCongrRight (M := fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) (N :=
          fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) fun (w : { w : InfinitePlace K // w.IsReal }) ↦
          if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ :
        (a : (i : { w : InfinitePlace K // w.IsReal }) → ℝ) → (i : { w : InfinitePlace K // w.IsReal }) → ℝ)
      x.1 w =
    x.1 w
⊢ ((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w = x.1 w
have simp_rw₂ : (if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ : (a : ℝ) → ℝ) (x.1 w) = x.1 w
Tactic: simp_rw [negAt, prodCongr_apply, piCongrRight_apply, if_neg hw,
    ContinuousLinearEquiv.refl_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
hw : w ∉ s
simp_rw :
  ((prodCongr
              (piCongrRight (M := fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) (N :=
                fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) fun (w : { w : InfinitePlace K // w.IsReal }) ↦
                if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ)
              (ContinuousLinearEquiv.refl ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ)) :
            (a : mixedSpace K) → mixedSpace K)
          x).1
      w =
    x.1 w
simp_rw₁ :
  (piCongrRight (M := fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) (N :=
          fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) fun (w : { w : InfinitePlace K // w.IsReal }) ↦
          if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ :
        (a : (i : { w : InfinitePlace K // w.IsReal }) → ℝ) → (i : { w : InfinitePlace K // w.IsReal }) → ℝ)
      x.1 w =
    x.1 w
simp_rw₂ : (if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ : (a : ℝ) → ℝ) (x.1 w) = x.1 w
⊢ ((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w = x.1 w
have simp_rw₃ : (ContinuousLinearEquiv.refl ℝ ℝ : (a : ℝ) → ℝ) (x.1 w) = x.1 w
Tactic: simp_rw [negAt, prodCongr_apply, piCongrRight_apply, if_neg hw,
    ContinuousLinearEquiv.refl_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
⊢ norm (E := ℝ) (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w) = ‖x.1 w‖
have pos : ∀ (hw : w ∈ s), norm (E := ℝ) (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w) = ‖x.1 w‖
Tactic: by_cases hw : w ∈ s
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
pos : ∀ (hw : w ∈ s), norm (E := ℝ) (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w) = ‖x.1 w‖
⊢ norm (E := ℝ) (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w) = ‖x.1 w‖
have neg : ∀ (hw : w ∉ s), norm (E := ℝ) (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w) = ‖x.1 w‖
Tactic: by_cases hw : w ∈ s
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
inst_1 : NumberField K
⊢ MeasurePreserving (α := mixedSpace K) (β := mixedSpace K) (⇑(negAt s) : (a : mixedSpace K) → mixedSpace K)
    (volume : Measure (mixedSpace K)) (volume : Measure (mixedSpace K))
have refine : ∀ (w : { w : InfinitePlace K // w.IsReal }),
  MeasurePreserving (α := ℝ) (β := ℝ)
    (LinearMap.toAddHom
        (↑((fun (i : { w : InfinitePlace K // w.IsReal }) ↦
                ((↑((fun (w : { w : InfinitePlace K // w.IsReal }) ↦
                          (if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ : ℝ ≃L[ℝ] ℝ))
                        i) :
                    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                      (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i) :
                  (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i))
              w) :
          (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w →ₗ[ℝ]
            (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w)).1
    volume volume
Tactic: refine MeasurePreserving.prod (volume_preserving_pi fun w ↦ ?_) (MeasurePreserving.id _)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
inst_1 : NumberField K
w : { w : InfinitePlace K // w.IsReal }
⊢ MeasurePreserving (α := ℝ) (β := ℝ)
    (LinearMap.toAddHom
        (↑((fun (i : { w : InfinitePlace K // w.IsReal }) ↦
                ((↑((fun (w : { w : InfinitePlace K // w.IsReal }) ↦
                          (if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ : ℝ ≃L[ℝ] ℝ))
                        i) :
                    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                      (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i) :
                  (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i))
              w) :
          (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w →ₗ[ℝ]
            (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w)).1
    volume volume
have pos : ∀ (hw : w ∈ s),
  MeasurePreserving (α := ℝ) (β := ℝ)
    (LinearMap.toAddHom
        (↑((fun (i : { w : InfinitePlace K // w.IsReal }) ↦
                ((↑((fun (w : { w : InfinitePlace K // w.IsReal }) ↦
                          (if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ : ℝ ≃L[ℝ] ℝ))
                        i) :
                    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                      (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i) :
                  (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i))
              w) :
          (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w →ₗ[ℝ]
            (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w)).1
    volume volume
Tactic: by_cases hw : w ∈ s
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
inst_1 : NumberField K
w : { w : InfinitePlace K // w.IsReal }
pos :
  ∀ (hw : w ∈ s),
    MeasurePreserving (α := ℝ) (β := ℝ)
      (LinearMap.toAddHom
          (↑((fun (i : { w : InfinitePlace K // w.IsReal }) ↦
                  ((↑((fun (w : { w : InfinitePlace K // w.IsReal }) ↦
                            (if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ : ℝ ≃L[ℝ] ℝ))
                          i) :
                      (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                        (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i) :
                    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                      (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i))
                w) :
            (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w →ₗ[ℝ]
              (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w)).1
      volume volume
⊢ MeasurePreserving (α := ℝ) (β := ℝ)
    (LinearMap.toAddHom
        (↑((fun (i : { w : InfinitePlace K // w.IsReal }) ↦
                ((↑((fun (w : { w : InfinitePlace K // w.IsReal }) ↦
                          (if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ : ℝ ≃L[ℝ] ℝ))
                        i) :
                    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                      (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i) :
                  (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i))
              w) :
          (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w →ₗ[ℝ]
            (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w)).1
    volume volume
have neg : ∀ (hw : w ∉ s),
  MeasurePreserving (α := ℝ) (β := ℝ)
    (LinearMap.toAddHom
        (↑((fun (i : { w : InfinitePlace K // w.IsReal }) ↦
                ((↑((fun (w : { w : InfinitePlace K // w.IsReal }) ↦
                          (if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ : ℝ ≃L[ℝ] ℝ))
                        i) :
                    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                      (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i) :
                  (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i))
              w) :
          (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w →ₗ[ℝ]
            (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w)).1
    volume volume
Tactic: by_cases hw : w ∈ s
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
inst_1 : NumberField K
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ s
⊢ MeasurePreserving (α := ℝ) (β := ℝ)
    (LinearMap.toAddHom
        (↑((fun (i : { w : InfinitePlace K // w.IsReal }) ↦
                ((↑((fun (w : { w : InfinitePlace K // w.IsReal }) ↦
                          (if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ : ℝ ≃L[ℝ] ℝ))
                        i) :
                    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                      (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i) :
                  (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i))
              w) :
          (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w →ₗ[ℝ]
            (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w)).1
    volume volume
have pos : MeasurePreserving (α := ℝ) (β := ℝ) (LinearMap.toAddHom (↑(↑(neg ℝ) : ℝ ≃ₗ[ℝ] ℝ) : ℝ →ₗ[ℝ] ℝ)).1 volume volume
Tactic: simp_rw [if_pos hw]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
inst_1 : NumberField K
w : { w : InfinitePlace K // w.IsReal }
hw : w ∉ s
⊢ MeasurePreserving (α := ℝ) (β := ℝ)
    (LinearMap.toAddHom
        (↑((fun (i : { w : InfinitePlace K // w.IsReal }) ↦
                ((↑((fun (w : { w : InfinitePlace K // w.IsReal }) ↦
                          (if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ : ℝ ≃L[ℝ] ℝ))
                        i) :
                    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                      (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i) :
                  (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i ≃ₗ[ℝ]
                    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) i))
              w) :
          (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w →ₗ[ℝ]
            (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) w)).1
    volume volume
have neg : MeasurePreserving (α := ℝ) (β := ℝ)
  (LinearMap.toAddHom (↑(↑(ContinuousLinearEquiv.refl ℝ ℝ) : ℝ ≃ₗ[ℝ] ℝ) : ℝ →ₗ[ℝ] ℝ)).1 volume volume
Tactic: simp_rw [if_neg hw]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : InfinitePlace K
⊢ Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) ((negAt s : (a : mixedSpace K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
have inl : ∀ (hw : w.IsReal),
  Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) ((negAt s : (a : mixedSpace K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : InfinitePlace K
inl :
  ∀ (hw : w.IsReal),
    Eq (α := ℝ)
      ((normAtPlace w : (a : mixedSpace K) → ℝ) ((negAt s : (a : mixedSpace K) → mixedSpace K) x : mixedSpace K) : ℝ)
      ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
⊢ Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) ((negAt s : (a : mixedSpace K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
have inr : ∀ (hw : w.IsComplex),
  Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) ((negAt s : (a : mixedSpace K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : InfinitePlace K
hw : w.IsReal
⊢ Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) ((negAt s : (a : mixedSpace K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
have inl : norm (E := ℝ)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)) =
  ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
Tactic: simp_rw [normAtPlace_apply_of_isReal hw, negAt_apply_norm_isReal]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) ((negAt s : (a : mixedSpace K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
have inr : norm (E := ℂ)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).2
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)) =
  ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖
Tactic: simp_rw [normAtPlace_apply_of_isComplex hw, negAt_apply_isComplex]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
⊢ (negAt s).symm = negAt s
have h : ∀ (x : mixedSpace K) (w : { w : InfinitePlace K // w.IsReal }),
  Eq (α := ℝ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w)
Tactic: ext x w