awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
refine_2 : LE.le (α := ℝ) (↑|coeff (minpoly ℤ x) i| : ℝ) (↑(↑C : ℤ) : ℝ)
⊢ Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (coeff (minpoly ℤ x) i)

Tactic:
rw [mem_Icc, ← abs_le, ← @Int.cast_le ℝ]

Premises used: Int.cast_le, abs_le, Set.mem_Icc
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
⊢ LE.le (α := ℝ) (↑|coeff (minpoly ℤ x) i| : ℝ) (↑(↑C : ℤ) : ℝ)

Tactic:
(Eq.trans_le ?_ <| coeff_bdd_of_norm_le hx.2 i).trans (Nat.le_ceil _)

Premises used: Eq.trans_le, And.right, NumberField.Embeddings.coeff_bdd_of_norm_le, Nat.le_ceil, LE.le.trans
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
refine_2 : (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖coeff (minpoly ℚ x) i‖
⊢ LE.le (α := ℝ) (↑|coeff (minpoly ℤ x) i| : ℝ) (↑(↑C : ℤ) : ℝ)

Tactic:
refine (Eq.trans_le ?_ <| coeff_bdd_of_norm_le hx.2 i).trans (Nat.le_ceil _)

Premises used: Eq.trans_le, And.right, NumberField.Embeddings.coeff_bdd_of_norm_le, Nat.le_ceil, LE.le.trans
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
refine_2 : (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖(map (algebraMap ℤ ℚ) (minpoly ℤ x)).coeff i‖
refine_2₁ : (↑|coeff (minpoly ℤ x) i| : ℝ) = norm (E := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (coeff (minpoly ℤ x) i) : ℚ)
refine_2₂ : (↑|coeff (minpoly ℤ x) i| : ℝ) = norm (E := ℚ) (↑(coeff (minpoly ℤ x) i) : ℚ)
refine_2₃ : (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖coeff (minpoly ℤ x) i‖
refine_2₄ : Eq (α := ℝ) (↑|coeff (minpoly ℤ x) i| : ℝ) |(↑(coeff (minpoly ℤ x) i) : ℝ)|
refine_2₅ refine_2₆ : Eq (α := ℝ) |(↑(coeff (minpoly ℤ x) i) : ℝ)| |(↑(coeff (minpoly ℤ x) i) : ℝ)|
⊢ (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖coeff (minpoly ℚ x) i‖

Tactic:
rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]

Premises used: Int.cast_abs, Polynomial.coeff_map, Int.norm_eq_abs, eq_intCast, Int.norm_cast_rat
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
a : ℕ
h : Membership.mem (γ := Set ℕ) univ a
φ : K →+* A
⊢ norm.{u_2} (E := A) ((φ : (a : K) → A) ((fun (x_1 : ℕ) ↦ x ^ x_1) a) : A) ≤ 1

Tactic:
simp [pow_le_one₀ (norm_nonneg (φ x)) <| hx φ]

Premises used: DFunLike.coe, norm_nonneg, pow_le_one₀
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
obtain : ∀ (a b : ℕ) (habne : a ≠ b) (h : x ^ a = x ^ b), ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1
⊢ ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1

Tactic:
obtain ⟨a, -, b, -, habne, h⟩ :=
    Set.Infinite.exists_ne_map_eq_of_mapsTo (f := (x ^ · : ℕ → K)) Set.infinite_univ
      (fun a _ => mem_setOf.mpr <|
        ⟨hxi.pow a, fun φ => by simp [pow_le_one₀ (norm_nonneg (φ x)) <| hx φ]⟩)
      (finite_of_norm_le K A (1 : ℝ))

Premises used: Iff.mpr, Set.mem_setOf, Set.infinite_univ, NumberField.Embeddings.finite_of_norm_le, OfNat.ofNat, Set.Infinite.exists_ne_map_eq_of_mapsTo
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
inr :
  ∀
    (this :
      ∀ (K : Type u_1) [inst : Field K] [NumberField K] (A : Type u_2) [inst_6 : NormedField A] [IsAlgClosed A]
        [NormedAlgebra ℚ A] {x : K} (hx₀ : x ≠ 0) (hxi : IsIntegral ℤ x)
        (hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1) (a b : ℕ) (habne : a ≠ b)
        (h : x ^ a = x ^ b) (hlt : b < a), ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1)
    (hlt : ¬b < a), ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1
wlog :
  ∀ (K : Type u_1) [inst : Field K] [NumberField K] (A : Type u_2) [inst_6 : NormedField A] [IsAlgClosed A]
    [NormedAlgebra ℚ A] {x : K} (hx₀ : x ≠ 0) (hxi : IsIntegral ℤ x)
    (hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1) (a b : ℕ) (habne : a ≠ b)
    (h : x ^ a = x ^ b) (hlt : b < a), ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1
⊢ ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1

Tactic:
wlog hlt : b < a
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
this :
  ∀ (K : Type u_1) [inst : Field K] [NumberField K] (A : Type u_2) [inst_6 : NormedField A] [IsAlgClosed A]
    [NormedAlgebra ℚ A] {x : K} (hx₀ : x ≠ 0) (hxi : IsIntegral ℤ x)
    (hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1) (a b : ℕ) (habne : a ≠ b)
    (h : x ^ a = x ^ b) (hlt : b < a), ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1
hlt : ¬b < a
⊢ ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1

Tactic:
this K A hx₀ hxi hx b a habne.symm h.symm (habne.lt_or_gt.resolve_right hlt)

Premises used: Ne.symm, Or.resolve_right, Eq.symm, Ne.lt_or_gt
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
this :
  ∀ (K : Type u_1) [inst : Field K] [NumberField K] (A : Type u_2) [inst_6 : NormedField A] [IsAlgClosed A]
    [NormedAlgebra ℚ A] {x : K} (hx₀ : x ≠ 0) (hxi : IsIntegral ℤ x)
    (hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1) (a b : ℕ) (habne : a ≠ b)
    (h : x ^ a = x ^ b) (hlt : b < a), ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1
hlt : ¬b < a
⊢ ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1

Tactic:
exact this K A hx₀ hxi hx b a habne.symm h.symm (habne.lt_or_gt.resolve_right hlt)

Premises used: Ne.symm, Or.resolve_right, Eq.symm, Ne.lt_or_gt
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K_1 : Type u_1
inst : Field K_1
A_1 : Type u_2
inst_1 : NormedField A_1
K : Type u_1
inst_2 : Field K
inst_3 : NumberField K
A : Type u_2
inst_4 : NormedField A
inst_5 : IsAlgClosed A
inst_6 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
hlt : b < a
⊢ ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1

Tactic:
⟨a - b, tsub_pos_of_lt hlt, ?_⟩

Premises used: HSub.hSub, Exists.intro, tsub_pos_of_lt
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K_1 : Type u_1
inst : Field K_1
A_1 : Type u_2
inst_1 : NormedField A_1
K : Type u_1
inst_2 : Field K
inst_3 : NumberField K
A : Type u_2
inst_4 : NormedField A
inst_5 : IsAlgClosed A
inst_6 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
hlt : b < a
refine : x ^ (a - b) = 1
⊢ ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1

Tactic:
refine ⟨a - b, tsub_pos_of_lt hlt, ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K_1 : Type u_1
inst : Field K_1
A_1 : Type u_2
inst_1 : NormedField A_1
K : Type u_1
inst_2 : Field K
inst_3 : NumberField K
A : Type u_2
inst_4 : NormedField A
inst_5 : IsAlgClosed A
inst_6 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
hlt : b < a
⊢ x ^ (a - b) = 1 ∨ x ^ b = 0

Tactic:
rw [← Nat.sub_add_cancel hlt.le, pow_add, mul_left_eq_self₀] at h

Premises used: pow_add, LT.lt.le, mul_left_eq_self₀, Nat.sub_add_cancel
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K_1 : Type u_1
inst : Field K_1
A_1 : Type u_2
inst_1 : NormedField A_1
K : Type u_1
inst_2 : Field K
inst_3 : NumberField K
A : Type u_2
inst_4 : NormedField A
inst_5 : IsAlgClosed A
inst_6 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
hlt : b < a
h₁ : x ^ (a - b) = 1 ∨ x ^ b = 0
⊢ b < a

Tactic:
rw [← Nat.sub_add_cancel hlt.le, pow_add, mul_left_eq_self₀] at h

Premises used: pow_add, LT.lt.le, mul_left_eq_self₀, Nat.sub_add_cancel
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K_1 : Type u_1
inst : Field K_1
A_1 : Type u_2
inst_1 : NormedField A_1
K : Type u_1
inst_2 : Field K
inst_3 : NumberField K
A : Type u_2
inst_4 : NormedField A
inst_5 : IsAlgClosed A
inst_6 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
⊢ x ^ (a - b) = 1

Tactic:
h.resolve_right fun hp ↦ hx₀ (eq_zero_of_pow_eq_zero hp)

Premises used: eq_zero_of_pow_eq_zero, Or.resolve_right
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K_1 : Type u_1
inst : Field K_1
A_1 : Type u_2
inst_1 : NormedField A_1
K : Type u_1
inst_2 : Field K
inst_3 : NumberField K
A : Type u_2
inst_4 : NormedField A
inst_5 : IsAlgClosed A
inst_6 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
⊢ x ^ (a - b) = 1

Tactic:
refine h.resolve_right fun hp ↦ hx₀ (eq_zero_of_pow_eq_zero hp)

Premises used: eq_zero_of_pow_eq_zero, Or.resolve_right
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) = 1
apply : x ≠ 0
⊢ ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1

Tactic:
apply pow_eq_one_of_norm_le_one K A _ hxi fun φ ↦ le_of_eq <| hx φ

Premises used: NumberField.Embeddings.pow_eq_one_of_norm_le_one, le_of_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
hxi : IsIntegral.{0, u_1} ℤ (A := K) 0
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) 0 : A) = 1
⊢ ∀ (φ : K →+* A), False

