awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 }
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)
⊢ (negAt s).symm = negAt s
have 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)
Tactic: ext x 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 : { 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)
have 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)
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),
    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)
have 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)
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 }
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)
have pos : (((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w = -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]
-- 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
pos : (((negAt s).symm : (a : mixedSpace K) → mixedSpace K) 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)
have 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
Tactic: simp_rw [negAt_apply_isReal_and_mem _ hw, negAt, prodCongr_symm,
        prodCongr_apply, piCongrRight_symm_apply, if_pos hw, symm_neg,
        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
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
⊢ Eq (α := ℝ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w)
have 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
Tactic: simp_rw [negAt_apply_isReal_and_mem _ hw, negAt, prodCongr_symm,
        prodCongr_apply, piCongrRight_symm_apply, if_pos hw, symm_neg,
        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
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
⊢ Eq (α := ℝ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w)
have 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
Tactic: simp_rw [negAt_apply_isReal_and_mem _ hw, negAt, prodCongr_symm,
        prodCongr_apply, piCongrRight_symm_apply, if_pos hw, symm_neg,
        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
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
⊢ Eq (α := ℝ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w)
have pos₄ : (ContinuousLinearEquiv.symm (if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) : (a : ℝ) → ℝ) (x.1 w) = -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]
-- 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
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
⊢ Eq (α := ℝ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w)
have pos₅ : (ContinuousLinearEquiv.symm (neg ℝ) : (a : ℝ) → ℝ) (x.1 w) = -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]
-- 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
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
⊢ Eq (α := ℝ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w)
have pos₆ : (neg ℝ : (a : ℝ) → ℝ) (x.1 w) = -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]
-- 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
⊢ Eq (α := ℝ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w)
have neg : (((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w = 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]
-- 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
neg : (((negAt s).symm : (a : mixedSpace K) → mixedSpace K) 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)
have 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
Tactic: simp_rw [negAt_apply_isReal_and_notMem _ hw, negAt, prodCongr_symm,
        prodCongr_apply, piCongrRight_symm_apply, if_neg hw, refl_symm,
        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
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
⊢ Eq (α := ℝ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w)
have 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
Tactic: simp_rw [negAt_apply_isReal_and_notMem _ hw, negAt, prodCongr_symm,
        prodCongr_apply, piCongrRight_symm_apply, if_neg hw, refl_symm,
        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
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
⊢ Eq (α := ℝ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w)
have 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
Tactic: simp_rw [negAt_apply_isReal_and_notMem _ hw, negAt, prodCongr_symm,
        prodCongr_apply, piCongrRight_symm_apply, if_neg hw, refl_symm,
        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
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
⊢ Eq (α := ℝ) ((((negAt s).symm : (a : mixedSpace K) → mixedSpace K) x).1 w)
    (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w)
have neg₄ : (ContinuousLinearEquiv.symm (if w ∈ s then ContinuousLinearEquiv.neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) :
      (a : ℝ) → ℝ)
    (x.1 w) =
  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]