awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : IsTotallyReal K
⊢ IsTotallyReal.{u_2} ↥⊤

Tactic:
isTotallyReal_top_iff.mpr ‹_›

Premises used: Iff.mpr, NumberField.isTotallyReal_top_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
⊢ IsTotallyReal.{u_2} ↥⊥

Tactic:
IsTotallyReal.ofRingEquiv (IntermediateField.botEquiv ℚ K).symm.toRingEquiv

Premises used: AlgEquiv.symm, Rat, AlgEquiv.toRingEquiv, NumberField.IsTotallyReal.ofRingEquiv, IntermediateField.botEquiv
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
rw : IsTotallyReal.{u_2} ↥(RingHom.fieldRange (algebraMap ℚ K))
⊢ IsTotallyReal.{u_2} ↥⊥

Tactic:
rw [Subfield.bot_eq_of_charZero]

Premises used: Subfield.bot_eq_of_charZero
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
⊢ IsTotallyReal.{u_2} ↥(RingHom.fieldRange (algebraMap ℚ K))

Tactic:
IsTotallyReal.ofRingEquiv (algebraMap ℚ K).rangeRestrictFieldEquiv

Premises used: Algebra.algebraMap, Rat, RingHom.rangeRestrictFieldEquiv, NumberField.IsTotallyReal.ofRingEquiv
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
⊢ IsTotallyReal.{u_2} ↥(RingHom.fieldRange (algebraMap ℚ K))

Tactic:
exact IsTotallyReal.ofRingEquiv (algebraMap ℚ K).rangeRestrictFieldEquiv

Premises used: Algebra.algebraMap, Rat, RingHom.rangeRestrictFieldEquiv, NumberField.IsTotallyReal.ofRingEquiv
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
a b : K
hx :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} a
hy :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} b
x : K →+* ℂ
rw :
  star (HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₁ :
  HMul.hMul (α := ℂ) (β := ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) (star ((x : (a : K) → ℂ) a) : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₂ :
  HMul.hMul (α := ℂ) (β := ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) ((x : (a : K) → ℂ) a : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₃ :
  HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) b : ℂ) ((x : (a : K) → ℂ) a : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₄ rw₅ :
  HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
⊢ Eq (α := ℂ) (star ((x : (a : K) → ℂ) (a * b)) : ℂ) ((x : (a : K) → ℂ) (a * b) : ℂ)

Tactic:
rw [map_mul, star_mul, hx, hy, mul_comm]

Premises used: map_mul, mul_comm, StarMul.star_mul
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
⊢ Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
a b : K
hx :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} a
hy :
  Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} b
x : K →+* ℂ
rw :
  star (HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₁ :
  HAdd.hAdd (α := ℂ) (β := ℂ) (star ((x : (a : K) → ℂ) a) : ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₂ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) (star ((x : (a : K) → ℂ) b) : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
rw₃ rw₄ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((x : (a : K) → ℂ) a : ℂ) ((x : (a : K) → ℂ) b : ℂ)
⊢ Eq (α := ℂ) (star ((x : (a : K) → ℂ) (a + b)) : ℂ) ((x : (a : K) → ℂ) (a + b) : ℂ)

Tactic:
rw [map_add, star_add, hx, hy]

Premises used: StarAddMonoid.star_add, map_add
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
⊢ Membership.mem (γ := Set K)
    {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
⊢ ∀ {x : K},
    Membership.mem (γ := Set K)
        {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} x →
      Membership.mem (γ := Set K)
        {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} (-x)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
⊢ ∀ (x : K),
    Membership.mem (γ := Set K)
        {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} x →
      Membership.mem (γ := Set K)
        {x : K | ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)} x⁻¹

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
x : K
⊢ Membership.mem (γ := Subfield K) (maximalRealSubfield K) x ↔
    ∀ (φ : K →+* ℂ), Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
E : Subfield K
inst_1 : IsTotallyReal.{u_2} ↥E
x : K
hx : x ∈ E
φ : K →+* ℂ
⊢ Eq (α := ℂ) ((φ : (a : K) → ℂ) x : ℂ)
    ((φ.comp E.subtype : (a : ↥E) → ℂ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) x hx) : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
E : Subfield K
inst_1 : IsTotallyReal.{u_2} ↥E
x : K
hx : x ∈ E
φ : K →+* ℂ
rw :
  Eq (α := ℂ) ((conjugate (φ.comp E.subtype) : (a : ↥E) → ℂ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) x hx) : ℂ)
    ((φ.comp E.subtype : (a : ↥E) → ℂ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) x hx) : ℂ)