Tactic:
simp_rw [map_zero, norm_zero, zero_ne_one] at hx

Premises used: norm_zero, map_zero, zero_ne_one
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
hxi : IsIntegral.{0, u_1} ℤ (A := K) 0
hx : ∀ (φ : K →+* A), False
⊢ False

Tactic:
hx (IsAlgClosed.lift (R := ℚ)).toRingHom

Premises used: IsAlgClosed.lift, AlgHom.toRingHom
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
hxi : IsIntegral.{0, u_1} ℤ (A := K) 0
hx : ∀ (φ : K →+* A), False
⊢ False

Tactic:
exact hx (IsAlgClosed.lift (R := ℚ)).toRingHom

Premises used: IsAlgClosed.lift, AlgHom.toRingHom
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
A : Type u_2
inst_1 : NormedDivisionRing A
inst_2 : Nontrivial A
φ : K →+* A
x : K
⊢ (place φ : (a : K) → ℝ) x = norm.{u_2} (E := A) ((φ : (a : K) → A) x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
φ : k →+* ℂ
this : Algebra k ℂ := φ.toAlgebra
⊢ K →+* ℂ

Tactic:
exact (IsAlgClosed.lift (R := k)).toRingHom

Premises used: IsAlgClosed.lift, AlgHom.toRingHom
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
φ : k →+* ℂ
this : Algebra k ℂ := φ.toAlgebra
rw : @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑IsAlgClosed.lift : K →+* ℂ) (algebraMap k K) = φ
rw₁ : algebraMap k ℂ = φ
rw₂ rw₃ : φ = φ
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (AlgHom.toRingHom.{u_2, u_1, 0} (R := k) IsAlgClosed.lift)
      (algebraMap k K) =
    φ

