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 }
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
⊢ 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 (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]
-- 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
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
⊢ 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.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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
⊢ ((negAt (signSet x) : (a : mixedSpace K) → mixedSpace K) x).1 w = ‖x.1 w‖
have pos : ∀ (hw : x.1 w ≤ 0), ((negAt (signSet x) : (a : mixedSpace K) → mixedSpace K) x).1 w = ‖x.1 w‖
Tactic: by_cases hw : x.1 w ≤ 0
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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‖
⊢ ((negAt (signSet x) : (a : mixedSpace K) → mixedSpace K) x).1 w = ‖x.1 w‖
have neg : ∀ (hw : ¬x.1 w ≤ 0), ((negAt (signSet x) : (a : mixedSpace K) → mixedSpace K) x).1 w = ‖x.1 w‖
Tactic: by_cases hw : x.1 w ≤ 0
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
hw : x.1 w ≤ 0
⊢ ((negAt (signSet x) : (a : mixedSpace K) → mixedSpace K) x).1 w = ‖x.1 w‖
have pos : -x.1 w = ‖x.1 w‖
Tactic: rw [negAt_apply_isReal_and_mem _ hw, Real.norm_of_nonpos hw]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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‖
⊢ ((negAt (signSet x) : (a : mixedSpace K) → mixedSpace K) x).1 w = ‖x.1 w‖
have pos₁ : -x.1 w = -x.1 w
Tactic: rw [negAt_apply_isReal_and_mem _ hw, Real.norm_of_nonpos hw]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
hw : ¬x.1 w ≤ 0
⊢ ((negAt (signSet x) : (a : mixedSpace K) → mixedSpace K) x).1 w = ‖x.1 w‖
have neg : x.1 w = ‖x.1 w‖
Tactic: rw [negAt_apply_isReal_and_notMem _ hw, Real.norm_of_nonneg (lt_of_not_ge hw).le]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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‖
⊢ ((negAt (signSet x) : (a : mixedSpace K) → mixedSpace K) x).1 w = ‖x.1 w‖
have neg₁ : x.1 w = x.1 w
Tactic: rw [negAt_apply_isReal_and_notMem _ hw, Real.norm_of_nonneg (lt_of_not_ge hw).le]
-- 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 }
A : Set (mixedSpace K)
⊢ Eq (α := Set (mixedSpace K)) ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) ⁻¹' A)
    ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' A)
have rw : Eq (α := Set (mixedSpace K)) ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) ⁻¹' A)
  ((⇑(negAt s).symm : (a : mixedSpace K) → mixedSpace K) ⁻¹' A)
Tactic: rw [ContinuousLinearEquiv.image_eq_preimage_symm, negAt_symm]
-- 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 }
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)
⊢ Eq (α := Set (mixedSpace K)) ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) ⁻¹' A)
    ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' A)
