awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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 ContinuousLinearEquiv.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
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 ContinuousLinearEquiv.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 ContinuousLinearEquiv.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
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
pos : MeasurePreserving (α := ℝ) (β := ℝ) (LinearMap.toAddHom (↑(↑(neg ℝ) : ℝ ≃ₗ[ℝ] ℝ) : ℝ →ₗ[ℝ] ℝ)).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

Tactic:
simp_rw [if_pos hw]

Premises used: if_pos
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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 (↑(↑(neg ℝ) : ℝ ≃ₗ[ℝ] ℝ) : ℝ →ₗ[ℝ] ℝ)).1 volume volume

Tactic:
Measure.measurePreserving_neg _

Premises used: MeasureTheory.Measure.measurePreserving_neg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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 (↑(↑(neg ℝ) : ℝ ≃ₗ[ℝ] ℝ) : ℝ →ₗ[ℝ] ℝ)).1 volume volume

Tactic:
exact Measure.measurePreserving_neg _

Premises used: MeasureTheory.Measure.measurePreserving_neg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
neg :
  MeasurePreserving (α := ℝ) (β := ℝ)
    (LinearMap.toAddHom (↑(↑(ContinuousLinearEquiv.refl ℝ ℝ) : ℝ ≃ₗ[ℝ] ℝ) : ℝ →ₗ[ℝ] ℝ)).1 volume volume