Tactic:
rw [AlgHom.toRingHom_eq_coe, AlgHom.comp_algebraMap_of_tower, RingHom.algebraMap_toAlgebra']

Premises used: RingHom.algebraMap_toAlgebra', AlgHom.comp_algebraMap_of_tower, AlgHom.toRingHom_eq_coe
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
φ : k →+* ℂ
x : k
⊢ Eq (α := ℂ) ((lift K φ : (a : K) → ℂ) ((algebraMap k K : (a : k) → K) x : K) : ℂ) ((φ : (a : k) → ℂ) x : ℂ)

Tactic:
RingHom.congr_fun (lift_comp_algebraMap K φ) x

Premises used: RingHom.congr_fun, NumberField.ComplexEmbedding.lift_comp_algebraMap
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
φ : K →+* ℂ
σ : k →+* K
⊢ (conjugate φ).comp σ = conjugate (φ.comp σ)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, starRingEnd, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
x : K →+* ℂ
⊢ conjugate (conjugate x) = x

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
x : K
⊢ Eq (α := ℂ) ((conjugate φ : (a : K) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
a : ∀ (x : K), Eq (α := ℝ) ((place (conjugate φ) : (a : K) → ℝ) x : ℝ) ((place φ : (a : K) → ℝ) x : ℝ)
⊢ place (conjugate φ) = place φ

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
x : K
⊢ Eq (α := ℝ) ((place (conjugate φ) : (a : K) → ℝ) x : ℝ) ((place φ : (a : K) → ℝ) x : ℝ)

Tactic:
simp only [place_apply, norm_conj, conjugate_coe_eq]

Premises used: Complex.norm_conj, NumberField.place_apply, NumberField.ComplexEmbedding.conjugate_coe_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
⊢ IsReal φ ↔ conjugate φ = φ

Tactic:
isSelfAdjoint_iff

Premises used: isSelfAdjoint_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
⊢ IsReal (conjugate φ) ↔ IsReal φ

Tactic:
IsSelfAdjoint.star_iff

Premises used: IsSelfAdjoint.star_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
φ : K →+* ℂ
hφ : IsReal φ
⊢ re ((φ : (a : K) → ℂ) 1) = 1

Tactic:
simp only [map_one, one_re]

Premises used: map_one, Complex.one_re
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
φ : K →+* ℂ
hφ : IsReal φ
⊢ ∀ (x y : K), re ((φ : (a : K) → ℂ) (x * y)) = re ((φ : (a : K) → ℂ) x) * re ((φ : (a : K) → ℂ) y)

Tactic:
simp only [Complex.conj_eq_iff_im.mp (RingHom.congr_fun hφ _), map_mul, mul_re,
      mul_zero, tsub_zero, forall_const]

Premises used: Complex.mul_re, RingHom.congr_fun, MulZeroClass.mul_zero, tsub_zero, map_mul, Iff.mp, Complex.conj_eq_iff_im, forall_const
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
φ : K →+* ℂ
hφ : IsReal φ
⊢ re ((φ : (a : K) → ℂ) 0) = 0

Tactic:
simp only [map_zero, zero_re]

Premises used: map_zero, Complex.zero_re
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
φ : K →+* ℂ
hφ : IsReal φ
⊢ ∀ (x y : K), re ((φ : (a : K) → ℂ) (x + y)) = re ((φ : (a : K) → ℂ) x) + re ((φ : (a : K) → ℂ) y)

Tactic:
simp only [map_add, add_re, forall_const]

Premises used: Complex.add_re, map_add, forall_const
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
a : (↑((hφ.embedding : (a : K) → ℝ) x) : ℂ).re = re ((φ : (a : K) → ℂ) x)
a₁ : (↑((hφ.embedding : (a : K) → ℝ) x) : ℂ).im = im ((φ : (a : K) → ℂ) x)
⊢ (↑((hφ.embedding : (a : K) → ℝ) x) : ℂ) = (φ : (a : K) → ℂ) x

Tactic:
apply Complex.ext

Premises used: Complex.ext
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (↑((hφ.embedding : (a : K) → ℝ) x) : ℂ).re = re ((φ : (a : K) → ℂ) x)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
a : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)
⊢ (↑((hφ.embedding : (a : K) → ℝ) x) : ℂ).im = im ((φ : (a : K) → ℂ) x)

Tactic:
rw [ofReal_im, eq_comm, ← Complex.conj_eq_iff_im]

Premises used: eq_comm, Complex.conj_eq_iff_im, Complex.ofReal_im
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)

Tactic:
RingHom.congr_fun hφ x

Premises used: RingHom.congr_fun
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ) ((φ : (a : K) → ℂ) x : ℂ)