⊢ Eq (α := ℂ) (star ((φ : (a : K) → ℂ) x) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)

Tactic:
rw [show φ x = (φ.comp E.subtype) ⟨x, hx⟩ by simp, RCLike.star_def, ← conjugate_coe_eq]

Premises used: RCLike.star_def, NumberField.ComplexEmbedding.conjugate_coe_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
E : Subfield K
inst_1 : IsTotallyReal.{u_2} ↥E
x : K
hx : x ∈ E
φ : K →+* ℂ
⊢ Eq (α := ℂ) ((conjugate (φ.comp E.subtype) : (a : ↥E) → ℂ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) x hx) : ℂ)
    ((φ.comp E.subtype : (a : ↥E) → ℂ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) x hx) : ℂ)

Tactic:
RingHom.congr_fun ?_ _

Premises used: RingHom.congr_fun
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
E : Subfield K
inst_1 : IsTotallyReal.{u_2} ↥E
x : K
hx : x ∈ E
φ : K →+* ℂ
refine : conjugate (φ.comp E.subtype) = φ.comp E.subtype
⊢ Eq (α := ℂ) ((conjugate (φ.comp E.subtype) : (a : ↥E) → ℂ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) x hx) : ℂ)
    ((φ.comp E.subtype : (a : ↥E) → ℂ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) x hx) : ℂ)

Tactic:
refine RingHom.congr_fun ?_ _

Premises used: RingHom.congr_fun
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
E : Subfield K
inst_1 : IsTotallyReal.{u_2} ↥E
x : K
hx : x ∈ E
φ : K →+* ℂ
⊢ conjugate (φ.comp E.subtype) = φ.comp E.subtype

Tactic:
ComplexEmbedding.isReal_iff.mp <| isReal_mk_iff.mp <| isReal _

Premises used: NumberField.InfinitePlace.isReal_mk_iff, Iff.mp, NumberField.ComplexEmbedding.isReal_iff, NumberField.IsTotallyReal.isReal
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
E : Subfield K
inst_1 : IsTotallyReal.{u_2} ↥E
x : K
hx : x ∈ E
φ : K →+* ℂ
⊢ conjugate (φ.comp E.subtype) = φ.comp E.subtype

Tactic:
exact ComplexEmbedding.isReal_iff.mp <| isReal_mk_iff.mp <| isReal _

Premises used: NumberField.InfinitePlace.isReal_mk_iff, Iff.mp, NumberField.ComplexEmbedding.isReal_iff, NumberField.IsTotallyReal.isReal
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : IsTotallyReal K
⊢ Eq (α := Subfield K) (maximalRealSubfield K) ⊤

Tactic:
top_unique <| NumberField.IsTotallyReal.le_maximalRealSubfield _

Premises used: top_unique, NumberField.IsTotallyReal.le_maximalRealSubfield
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
k : Subfield K
⊢ Algebra.IsAlgebraic (↥k) K

Tactic:
Algebra.IsAlgebraic.tower_top k (K := ℚ) (A := K)

Premises used: Algebra.IsAlgebraic.tower_top, Membership.mem, Subtype
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
w : InfinitePlace ↥(maximalRealSubfield K)
rw : conjugate w.embedding = w.embedding
⊢ w.IsReal

Tactic:
rw [InfinitePlace.isReal_iff, ComplexEmbedding.isReal_iff]

Premises used: NumberField.InfinitePlace.isReal_iff, NumberField.ComplexEmbedding.isReal_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
w : InfinitePlace ↥(maximalRealSubfield K)
a :
  ∀ (x : ↥(maximalRealSubfield K)),
    Eq (α := ℂ) ((conjugate w.embedding : (a : ↥(maximalRealSubfield K)) → ℂ) x : ℂ)
      ((w.embedding : (a : ↥(maximalRealSubfield K)) → ℂ) x : ℂ)
⊢ conjugate w.embedding = w.embedding

Tactic:
ext x
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
w : InfinitePlace ↥(maximalRealSubfield K)
x : ↥(maximalRealSubfield K)
a :
  Eq (α := ℂ)
    (star
        ((lift K w.embedding : (a : K) → ℂ)
          ((algebraMap (↥(maximalRealSubfield K)) K : (a : ↥(maximalRealSubfield K)) → K) x : K)) :
      ℂ)
    ((lift K w.embedding : (a : K) → ℂ)
        ((algebraMap (↥(maximalRealSubfield K)) K : (a : ↥(maximalRealSubfield K)) → K) x : K) :
      ℂ)