have rw₁ : 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]
-- 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 }
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
⊢ x.1 w < 0
have obtain : ∀ (y : mixedSpace K) (hy : y ∈ plusPart A), LT.lt (α := ℝ) (((negAt s : (a : mixedSpace K) → mixedSpace K) y).1 w) 0
Tactic: obtain ⟨y, hy, rfl⟩ := hx
Cleared hypotheses: x, hx
-- 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 }
A : Set (mixedSpace K)
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ LT.lt (α := ℝ) (((negAt s : (a : mixedSpace K) → mixedSpace K) y).1 w) 0
have rw : 0 < y.1 w
Tactic: rw [negAt_apply_isReal_and_mem _ hw, neg_lt_zero]
-- 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 }
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
⊢ 0 < x.1 w
have obtain : ∀ (y : mixedSpace K) (hy : y ∈ plusPart A), LT.lt (α := ℝ) 0 (((negAt s : (a : mixedSpace K) → mixedSpace K) y).1 w)
Tactic: obtain ⟨y, hy, rfl⟩ := hx
Cleared hypotheses: x, hx
-- 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 }
A : Set (mixedSpace K)
w : { w : InfinitePlace K // w.IsReal }
hw : w ∉ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ LT.lt (α := ℝ) 0 (((negAt s : (a : mixedSpace K) → mixedSpace K) y).1 w)
have rw : 0 < y.1 w
Tactic: rw [negAt_apply_isReal_and_notMem _ hw]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
have refine : ∀ (x : mixedSpace K)
  (hx :
    Membership.mem (γ := Set (mixedSpace K))
      ((fun (s : Set { w : InfinitePlace K // w.IsReal }) ↦
          ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A : Set (mixedSpace K)))
        s)
      x)
  (hx' :
    Membership.mem (γ := Set (mixedSpace K))
      ((fun (s : Set { w : InfinitePlace K // w.IsReal }) ↦
          ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A : Set (mixedSpace K)))
        t)
      x),
  False
Tactic: refine Set.disjoint_left.mpr fun _ hx hx' ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
s t : Set { w : InfinitePlace K // w.IsReal }
hst : s ≠ t
x : mixedSpace K
hx :
  Membership.mem (γ := Set (mixedSpace K))
    ((fun (s : Set { w : InfinitePlace K // w.IsReal }) ↦
        ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A : Set (mixedSpace K)))
      s)
    x
hx' :
  Membership.mem (γ := Set (mixedSpace K))
    ((fun (s : Set { w : InfinitePlace K // w.IsReal }) ↦
        ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A : Set (mixedSpace K)))
      t)
    x
⊢ False
have inl : ∀ (w : { w : InfinitePlace K // w.IsReal }) (hw : w ∈ s ∧ w ∉ t), False
Tactic: obtain ⟨w, hw | hw⟩ : ∃ w, (w ∈ s ∧ w ∉ t) ∨ (w ∈ t ∧ w ∉ s) := Set.symmDiff_nonempty.mpr hst
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
s t : Set { w : InfinitePlace K // w.IsReal }
hst : s ≠ t
x : mixedSpace K
hx :
  Membership.mem (γ := Set (mixedSpace K))
    ((fun (s : Set { w : InfinitePlace K // w.IsReal }) ↦
        ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A : Set (mixedSpace K)))
      s)
    x
hx' :
  Membership.mem (γ := Set (mixedSpace K))
    ((fun (s : Set { w : InfinitePlace K // w.IsReal }) ↦
        ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A : Set (mixedSpace K)))
      t)
    x
inl : ∀ (w : { w : InfinitePlace K // w.IsReal }) (hw : w ∈ s ∧ w ∉ t), False
⊢ False
have inr : ∀ (w : { w : InfinitePlace K // w.IsReal }) (hw : w ∈ t ∧ w ∉ s), False
Tactic: obtain ⟨w, hw | hw⟩ : ∃ w, (w ∈ s ∧ w ∉ t) ∨ (w ∈ t ∧ w ∉ s) := Set.symmDiff_nonempty.mpr hst
-- 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 }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w : InfinitePlace K // w.IsReal }), x.1 w ≠ 0
⊢ Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x ↔
    (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
have refine : ((∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0) →
  ∀ (h₁ : ∀ w ∈ s, x.1 w < 0) (h₂ : ∀ w ∉ s, x.1 w > 0),
    (negAt s : (a : mixedSpace K) → mixedSpace K) (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) = x
Tactic: refine ⟨fun hx ↦ ⟨fun _ hw ↦ neg_of_mem_negA_plusPart A hx hw,
      fun _ hw ↦ pos_of_notMem_negAt_plusPart A hx hw⟩,
      fun ⟨h₁, h₂⟩ ↦
        ⟨(fun w ↦ ‖x.1 w‖, x.2), ⟨(hA x).mp hx₁, fun w ↦ norm_pos_iff.mpr (hx₂ 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 }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w : InfinitePlace K // w.IsReal }), x.1 w ≠ 0
h : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
⊢ (negAt s : (a : mixedSpace K) → mixedSpace K) (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) = x
have fst : ∀ (w : { w : InfinitePlace K // w.IsReal }),
  ((negAt s : (a : mixedSpace K) → mixedSpace K) (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2)).1 w =
    x.1 w
Tactic: ext 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 }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w : InfinitePlace K // w.IsReal }), x.1 w ≠ 0
h : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
fst :
  ∀ (w : { w : InfinitePlace K // w.IsReal }),
    ((negAt s : (a : mixedSpace K) → mixedSpace K) (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2)).1 w =
      x.1 w
⊢ (negAt s : (a : mixedSpace K) → mixedSpace K) (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) = x
have snd : ∀ (w : { w : InfinitePlace K // w.IsComplex }),
  ((negAt s : (a : mixedSpace K) → mixedSpace K) (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2)).2 w =
    x.2 w
Tactic: ext 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 }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w : InfinitePlace K // w.IsReal }), x.1 w ≠ 0
h : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
w : { w : InfinitePlace K // w.IsReal }
⊢ ((negAt s : (a : mixedSpace K) → mixedSpace K) (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2)).1 w =
    x.1 w
have pos : ∀ (hw : w ∈ s),
  ((negAt s : (a : mixedSpace K) → mixedSpace K) (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2)).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 }
A : Set (mixedSpace K)
x : mixedSpace K
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hx₁ : x ∈ A
hx₂ : ∀ (w : { w : InfinitePlace K // w.IsReal }), x.1 w ≠ 0
h : (∀ w ∈ s, x.1 w < 0) ∧ ∀ w ∉ s, x.1 w > 0
h₁ : ∀ w ∈ s, x.1 w < 0
h₂ : ∀ w ∉ s, x.1 w > 0
w : { w : InfinitePlace K // w.IsReal }
pos :
  ∀ (hw : w ∈ s),
    ((negAt s : (a : mixedSpace K) → mixedSpace K) (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2)).1 w =
      x.1 w
⊢ ((negAt s : (a : mixedSpace K) → mixedSpace K) (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2)).1 w =
    x.1 w
have neg : ∀ (hw : w ∉ s),
  ((negAt s : (a : mixedSpace K) → mixedSpace K) (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2)).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
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
⊢ (⋃ (s : Set { w : InfinitePlace K // w.IsReal }), (⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) ∪
      A ∩ ⋃ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | x.1 w = 0} =
    A
have h : ∀ (x : mixedSpace K),
  x ∈
      (⋃ (s : Set { w : InfinitePlace K // w.IsReal }),
          (⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) ∪
        A ∩ ⋃ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | x.1 w = 0} ↔
    x ∈ A
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
⊢ x ∈
      (⋃ (s : Set { w : InfinitePlace K // w.IsReal }),
          (⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) ∪
        A ∩ ⋃ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | x.1 w = 0} ↔
    x ∈ A
have h : ((∃ (i : Set { w : InfinitePlace K // w.IsReal }),
      Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt i) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x) ∨
    x ∈ A ∧
      ∃ (i : { w : InfinitePlace K // w.IsReal }),
        Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | x.1 i = 0} x) ↔
  x ∈ A
Tactic: rw [Set.mem_union, Set.mem_inter_iff, Set.mem_iUnion, Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
⊢ ((∃ (i : Set { w : InfinitePlace K // w.IsReal }),
        Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt i) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x) ∨
      x ∈ A ∧
        ∃ (i : { w : InfinitePlace K // w.IsReal }),
          Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | x.1 i = 0} x) ↔
    x ∈ A
have h : ((∃ (i : Set { w : InfinitePlace K // w.IsReal }),
      Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt i) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x) ∨
    x ∈ A ∧
      ∃ (i : { w : InfinitePlace K // w.IsReal }),
        Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | x.1 i = 0} x) →
  x ∈ A
Tactic: refine ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h :
  ((∃ (i : Set { w : InfinitePlace K // w.IsReal }),
        Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt i) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x) ∨
      x ∈ A ∧
        ∃ (i : { w : InfinitePlace K // w.IsReal }),
          Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | x.1 i = 0} x) →
    x ∈ A
⊢ ((∃ (i : Set { w : InfinitePlace K // w.IsReal }),
        Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt i) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x) ∨
      x ∈ A ∧
        ∃ (i : { w : InfinitePlace K // w.IsReal }),
          Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | x.1 i = 0} x) ↔
    x ∈ A
have h₁ : ∀ (h : x ∈ A),
  (∃ (i : Set { w : InfinitePlace K // w.IsReal }),
      Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt i) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x) ∨
    x ∈ A ∧
      ∃ (i : { w : InfinitePlace K // w.IsReal }),
        Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | x.1 i = 0} x
Tactic: refine ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
s : Set { w : InfinitePlace K // w.IsReal }
x : mixedSpace K
hx : x ∈ A
right :
  Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | ∀ (w : { w : InfinitePlace K // w.IsReal }), 0 < x.1 w} x
⊢ Membership.mem (α := mixedSpace K) A ((negAt s : (a : mixedSpace K) → mixedSpace K) x : mixedSpace K)
have h : (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
Tactic: simp_rw +singlePass [hA, negAt_apply_norm_isReal, negAt_apply_snd]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ A
⊢ (∃ (i : Set { w : InfinitePlace K // w.IsReal }),
      Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt i) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x) ∨
    x ∈ A ∧
      ∃ (i : { w : InfinitePlace K // w.IsReal }),
        Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | x.1 i = 0} x
have h₁ : ∀ (hx : ∃ (a : { w : InfinitePlace K // w.IsReal }), x.1 a = 0),
  (∃ (i : Set { w : InfinitePlace K // w.IsReal }),
      Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt i) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x) ∨
    x ∈ A ∧
      ∃ (i : { w : InfinitePlace K // w.IsReal }),
        Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | x.1 i = 0} x
Tactic: obtain hx | hx := exists_or_forall_not (fun w ↦ x.1 w = 0)