Tactic:
exact RingHom.congr_fun hφ x

Premises used: RingHom.congr_fun
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
f : k →+* K
φ : K →+* ℂ
hφ : IsReal φ
a : ∀ (x : k), Eq (α := ℂ) ((star (φ.comp f) : (a : k) → ℂ) x : ℂ) ((φ.comp f : (a : k) → ℂ) x : ℂ)
⊢ IsReal (φ.comp f)

Tactic:
ext1 x
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
f : k →+* K
φ : K →+* ℂ
hφ : IsReal φ
x : k
⊢ Eq (α := ℂ) ((star (φ.comp f) : (a : k) → ℂ) x : ℂ) ((φ.comp f : (a : k) → ℂ) x : ℂ)

Tactic:
simpa using RingHom.congr_fun hφ (f x)

Premises used: RingHom.congr_fun, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp (↑f : k →+* K))
⊢ IsReal (RingHom.comp (φ.comp (↑f : k →+* K)) f.symm.toRingHom)

Tactic:
H.comp f.symm.toRingHom

Premises used: NumberField.ComplexEmbedding.IsReal.comp, RingEquiv.toRingHom, RingEquiv.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp (↑f : k →+* K))
h : φ = RingHom.comp (φ.comp (↑f : k →+* K)) f.symm.toRingHom
⊢ IsReal φ

Tactic:
convert! H.comp f.symm.toRingHom

Premises used: NumberField.ComplexEmbedding.IsReal.comp, RingEquiv.toRingHom, RingEquiv.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp (↑f : k →+* K))
h :
  ∀ (x : K),
    Eq (α := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ((RingHom.comp (φ.comp (↑f : k →+* K)) f.symm.toRingHom : (a : K) → ℂ) x : ℂ)
⊢ φ = RingHom.comp (φ.comp (↑f : k →+* K)) f.symm.toRingHom

Tactic:
ext1
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
f : k ≃+* K
φ : K →+* ℂ
H : IsReal (φ.comp (↑f : k →+* K))
x : K
⊢ Eq (α := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ((RingHom.comp (φ.comp (↑f : k →+* K)) f.symm.toRingHom : (a : K) → ℂ) x : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
inst_3 : IsGalois k K
φ ψ : K →+* ℂ
h : Eq (α := k →+* ℂ) (φ.comp (algebraMap k K)) (ψ.comp (algebraMap k K))
this_1 : Algebra k ℂ := RingHom.toAlgebra (φ.comp (algebraMap k K))
this : Algebra K ℂ := φ.toAlgebra
⊢ IsScalarTower k K ℂ

Tactic:
have : IsScalarTower k K ℂ := IsScalarTower.of_algebraMap_eq' rfl