⊢ Eq (α := ℂ) ((conjugate w.embedding : (a : ↥(maximalRealSubfield K)) → ℂ) x : ℂ)
    ((w.embedding : (a : ↥(maximalRealSubfield K)) → ℂ) x : ℂ)

Tactic:
rw [RingHom.star_apply, ← lift_algebraMap_apply K w.embedding]

Premises used: RingHom.star_apply, NumberField.InfinitePlace.embedding, NumberField.ComplexEmbedding.lift_algebraMap_apply
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
w : InfinitePlace ↥(maximalRealSubfield K)
x : ↥(maximalRealSubfield K)
⊢ Eq (α := ℂ)
    (star
        ((lift K w.embedding : (a : K) → ℂ)
          ((algebraMap (↥(maximalRealSubfield K)) K : (a : ↥(maximalRealSubfield K)) → K) x : K)) :
      ℂ)
    ((lift K w.embedding : (a : K) → ℂ)
        ((algebraMap (↥(maximalRealSubfield K)) K : (a : ↥(maximalRealSubfield K)) → K) x : K) :
      ℂ)

Tactic:
x.prop _

Premises used: Subtype.prop
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
w : InfinitePlace ↥(maximalRealSubfield K)
x : ↥(maximalRealSubfield K)
⊢ Eq (α := ℂ)
    (star
        ((lift K w.embedding : (a : K) → ℂ)
          ((algebraMap (↥(maximalRealSubfield K)) K : (a : ↥(maximalRealSubfield K)) → K) x : K)) :
      ℂ)
    ((lift K w.embedding : (a : K) → ℂ)
        ((algebraMap (↥(maximalRealSubfield K)) K : (a : ↥(maximalRealSubfield K)) → K) x : K) :
      ℂ)

Tactic:
exact x.prop _

Premises used: Subtype.prop
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsAlgebraic ℚ K
E : Subfield K
⊢ IsTotallyReal.{u_2} ↥E ↔ E ≤ maximalRealSubfield K

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

Premises used: Iff.intro, NumberField.IsTotallyReal.le_maximalRealSubfield
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsAlgebraic ℚ K
E : Subfield K
refine : ∀ (h : E ≤ maximalRealSubfield K), IsTotallyReal.{u_2} ↥E
⊢ IsTotallyReal.{u_2} ↥E ↔ E ≤ maximalRealSubfield K

Tactic:
refine ⟨fun h ↦ h.le_maximalRealSubfield, fun h ↦ ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsAlgebraic ℚ K
E : Subfield K
h : E ≤ maximalRealSubfield K
x : Algebra ↥E ↥(maximalRealSubfield K) := (Subfield.inclusion h).toAlgebra
⊢ IsScalarTower (↥E) (↥(maximalRealSubfield K)) K

Tactic:
have : IsScalarTower E (maximalRealSubfield K) K := IsScalarTower.of_algebraMap_eq' rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsAlgebraic ℚ K
E : Subfield K
h : E ≤ maximalRealSubfield K
x : Algebra ↥E ↥(maximalRealSubfield K) := (Subfield.inclusion h).toAlgebra
this : IsScalarTower (↥E) (↥(maximalRealSubfield K)) K
⊢ Algebra.IsAlgebraic.{u_2, u_2} ↥E ↥(maximalRealSubfield K)

Tactic:
have : Algebra.IsAlgebraic E (maximalRealSubfield K) :=
      Algebra.IsAlgebraic.tower_bot E (maximalRealSubfield K) K
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsAlgebraic ℚ K
E : Subfield K
h : E ≤ maximalRealSubfield K
x : Algebra ↥E ↥(maximalRealSubfield K) := (Subfield.inclusion h).toAlgebra
this_1 : IsScalarTower (↥E) (↥(maximalRealSubfield K)) K
this : Algebra.IsAlgebraic.{u_2, u_2} ↥E ↥(maximalRealSubfield K)
⊢ IsTotallyReal.{u_2} ↥E

Tactic:
IsTotallyReal.of_algebra _ (maximalRealSubfield K)