⊢ MeasurePreserving (α := ℝ) (β := ℝ)
    (LinearMap.toAddHom
        (↑((fun (i : { w : InfinitePlace K // w.IsReal }) ↦
                ((↑((fun (w : { w : InfinitePlace K // w.IsReal }) ↦
                          (if w ∈ s then ContinuousLinearEquiv.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:
simp_rw [if_neg hw]

Premises used: if_neg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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 (↑(↑(ContinuousLinearEquiv.refl ℝ ℝ) : ℝ ≃ₗ[ℝ] ℝ) : ℝ →ₗ[ℝ] ℝ)).1 volume volume

Tactic:
MeasurePreserving.id _

Premises used: MeasureTheory.MeasurePreserving.id
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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 (↑(↑(ContinuousLinearEquiv.refl ℝ ℝ) : ℝ ≃ₗ[ℝ] ℝ) : ℝ →ₗ[ℝ] ℝ)).1 volume volume

Tactic:
exact MeasurePreserving.id _

Premises used: MeasureTheory.MeasurePreserving.id
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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 : ℝ)
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 : ℝ)
⊢ 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

Premises used: NumberField.InfinitePlace.isReal_or_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : InfinitePlace K
hw : w.IsReal
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)‖
⊢ Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) ((negAt s : (a : mixedSpace K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)

Tactic:
simp_rw [normAtPlace_apply_of_isReal hw, negAt_apply_norm_isReal]

Premises used: NumberField.mixedEmbedding.normAtPlace_apply_of_isReal, NumberField.mixedEmbedding.negAt_apply_norm_isReal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : InfinitePlace K
hw : w.IsComplex
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)‖
⊢ Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) ((negAt s : (a : mixedSpace K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)

Tactic:
simp_rw [normAtPlace_apply_of_isComplex hw, negAt_apply_isComplex]

Premises used: NumberField.mixedEmbedding.negAt_apply_isComplex, NumberField.mixedEmbedding.normAtPlace_apply_of_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
inst_1 : NumberField K
x : mixedSpace K
⊢ Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) ((negAt s : (a : mixedSpace K) → mixedSpace K) x : mixedSpace K) :
      ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)

Tactic:
norm_eq_of_normAtPlace_eq (fun w ↦ normAtPlace_negAt _ _ w)

Premises used: NumberField.mixedEmbedding.normAtPlace_negAt, NumberField.mixedEmbedding.norm_eq_of_normAtPlace_eq
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
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)
h₁ :
  ∀ (x : mixedSpace K) (w : { w : InfinitePlace K // w.IsComplex }),
    Eq (α := ℂ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).2 w)
      (((negAt s : (a : mixedSpace K) → mixedSpace K) x).2 w)
⊢ (negAt s).symm = negAt s

Tactic:
ext x w
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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),
    Eq (α := ℝ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w)
      (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w)
neg :
  ∀ (hw : w ∉ s),
    Eq (α := ℝ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w)
      (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w)
⊢ Eq (α := ℝ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w)

Tactic:
by_cases hw : w ∈ s
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
pos : (((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w = -x.1 w
pos₁ :
  ((ContinuousLinearEquiv.symm
              (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
pos₂ :
  ((prodCongr
              (ContinuousLinearEquiv.symm
                (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.symm (ContinuousLinearEquiv.refl ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ))) :
            (a : mixedSpace K) → mixedSpace K)
          x).1
      w =
    -x.1 w
pos₃ :
  (ContinuousLinearEquiv.symm
          (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
pos₄ :
  (ContinuousLinearEquiv.symm (if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) : (a : ℝ) → ℝ) (x.1 w) = -x.1 w
pos₅ : (ContinuousLinearEquiv.symm (neg ℝ) : (a : ℝ) → ℝ) (x.1 w) = -x.1 w
pos₆ : (neg ℝ : (a : ℝ) → ℝ) (x.1 w) = -x.1 w
⊢ Eq (α := ℝ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w)

Tactic:
simp_rw [negAt_apply_isReal_and_mem _ hw, negAt, prodCongr_symm,
        prodCongr_apply, piCongrRight_symm_apply, if_pos hw, symm_neg,
        neg_apply]

Premises used: ContinuousLinearEquiv.symm_neg, NumberField.mixedEmbedding.negAt, ContinuousLinearEquiv.prodCongr_symm, if_pos, ContinuousLinearEquiv.neg_apply, NumberField.mixedEmbedding.negAt_apply_isReal_and_mem, ContinuousLinearEquiv.prodCongr_apply, ContinuousLinearEquiv.piCongrRight_symm_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
neg : (((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w = x.1 w
neg₁ :
  ((ContinuousLinearEquiv.symm
              (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 ContinuousLinearEquiv.neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ)
                (ContinuousLinearEquiv.refl ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ))) :
            (a : mixedSpace K) → mixedSpace K)
          x).1
      w =
    x.1 w
neg₂ :
  ((prodCongr
              (ContinuousLinearEquiv.symm
                (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 ContinuousLinearEquiv.neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ))
              (ContinuousLinearEquiv.symm (ContinuousLinearEquiv.refl ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ))) :
            (a : mixedSpace K) → mixedSpace K)
          x).1
      w =
    x.1 w
neg₃ :
  (ContinuousLinearEquiv.symm
          (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 ContinuousLinearEquiv.neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) :
        (a : (i : { w : InfinitePlace K // w.IsReal }) → ℝ) → (i : { w : InfinitePlace K // w.IsReal }) → ℝ)
      x.1 w =
    x.1 w
neg₄ :
  (ContinuousLinearEquiv.symm (if w ∈ s then ContinuousLinearEquiv.neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) :
        (a : ℝ) → ℝ)
      (x.1 w) =
    x.1 w
neg₅ : (ContinuousLinearEquiv.symm (ContinuousLinearEquiv.refl ℝ ℝ) : (a : ℝ) → ℝ) (x.1 w) = x.1 w
neg₆ : (ContinuousLinearEquiv.refl ℝ ℝ : (a : ℝ) → ℝ) (x.1 w) = x.1 w
⊢ Eq (α := ℝ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w)

Tactic:
simp_rw [negAt_apply_isReal_and_notMem _ hw, negAt, prodCongr_symm,
        prodCongr_apply, piCongrRight_symm_apply, if_neg hw, refl_symm,
        refl_apply]

Premises used: NumberField.mixedEmbedding.negAt, ContinuousLinearEquiv.prodCongr_symm, NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem, ContinuousLinearEquiv.refl_apply, ContinuousLinearEquiv.refl_symm, ContinuousLinearEquiv.prodCongr_apply, if_neg, ContinuousLinearEquiv.piCongrRight_symm_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
w : { w : InfinitePlace K // w.IsComplex }
⊢ Eq (α := ℂ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).2 w)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).2 w)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
pos : ∀ (hw : x.1 w ≤ 0), ((negAt (signSet x) : (a : mixedSpace K) → mixedSpace K) x).1 w = ‖x.1 w‖
neg : ∀ (hw : ¬x.1 w ≤ 0), ((negAt (signSet x) : (a : mixedSpace K) → mixedSpace K) x).1 w = ‖x.1 w‖
⊢ ((negAt (signSet x) : (a : mixedSpace K) → mixedSpace K) x).1 w = ‖x.1 w‖

Tactic:
by_cases hw : x.1 w ≤ 0

Premises used: Prod.fst
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
hw : x.1 w ≤ 0
pos : -x.1 w = ‖x.1 w‖
pos₁ pos₂ : -x.1 w = -x.1 w
⊢ ((negAt (signSet x) : (a : mixedSpace K) → mixedSpace K) x).1 w = ‖x.1 w‖

Tactic:
rw [negAt_apply_isReal_and_mem _ hw, Real.norm_of_nonpos hw]

Premises used: Real.norm_of_nonpos, NumberField.mixedEmbedding.negAt_apply_isReal_and_mem
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
hw : ¬x.1 w ≤ 0
neg : x.1 w = ‖x.1 w‖
neg₁ neg₂ : x.1 w = x.1 w
⊢ ((negAt (signSet x) : (a : mixedSpace K) → mixedSpace K) x).1 w = ‖x.1 w‖

Tactic:
rw [negAt_apply_isReal_and_notMem _ hw, Real.norm_of_nonneg (lt_of_not_ge hw).le]

Premises used: lt_of_not_ge, LT.lt.le, NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsComplex }
⊢ ((negAt (signSet x) : (a : mixedSpace K) → mixedSpace K) x).2 w = x.2 w

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
A : Set (mixedSpace K)
rw :
  Eq (α := Set (mixedSpace K)) ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) ⁻¹' A)
    ((⇑(negAt s).symm : (a : mixedSpace K) → mixedSpace K) ⁻¹' A)
rw₁ rw₂ :
  Eq (α := Set (mixedSpace K)) ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) ⁻¹' A)
    ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) ⁻¹' A)
⊢ Eq (α := Set (mixedSpace K)) ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) ⁻¹' A)
    ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' A)

Tactic:
rw [ContinuousLinearEquiv.image_eq_preimage_symm, negAt_symm]

Premises used: NumberField.mixedEmbedding.negAt_symm, ContinuousLinearEquiv.image_eq_preimage_symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hx : Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ s
obtain :
  ∀ (y : mixedSpace K) (hy : y ∈ plusPart A), LT.lt (α := ℝ) (((negAt s : (a : mixedSpace K) → mixedSpace K) y).1 w) 0
⊢ x.1 w < 0

Tactic:
obtain ⟨y, hy, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
A : Set (mixedSpace K)
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ s
y : mixedSpace K
hy : y ∈ plusPart A
rw : 0 < y.1 w
⊢ LT.lt (α := ℝ) (((negAt s : (a : mixedSpace K) → mixedSpace K) y).1 w) 0

Tactic:
rw [negAt_apply_isReal_and_mem _ hw, neg_lt_zero]

Premises used: neg_lt_zero, NumberField.mixedEmbedding.negAt_apply_isReal_and_mem
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
A : Set (mixedSpace K)
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ 0 < y.1 w

Tactic:
hy.2 w

Premises used: And.right
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
A : Set (mixedSpace K)
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ 0 < y.1 w

Tactic:
exact hy.2 w

Premises used: And.right
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hx : Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x
w : { w : InfinitePlace K // w.IsReal }
hw : w ∉ s
obtain :
  ∀ (y : mixedSpace K) (hy : y ∈ plusPart A), LT.lt (α := ℝ) 0 (((negAt s : (a : mixedSpace K) → mixedSpace K) y).1 w)
⊢ 0 < x.1 w

Tactic:
obtain ⟨y, hy, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
A : Set (mixedSpace K)
w : { w : InfinitePlace K // w.IsReal }
hw : w ∉ s
y : mixedSpace K
hy : y ∈ plusPart A
rw : 0 < y.1 w
⊢ LT.lt (α := ℝ) 0 (((negAt s : (a : mixedSpace K) → mixedSpace K) y).1 w)

Tactic:
rw [negAt_apply_isReal_and_notMem _ hw]

Premises used: NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
A : Set (mixedSpace K)
w : { w : InfinitePlace K // w.IsReal }
hw : w ∉ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ 0 < y.1 w

Tactic:
hy.2 w

Premises used: And.right
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
A : Set (mixedSpace K)
w : { w : InfinitePlace K // w.IsReal }
hw : w ∉ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ 0 < y.1 w

Tactic:
exact hy.2 w

Premises used: And.right
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
s t : Set { w : InfinitePlace K // w.IsReal }
hst : s ≠ t
⊢ Function.onFun (β := Set (mixedSpace K)) Disjoint
    (fun (s : Set { w : InfinitePlace K // w.IsReal }) ↦ (⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A)
    s t

Tactic:
Set.disjoint_left.mpr fun _ hx hx' ↦ ?_

Premises used: Iff.mpr, Set.disjoint_left