awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ Membership.mem (γ := Set (mixedSpace K))
      ((⇑(AlgHom.toLinearMap (RingHom.toIntAlgHom (mixedEmbedding K))) : (a : K) → mixedSpace K) ''
        (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set K))
      x ↔
    Membership.mem (γ := Set (mixedSpace K))
      ((⇑(mixedEmbedding K) : (a : K) → mixedSpace K) '' (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Set K)) x

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
h :
  ∀ (x : mixedSpace K),
    Membership.mem (γ := Submodule ℤ (mixedSpace K))
        (Submodule.span ℤ
          (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (⇑(fractionalIdealLatticeBasis K I :
                  Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
              (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))
        x ↔
      x ∈ idealLattice K I
⊢ Submodule.span ℤ
      (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
        (⇑(fractionalIdealLatticeBasis K I :
              Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)) =
    idealLattice K I

Tactic:
ext x
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ Membership.mem (γ := Submodule ℤ (mixedSpace K))
      (Submodule.span ℤ
        (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))
      x ↔
    x ∈ idealLattice K I

Tactic:
simp [mem_span_fractionalIdealLatticeBasis]

Premises used: NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
rw :
  DiscreteTopology.{u_1}
    ↥(Submodule.span ℤ
        (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))
⊢ DiscreteTopology.{u_1} ↥(idealLattice K I)

Tactic:
rw [← span_idealLatticeBasis]

Premises used: NumberField.mixedEmbedding.span_idealLatticeBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ DiscreteTopology.{u_1}
    ↥(Submodule.span ℤ
        (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
rw rw₁ rw₂ :
  DiscreteTopology.{u_1}
    ↥(Submodule.span ℤ
        (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))
⊢ DiscreteTopology.{u_1} ↥(idealLattice K I)

Tactic:
classical
  rw [← span_idealLatticeBasis]
  infer_instance

Premises used: NumberField.mixedEmbedding.span_idealLatticeBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
simp_rw :
  IsZLattice ℝ (E := mixedSpace K)
    (Submodule.span ℤ
      (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
        (⇑(fractionalIdealLatticeBasis K I :
              Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))
⊢ IsZLattice.{0, u_1} ℝ (E := mixedSpace K) (idealLattice K I)

Tactic:
simp_rw [← span_idealLatticeBasis]

Premises used: NumberField.mixedEmbedding.span_idealLatticeBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ IsZLattice ℝ (E := mixedSpace K)
    (Submodule.span ℤ
      (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
        (⇑(fractionalIdealLatticeBasis K I :
              Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
          (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
rw :
  MeasureTheory.IsAddFundamentalDomain.{u_1, u_1}
    ↥(Submodule.span ℤ
        (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))
    (α := mixedSpace K)
    (ZSpan.fundamentalDomain (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
      (fractionalIdealLatticeBasis K I))
    (MeasureTheory.volume : MeasureTheory.Measure (mixedSpace K))
⊢ MeasureTheory.IsAddFundamentalDomain.{u_1, u_1} ↥(idealLattice K I) (α := mixedSpace K)
    (ZSpan.fundamentalDomain (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
      (fractionalIdealLatticeBasis K I))
    (MeasureTheory.volume : MeasureTheory.Measure (mixedSpace K))

Tactic:
rw [← span_idealLatticeBasis]

Premises used: NumberField.mixedEmbedding.span_idealLatticeBasis
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ MeasureTheory.IsAddFundamentalDomain.{u_1, u_1}
    ↥(Submodule.span ℤ
        (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))
    (α := mixedSpace K)
    (ZSpan.fundamentalDomain (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
      (fractionalIdealLatticeBasis K I))
    (MeasureTheory.volume : MeasureTheory.Measure (mixedSpace K))

Tactic:
ZSpan.isAddFundamentalDomain (fractionalIdealLatticeBasis K I) _

Premises used: Set.Mem, setOf, NumberField.mixedEmbedding.fractionalIdealLatticeBasis, ZSpan.isAddFundamentalDomain
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
⊢ MeasureTheory.IsAddFundamentalDomain.{u_1, u_1}
    ↥(Submodule.span ℤ
        (Set.range (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (⇑(fractionalIdealLatticeBasis K I :
                Basis (ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) ℝ (mixedSpace K)) :
            (a : ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) → mixedSpace K)))
    (α := mixedSpace K)
    (ZSpan.fundamentalDomain (ι := ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)) (K := ℝ)
      (fractionalIdealLatticeBasis K I))
    (MeasureTheory.volume : MeasureTheory.Measure (mixedSpace K))

Tactic:
exact ZSpan.isAddFundamentalDomain (fractionalIdealLatticeBasis K I) _

Premises used: NumberField.mixedEmbedding.fractionalIdealLatticeBasis, ZSpan.isAddFundamentalDomain
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Nontrivial.{u_1} (euclidean.mixedSpace K)

Tactic:
(toMixed K).toEquiv.nontrivial

Premises used: Equiv.nontrivial, ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.toEquiv, NumberField.mixedEmbedding.euclidean.toMixed
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
rw₁ rw₂ : finrank ℚ K = finrank ℚ K
⊢ finrank.{0, u_1} ℝ (euclidean.mixedSpace K) = finrank ℚ K

Tactic:
rw [LinearEquiv.finrank_eq (toMixed K).toLinearEquiv, mixedEmbedding.finrank]

Premises used: ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.finrank_eq, NumberField.mixedEmbedding.finrank, NumberField.mixedEmbedding.euclidean.toMixed
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a :
  ∀ (i : index K) (x : { w : InfinitePlace K // w.IsReal }),
    Eq (α := ℝ)
      (((Basis.map (OrthonormalBasis.toBasis (stdOrthonormalBasis K))
                (↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
              (a : index K) → mixedSpace K)
            i).1
        x)
      (((stdBasis K : (a : index K) → mixedSpace K) i).1 x)
a₁ :
  ∀ (i : index K) (x : { w : InfinitePlace K // w.IsComplex }),
    Eq (α := ℂ)
      (((Basis.map (OrthonormalBasis.toBasis (stdOrthonormalBasis K))
                (↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
              (a : index K) → mixedSpace K)
            i).2
        x)
      (((stdBasis K : (a : index K) → mixedSpace K) i).2 x)
⊢ Eq (α := Basis (index K) ℝ (mixedSpace K))
    (Basis.map (OrthonormalBasis.toBasis (stdOrthonormalBasis K))
      (↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K))
    (stdBasis K)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i : index K
x : { w : InfinitePlace K // w.IsReal }
⊢ Eq (α := ℝ)
    (((Basis.map (OrthonormalBasis.toBasis (stdOrthonormalBasis K))
              (↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
            (a : index K) → mixedSpace K)
          i).1
      x)
    (((stdBasis K : (a : index K) → mixedSpace K) i).1 x)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i : index K
x : { w : InfinitePlace K // w.IsComplex }
⊢ Eq (α := ℂ)
    (((Basis.map (OrthonormalBasis.toBasis (stdOrthonormalBasis K))
              (↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) :
            (a : index K) → mixedSpace K)
          i).2
      x)
    (((stdBasis K : (a : index K) → mixedSpace K) i).2 x)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 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
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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))
⊢ 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))

Tactic:
this.symm

Premises used: MeasureTheory.MeasurePreserving.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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))
⊢ 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))

Tactic:
exact this.symm

Premises used: MeasureTheory.MeasurePreserving.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 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:
infer_instance
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw rw₁ 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))
⊢ DiscreteTopology.{u_1} ↥(euclidean.integerLattice K)

Tactic:
classical
  rw [euclidean.integerLattice]
  infer_instance

Premises used: NumberField.mixedEmbedding.euclidean.integerLattice
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsZLattice.{0, u_1} ℝ (E := euclidean.mixedSpace K)
    (ZLattice.comap ℝ (E := mixedSpace K) (mixedEmbedding.integerLattice K)
      (↑(↑(toMixed K) : euclidean.mixedSpace K ≃ₗ[ℝ] mixedSpace K) : euclidean.mixedSpace K →ₗ[ℝ] mixedSpace K))

Tactic:
infer_instance
-- 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
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
simp_rw₃ : (neg ℝ : (a : ℝ) → ℝ) (x.1 w) = -x.1 w
⊢ ((negAt s : (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]

Premises used: NumberField.mixedEmbedding.negAt, if_pos, ContinuousLinearEquiv.neg_apply, ContinuousLinearEquiv.prodCongr_apply, ContinuousLinearEquiv.piCongrRight_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
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
simp_rw₃ : (ContinuousLinearEquiv.refl ℝ ℝ : (a : ℝ) → ℝ) (x.1 w) = x.1 w
⊢ ((negAt s : (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]

Premises used: NumberField.mixedEmbedding.negAt, ContinuousLinearEquiv.refl_apply, ContinuousLinearEquiv.prodCongr_apply, if_neg, ContinuousLinearEquiv.piCongrRight_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 }
⊢ ((negAt s : (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 }
x : mixedSpace K
⊢ ((negAt s : (a : mixedSpace K) → mixedSpace K) x).2 = x.2

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 }
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‖
neg : ∀ (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‖

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
⊢ norm (E := ℝ) (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w) = ‖x.1 w‖

Tactic:
simp [hw]
-- 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
⊢ norm (E := ℝ) (((negAt s : (a : mixedSpace K) → mixedSpace K) x).1 w) = ‖x.1 w‖

Tactic:
simp [hw]
-- 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
⊢ MeasurePreserving (α := mixedSpace K) (β := mixedSpace K) (⇑(negAt s) : (a : mixedSpace K) → mixedSpace K)
    (volume : Measure (mixedSpace K)) (volume : Measure (mixedSpace K))

Tactic:
MeasurePreserving.prod (volume_preserving_pi fun w ↦ ?_) (MeasurePreserving.id _)

Premises used: MeasureTheory.volume_preserving_pi, MeasureTheory.MeasurePreserving.prod, Prod.map, 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
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
⊢ MeasurePreserving (α := mixedSpace K) (β := mixedSpace K) (⇑(negAt s) : (a : mixedSpace K) → mixedSpace K)
    (volume : Measure (mixedSpace K)) (volume : Measure (mixedSpace K))

Tactic:
refine MeasurePreserving.prod (volume_preserving_pi fun w ↦ ?_) (MeasurePreserving.id _)

Premises used: MeasureTheory.volume_preserving_pi, MeasureTheory.MeasurePreserving.prod, MeasureTheory.MeasurePreserving.id