awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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:
refine Set.disjoint_left.mpr fun _ hx hx' ↦ ?_

Premises used: Iff.mpr, Set.disjoint_left
-- 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
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
⊢ ∃ (w : { w : InfinitePlace K // w.IsReal }), w ∈ s ∧ w ∉ t ∨ w ∈ t ∧ w ∉ s

Tactic:
Set.symmDiff_nonempty.mpr hst

Premises used: Iff.mpr, Set.union, Set.Mem, Set.diff, setOf, Set.Nonempty, Set.symmDiff_nonempty, symmDiff
-- 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
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
inr : ∀ (w : { w : InfinitePlace K // w.IsReal }) (hw : w ∈ t ∧ w ∉ s), False
⊢ False

Tactic:
obtain ⟨w, hw | hw⟩ : ∃ w, (w ∈ s ∧ w ∉ t) ∨ (w ∈ t ∧ w ∉ s) := Set.symmDiff_nonempty.mpr hst

Premises used: Iff.mpr, Set.symmDiff_nonempty
-- 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
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
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ s ∧ w ∉ t
⊢ False

Tactic:
lt_irrefl _ <|
      (neg_of_mem_negA_plusPart A hx hw.1).trans (pos_of_notMem_negAt_plusPart A hx' hw.2)

Premises used: lt_irrefl, NumberField.mixedEmbedding.neg_of_mem_negA_plusPart, And.right, And.left, LT.lt.trans, NumberField.mixedEmbedding.pos_of_notMem_negAt_plusPart
-- 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
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
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ s ∧ w ∉ t
⊢ False

Tactic:
exact lt_irrefl _ <|
      (neg_of_mem_negA_plusPart A hx hw.1).trans (pos_of_notMem_negAt_plusPart A hx' hw.2)

Premises used: lt_irrefl, NumberField.mixedEmbedding.neg_of_mem_negA_plusPart, And.right, And.left, LT.lt.trans, NumberField.mixedEmbedding.pos_of_notMem_negAt_plusPart
-- 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
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
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ t ∧ w ∉ s
⊢ False

Tactic:
lt_irrefl _ <|
      (neg_of_mem_negA_plusPart A hx' hw.1).trans (pos_of_notMem_negAt_plusPart A hx hw.2)

Premises used: lt_irrefl, NumberField.mixedEmbedding.neg_of_mem_negA_plusPart, And.right, And.left, LT.lt.trans, NumberField.mixedEmbedding.pos_of_notMem_negAt_plusPart
-- 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
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
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ t ∧ w ∉ s
⊢ False

Tactic:
exact lt_irrefl _ <|
      (neg_of_mem_negA_plusPart A hx' hw.1).trans (pos_of_notMem_negAt_plusPart A hx hw.2)

Premises used: lt_irrefl, NumberField.mixedEmbedding.neg_of_mem_negA_plusPart, And.right, And.left, LT.lt.trans, NumberField.mixedEmbedding.pos_of_notMem_negAt_plusPart
-- 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
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

Tactic:
⟨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)⟩, ?_⟩⟩

Premises used: Iff.mpr, Norm.norm, norm_pos_iff, NumberField.mixedEmbedding.negAt, _private.0.NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem.match_1, Membership.mem, Prod.mk, NumberField.mixedEmbedding.neg_of_mem_negA_plusPart, Prod.fst, And.intro, Iff.intro, Exists.intro, Iff.mp, Set.image, NumberField.mixedEmbedding.pos_of_notMem_negAt_plusPart, Prod.snd, DFunLike.coe, NumberField.mixedEmbedding.plusPart
-- 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
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
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
⊢ 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

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)⟩, ?_⟩⟩
-- 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
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
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
⊢ (negAt s : (a : mixedSpace K) → mixedSpace K) (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) = x

Tactic:
ext w
-- 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
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
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
⊢ ((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
-- 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
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 }
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:
simp [negAt_apply_isReal_and_mem _ hw, abs_of_neg (h₁ w hw)]

Premises used: abs_of_neg, 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)
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 }
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:
simp [negAt_apply_isReal_and_notMem _ hw, abs_of_pos (h₂ w hw)]

Premises used: NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem, abs_of_pos
-- 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
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.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:
rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
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
⊢ (⋃ (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

Tactic:
ext x
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
⊢ 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:
rw [Set.mem_union, Set.mem_inter_iff, Set.mem_iUnion, Set.mem_iUnion]

Premises used: Set.mem_union, Set.mem_inter_iff, Set.mem_iUnion
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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

Tactic:
⟨?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
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
⊢ ((∃ (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 ↦ ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
h : (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
⊢ Membership.mem (α := mixedSpace K) A ((negAt s : (a : mixedSpace K) → mixedSpace K) x : mixedSpace K)

Tactic:
simp_rw +singlePass [hA, negAt_apply_norm_isReal, negAt_apply_snd]

Premises used: NumberField.mixedEmbedding.negAt_apply_snd, NumberField.mixedEmbedding.negAt_apply_norm_isReal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
h h₁ h₂ h₃ : x ∈ A
⊢ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A

Tactic:
rwa [← hA]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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 : { w : InfinitePlace K // w.IsReal }),
      Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | x.1 i = 0} x
⊢ x ∈ A

Tactic:
h.left

Premises used: And.left
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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 : { w : InfinitePlace K // w.IsReal }),
      Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | x.1 i = 0} x
⊢ x ∈ A

Tactic:
exact h.left

Premises used: And.left
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
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
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
⊢ (∃ (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)

Premises used: Prod.fst, OfNat.ofNat, Eq, exists_or_forall_not
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
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:
Or.inr ⟨h, hx⟩

Premises used: And.intro, Or.inr
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
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:
exact Or.inr ⟨h, hx⟩

Premises used: Or.inr
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
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:
Or.inl ⟨signSet x,
        (mem_negAt_plusPart_of_mem A hA h hx).mpr ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩

Premises used: Iff.mpr, NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem, And.intro, Exists.intro, NumberField.mixedEmbedding.signSet, Or.inl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
hx : ∀ (a : { w : InfinitePlace K // w.IsReal }), ¬x.1 a = 0
h₁ : ∀ (w : { w : InfinitePlace K // w.IsReal }) (hw : w ∈ signSet x), x.1 w < 0
h₂ : ∀ (w : { w : InfinitePlace K // w.IsReal }) (hw : w ∉ signSet x), x.1 w > 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:
refine Or.inl ⟨signSet x,
        (mem_negAt_plusPart_of_mem A hA h hx).mpr ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩

Premises used: Or.inl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
hx : ∀ (a : { w : InfinitePlace K // w.IsReal }), ¬x.1 a = 0
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ signSet x
⊢ x.1 w < 0

Tactic:
lt_of_le_of_ne hw (hx w)

Premises used: lt_of_le_of_ne