Premises used: NumberField.maximalRealSubfield, NumberField.IsTotallyReal.of_algebra, Membership.mem, Subtype
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsAlgebraic ℚ K
E : Subfield K
h : E ≤ maximalRealSubfield K
x : Algebra ↥E ↥(maximalRealSubfield K) := (Subfield.inclusion h).toAlgebra
this_1 : IsScalarTower (↥E) (↥(maximalRealSubfield K)) K
this : Algebra.IsAlgebraic.{u_2, u_2} ↥E ↥(maximalRealSubfield K)
⊢ IsTotallyReal.{u_2} ↥E

Tactic:
exact IsTotallyReal.of_algebra _ (maximalRealSubfield K)

Premises used: NumberField.maximalRealSubfield, NumberField.IsTotallyReal.of_algebra, Membership.mem, Subtype
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F_1 : Type u_1
inst : Field F_1
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
E F : Subfield K
hE : IsTotallyReal.{u_2} ↥E
hF : IsTotallyReal.{u_2} ↥F
rw : IsTotallyReal.{u_2} ↥E ∧ IsTotallyReal.{u_2} ↥F
⊢ IsTotallyReal.{u_2} ↥(E ⊔ F)

Tactic:
rw [isTotallyReal_iff_le_maximalRealSubfield, sup_le_iff,
    ← isTotallyReal_iff_le_maximalRealSubfield, ← isTotallyReal_iff_le_maximalRealSubfield]

Premises used: NumberField.isTotallyReal_iff_le_maximalRealSubfield, sup_le_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F_1 : Type u_1
inst : Field F_1
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
E F : Subfield K
hE : IsTotallyReal.{u_2} ↥E
hF : IsTotallyReal.{u_2} ↥F
⊢ IsTotallyReal.{u_2} ↥E ∧ IsTotallyReal.{u_2} ↥F

Tactic:
⟨hE, hF⟩

Premises used: And.intro
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F_1 : Type u_1
inst : Field F_1
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
E F : Subfield K
hE : IsTotallyReal.{u_2} ↥E
hF : IsTotallyReal.{u_2} ↥F
⊢ IsTotallyReal.{u_2} ↥E ∧ IsTotallyReal.{u_2} ↥F

Tactic:
exact ⟨hE, hF⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst_4 : ∀ (i : ι), IsTotallyReal.{u_2} ↥(k i)
inl : ∀ (hι : IsEmpty ι), IsTotallyReal.{u_2} ↥(⨆ (i : ι), k i)
inr : ∀ (i : ι), IsTotallyReal.{u_2} ↥(⨆ (i : ι), k i)
⊢ IsTotallyReal.{u_2} ↥(⨆ (i : ι), k i)

Tactic:
obtain hι | ⟨⟨i⟩⟩ := isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst_4 : ∀ (i : ι), IsTotallyReal.{u_2} ↥(k i)
hι : IsEmpty ι
inl : IsTotallyReal.{u_2} ↥⊥
⊢ IsTotallyReal.{u_2} ↥(⨆ (i : ι), k i)

Tactic:
rw [iSup_of_empty]

Premises used: iSup_of_empty
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst_4 : ∀ (i : ι), IsTotallyReal.{u_2} ↥(k i)
hι : IsEmpty ι
⊢ IsTotallyReal.{u_2} ↥⊥

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst_4 : ∀ (i : ι), IsTotallyReal.{u_2} ↥(k i)
i : ι
inr : ∀ (i : ι), k i ≤ maximalRealSubfield K
⊢ IsTotallyReal.{u_2} ↥(⨆ (i : ι), k i)

Tactic:
rw [isTotallyReal_iff_le_maximalRealSubfield, iSup_le_iff]

Premises used: NumberField.isTotallyReal_iff_le_maximalRealSubfield, iSup_le_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst_4 : ∀ (i : ι), IsTotallyReal.{u_2} ↥(k i)
i : ι
⊢ ∀ (i : ι), k i ≤ maximalRealSubfield K

Tactic:
fun i ↦ IsTotallyReal.le_maximalRealSubfield (k i)

Premises used: NumberField.IsTotallyReal.le_maximalRealSubfield
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst_4 : ∀ (i : ι), IsTotallyReal.{u_2} ↥(k i)
i : ι
⊢ ∀ (i : ι), k i ≤ maximalRealSubfield K

Tactic:
exact fun i ↦ IsTotallyReal.le_maximalRealSubfield (k i)

Premises used: NumberField.IsTotallyReal.le_maximalRealSubfield
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsAlgebraic ℚ K
h : Eq (α := Subfield K) (maximalRealSubfield K) ⊤
⊢ Algebra.IsIntegral (↥⊤) K

Tactic:
have : Algebra.IsIntegral (⊤ : Subfield K) K := Algebra.IsIntegral.tower_top ℚ
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsAlgebraic ℚ K
h : Eq (α := Subfield K) (maximalRealSubfield K) ⊤
this : Algebra.IsIntegral (↥⊤) K
rw : IsTotallyReal.{u_2} ↥⊤
rw₁ : LE.le (α := Subfield K) ⊤ (maximalRealSubfield K)
rw₂ rw₃ : LE.le.{u_2} (α := Subfield K) ⊤ ⊤
⊢ IsTotallyReal K

Tactic:
rw [← isTotallyReal_top_iff, isTotallyReal_iff_le_maximalRealSubfield, h]

Premises used: NumberField.isTotallyReal_top_iff, NumberField.isTotallyReal_iff_le_maximalRealSubfield
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : NumberField K
⊢ nrRealPlaces K = 0 ↔ IsTotallyComplex K

Tactic:
simp [Fintype.card_eq_zero_iff, isEmpty_subtype, isTotallyComplex_iff]

Premises used: NumberField.isTotallyComplex_iff, Fintype.card_eq_zero_iff, isEmpty_subtype
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : IsTotallyComplex K
φ : K →+* ℂ
⊢ ¬ComplexEmbedding.IsReal φ

Tactic:
isReal_mk_iff.not.mp <| not_isReal_iff_isComplex.mpr <| isComplex (InfinitePlace.mk φ)

Premises used: Iff.mpr, Iff.not, NumberField.InfinitePlace.mk, NumberField.InfinitePlace.isReal_mk_iff, NumberField.IsTotallyComplex.isComplex, Iff.mp, NumberField.InfinitePlace.not_isReal_iff_isComplex
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : IsTotallyComplex K
w : InfinitePlace K
⊢ w.mult = 2

Tactic:
mult_isComplex ⟨w, isComplex w⟩

Premises used: NumberField.InfinitePlace.mult_isComplex, NumberField.IsTotallyComplex.isComplex, Subtype.mk
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : NumberField K
h : IsTotallyComplex K
⊢ nrRealPlaces K = 0

Tactic:
nrRealPlaces_eq_zero_iff.mpr h

Premises used: Iff.mpr, NumberField.nrRealPlaces_eq_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Goal:
K : Type u_2
inst : Field K
inst_1 : NumberField K
h : IsTotallyComplex K
rw : nrRealPlaces K + 2 * nrComplexPlaces K = 2 * nrComplexPlaces K
rw₁ : 0 + 2 * nrComplexPlaces K = 2 * nrComplexPlaces K
rw₂ rw₃ : 2 * nrComplexPlaces K = 2 * nrComplexPlaces K
⊢ finrank ℚ K = 2 * nrComplexPlaces K

Tactic:
rw [← card_add_two_mul_card_eq_rank, nrRealPlaces_eq_zero_iff.mpr h, zero_add]

Premises used: Iff.mpr, NumberField.nrRealPlaces_eq_zero_iff, zero_add, NumberField.InfinitePlace.card_add_two_mul_card_eq_rank
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
⊢ Eq (α := ℚ) ((↑((norm ℤ : (a : 𝓞 K) → ℤ) x) : ℚ) : ℚ) ((norm ℚ : (a : K) → ℚ) (↑x : K) : ℚ)

Tactic:
(Algebra.norm_localization (R := ℤ) (Rₘ := ℚ) (S := 𝓞 K) (Sₘ := K) (nonZeroDivisors ℤ) x).symm

Premises used: Algebra.norm_localization, nonZeroDivisors, Int, Eq.symm, Rat.ofInt
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
⊢ Eq (α := ℚ) ((↑((trace ℤ (𝓞 K) : (a : 𝓞 K) → ℤ) x) : ℚ) : ℚ) ((trace ℚ K : (a : K) → ℚ) (↑x : K) : ℚ)

Tactic:
(Algebra.trace_localization (R := ℤ) (Rₘ := ℚ) (S := 𝓞 K) (Sₘ := K) (nonZeroDivisors ℤ) x).symm

Premises used: nonZeroDivisors, Int, Algebra.trace_localization, Eq.symm, Rat.ofInt
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
L : Type u_1
K : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : 𝓞 L
⊢ Eq.{u_2 + 1} (α := K) ((↑((norm K : (a : 𝓞 L) → 𝓞 K) x) : K) : K) ((Algebra.norm K : (a : L) → K) (↑x : L) : K)

Tactic:
rfl

Premises used: rfl