[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : Field A
inst✝¹ : CharZero A
inst✝ : IsAlgClosed A
⊢ Fintype.card (K →+* A) = finrank ℚ K
[PROOFSTEP]
rw [Fintype.ofEquiv_card RingHom.equivRatAlgHom.symm, AlgHom.card]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : Field A
inst✝¹ : CharZero A
inst✝ : IsAlgClosed A
⊢ Nonempty (K →+* A)
[PROOFSTEP]
rw [← Fintype.card_pos_iff, NumberField.Embeddings.card K A]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : Field A
inst✝¹ : CharZero A
inst✝ : IsAlgClosed A
⊢ 0 < finrank ℚ K
[PROOFSTEP]
exact FiniteDimensional.finrank_pos
[GOAL]
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
⊢ (range fun φ => ↑φ x) = rootSet (minpoly ℚ x) A
[PROOFSTEP]
convert (NumberField.isAlgebraic K).range_eval_eq_rootSet_minpoly A x using 1
[GOAL]
case h.e'_2
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
⊢ (range fun φ => ↑φ x) = range fun ψ => ↑ψ x
[PROOFSTEP]
ext a
[GOAL]
case h.e'_2.h
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
a : (fun x => A) x
⊢ (a ∈ range fun φ => ↑φ x) ↔ a ∈ range fun ψ => ↑ψ x
[PROOFSTEP]
exact ⟨fun ⟨φ, hφ⟩ => ⟨φ.toRatAlgHom, hφ⟩, fun ⟨φ, hφ⟩ => ⟨φ.toRingHom, hφ⟩⟩
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B
i : ℕ
⊢ ‖coeff (minpoly ℚ x) i‖ ≤ max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))
[PROOFSTEP]
have hx := IsSeparable.isIntegral ℚ x
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
⊢ ‖coeff (minpoly ℚ x) i‖ ≤ max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))
[PROOFSTEP]
rw [← norm_algebraMap' A, ← coeff_map (algebraMap ℚ A)]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
⊢ ‖coeff (map (algebraMap ℚ A) (minpoly ℚ x)) i‖ ≤ max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))
[PROOFSTEP]
refine
  coeff_bdd_of_roots_le _ (minpoly.monic hx) (IsAlgClosed.splits_codomain _) (minpoly.natDegree_le x) (fun z hz => ?_) i
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : (fun x => A) (coeff (minpoly ℚ x) i)
hz : z ∈ roots (map (algebraMap ℚ A) (minpoly ℚ x))
⊢ ‖z‖ ≤ B
[PROOFSTEP]
classical
rw [← Multiset.mem_toFinset] at hz 
obtain ⟨φ, rfl⟩ := (range_eval_eq_rootSet_minpoly K A x).symm.subset hz
exact h φ
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : (fun x => A) (coeff (minpoly ℚ x) i)
hz : z ∈ roots (map (algebraMap ℚ A) (minpoly ℚ x))
⊢ ‖z‖ ≤ B
[PROOFSTEP]
rw [← Multiset.mem_toFinset] at hz 
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : (fun x => A) (coeff (minpoly ℚ x) i)
hz✝ : z ∈ roots (map (algebraMap ℚ A) (minpoly ℚ x))
hz : z ∈ Multiset.toFinset (roots (map (algebraMap ℚ A) (minpoly ℚ x)))
⊢ ‖z‖ ≤ B
[PROOFSTEP]
obtain ⟨φ, rfl⟩ := (range_eval_eq_rootSet_minpoly K A x).symm.subset hz
[GOAL]
case intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
φ : K →+* A
hz✝ : (fun φ => ↑φ x) φ ∈ roots (map (algebraMap ℚ A) (minpoly ℚ x))
hz : (fun φ => ↑φ x) φ ∈ Multiset.toFinset (roots (map (algebraMap ℚ A) (minpoly ℚ x)))
⊢ ‖(fun φ => ↑φ x) φ‖ ≤ B
[PROOFSTEP]
exact h φ
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
⊢ Set.Finite {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
[PROOFSTEP]
let C := Nat.ceil (max B 1 ^ finrank ℚ K * (finrank ℚ K).choose (finrank ℚ K / 2))
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
⊢ Set.Finite {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
[PROOFSTEP]
have := bUnion_roots_finite (algebraMap ℤ K) (finrank ℚ K) (finite_Icc (-C : ℤ) C)
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
⊢ Set.Finite {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
[PROOFSTEP]
refine this.subset fun x hx => ?_
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
⊢ x ∈
    ⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f)))
[PROOFSTEP]
simp_rw [mem_iUnion]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
⊢ ∃ i i_1, x ∈ ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) i)))
[PROOFSTEP]
have h_map_ℚ_minpoly := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hx.1
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
⊢ ∃ i i_1, x ∈ ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) i)))
[PROOFSTEP]
refine ⟨_, ⟨?_, fun i => ?_⟩, mem_rootSet.2 ⟨minpoly.ne_zero hx.1, minpoly.aeval ℤ x⟩⟩
[GOAL]
case refine_1
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
⊢ natDegree (minpoly ℤ x) ≤ finrank ℚ K
[PROOFSTEP]
rw [← (minpoly.monic hx.1).natDegree_map (algebraMap ℤ ℚ), ← h_map_ℚ_minpoly]
[GOAL]
case refine_1
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
⊢ natDegree (minpoly ℚ x) ≤ finrank ℚ K
[PROOFSTEP]
exact minpoly.natDegree_le x
[GOAL]
case refine_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
⊢ coeff (minpoly ℤ x) i ∈
    Icc (-↑⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊)
      ↑⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
[PROOFSTEP]
rw [mem_Icc, ← abs_le, ← @Int.cast_le ℝ]
[GOAL]
case refine_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
⊢ ↑|coeff (minpoly ℤ x) i| ≤ ↑↑⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
[PROOFSTEP]
refine (Eq.trans_le ?_ <| coeff_bdd_of_norm_le hx.2 i).trans (Nat.le_ceil _)
[GOAL]
case refine_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
⊢ ↑|coeff (minpoly ℤ x) i| = ‖coeff (minpoly ℚ x) i‖
[PROOFSTEP]
rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖↑φ x‖ = 1
⊢ ∃ n x_1, x ^ n = 1
[PROOFSTEP]
obtain ⟨a, -, b, -, habne, h⟩ :=
  @Set.Infinite.exists_ne_map_eq_of_mapsTo _ _ _ _ ((· ^ ·) x : ℕ → K) Set.infinite_univ
    (by exact fun a _ => ⟨hxi.pow a, fun φ => by simp [hx φ]⟩) (finite_of_norm_le K A (1 : ℝ))
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖↑φ x‖ = 1
⊢ MapsTo ((fun x x_1 => x ^ x_1) x) univ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ 1}
[PROOFSTEP]
exact fun a _ => ⟨hxi.pow a, fun φ => by simp [hx φ]⟩
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖↑φ x‖ = 1
a : ℕ
x✝ : a ∈ univ
φ : K →+* A
⊢ ‖↑φ ((fun x x_1 => x ^ x_1) x a)‖ ≤ 1
[PROOFSTEP]
simp [hx φ]
[GOAL]
case intro.intro.intro.intro.intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖↑φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : (fun x x_1 => x ^ x_1) x a = (fun x x_1 => x ^ x_1) x b
⊢ ∃ n x_1, x ^ n = 1
[PROOFSTEP]
wlog hlt : b < a
[GOAL]
case intro.intro.intro.intro.intro.inr
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖↑φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : (fun x x_1 => x ^ x_1) x a = (fun x x_1 => x ^ x_1) x b
this :
  ∀ (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},
    IsIntegral ℤ x →
      (∀ (φ : K →+* A), ‖↑φ x‖ = 1) →
        ∀ (a b : ℕ), a ≠ b → (fun x x_1 => x ^ x_1) x a = (fun x x_1 => x ^ x_1) x b → b < a → ∃ n x_1, x ^ n = 1
hlt : ¬b < a
⊢ ∃ n x_1, x ^ n = 1
[PROOFSTEP]
exact this K A hxi hx b a habne.symm h.symm (habne.lt_or_lt.resolve_right hlt)
[GOAL]
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖↑φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : (fun x x_1 => x ^ x_1) x a = (fun x x_1 => x ^ x_1) x b
hlt : b < a
⊢ ∃ n x_1, x ^ n = 1
[PROOFSTEP]
refine ⟨a - b, tsub_pos_of_lt hlt, ?_⟩
[GOAL]
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖↑φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : (fun x x_1 => x ^ x_1) x a = (fun x x_1 => x ^ x_1) x b
hlt : b < a
⊢ x ^ (a - b) = 1
[PROOFSTEP]
dsimp at h 
[GOAL]
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖↑φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
hlt : b < a
⊢ x ^ (a - b) = 1
[PROOFSTEP]
rw [← Nat.sub_add_cancel hlt.le, pow_add, mul_left_eq_self₀] at h 
[GOAL]
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖↑φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
⊢ x ^ (a - b) = 1
[PROOFSTEP]
refine h.resolve_right fun hp => ?_
[GOAL]
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖↑φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
hp : x ^ b = 0
⊢ False
[PROOFSTEP]
specialize hx (IsAlgClosed.lift (NumberField.isAlgebraic K)).toRingHom
[GOAL]
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
hp : x ^ b = 0
hx : ‖↑↑(IsAlgClosed.lift (_ : Algebra.IsAlgebraic ℚ K)) x‖ = 1
⊢ False
[PROOFSTEP]
rw [pow_eq_zero hp, map_zero, norm_zero] at hx 
[GOAL]
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
hp : x ^ b = 0
hx : 0 = 1
⊢ False
[PROOFSTEP]
norm_num at hx 
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
⊢ place (conjugate φ) = place φ
[PROOFSTEP]
ext
[GOAL]
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
x✝ : K
⊢ ↑(place (conjugate φ)) x✝ = ↑(place φ) x✝
[PROOFSTEP]
simp only [place_apply, norm_eq_abs, abs_conj, conjugate_coe_eq]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
⊢ (fun x => (↑φ x).re) 1 = 1
[PROOFSTEP]
simp only [map_one, one_re]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
⊢ ∀ (x y : K),
    OneHom.toFun { toFun := fun x => (↑φ x).re, map_one' := (_ : (↑φ 1).re = 1) } (x * y) =
      OneHom.toFun { toFun := fun x => (↑φ x).re, map_one' := (_ : (↑φ 1).re = 1) } x *
        OneHom.toFun { toFun := fun x => (↑φ x).re, map_one' := (_ : (↑φ 1).re = 1) } y
[PROOFSTEP]
simp only [Complex.conj_eq_iff_im.mp (RingHom.congr_fun hφ _), map_mul, mul_re, mul_zero, tsub_zero, eq_self_iff_true,
  forall_const]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun x => (↑φ x).re, map_one' := (_ : (↑φ 1).re = 1) },
          map_mul' := (_ : ∀ (a a_1 : K), (↑φ (a * a_1)).re = (↑φ a).re * (↑φ a_1).re) })
      0 =
    0
[PROOFSTEP]
simp only [map_zero, zero_re]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
⊢ ∀ (x y : K),
    OneHom.toFun
        (↑{ toOneHom := { toFun := fun x => (↑φ x).re, map_one' := (_ : (↑φ 1).re = 1) },
            map_mul' := (_ : ∀ (a a_1 : K), (↑φ (a * a_1)).re = (↑φ a).re * (↑φ a_1).re) })
        (x + y) =
      OneHom.toFun
          (↑{ toOneHom := { toFun := fun x => (↑φ x).re, map_one' := (_ : (↑φ 1).re = 1) },
              map_mul' := (_ : ∀ (a a_1 : K), (↑φ (a * a_1)).re = (↑φ a).re * (↑φ a_1).re) })
          x +
        OneHom.toFun
          (↑{ toOneHom := { toFun := fun x => (↑φ x).re, map_one' := (_ : (↑φ 1).re = 1) },
              map_mul' := (_ : ∀ (a a_1 : K), (↑φ (a * a_1)).re = (↑φ a).re * (↑φ a_1).re) })
          y
[PROOFSTEP]
simp only [map_add, add_re, eq_self_iff_true, forall_const]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ ↑(↑(embedding hφ) x) = ↑φ x
[PROOFSTEP]
ext
[GOAL]
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (↑(↑(embedding hφ) x)).re = (↑φ x).re
[PROOFSTEP]
rfl
[GOAL]
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (↑(↑(embedding hφ) x)).im = (↑φ x).im
[PROOFSTEP]
rw [ofReal_im, eq_comm, ← Complex.conj_eq_iff_im]
[GOAL]
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ ↑(starRingEnd ℂ) (↑φ x) = ↑φ x
[PROOFSTEP]
exact RingHom.congr_fun hφ x
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
⊢ mk (ComplexEmbedding.conjugate φ) = mk φ
[PROOFSTEP]
refine FunLike.ext _ _ (fun x => ?_)
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
x : K
⊢ ↑(mk (ComplexEmbedding.conjugate φ)) x = ↑(mk φ) x
[PROOFSTEP]
rw [apply, apply, ComplexEmbedding.conjugate_coe_eq, Complex.abs_conj]
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : K
⊢ ‖↑(embedding w) x‖ = ↑w x
[PROOFSTEP]
nth_rewrite 2 [← mk_embedding w]
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : K
⊢ ‖↑(embedding w) x‖ = ↑(mk (embedding w)) x
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
inst✝ : Field K
x : K
r : ℝ
⊢ (∀ (φ : K →+* ℂ), ‖↑φ x‖ = r) → ∀ (w : InfinitePlace K), ↑w x = r
[PROOFSTEP]
rintro hφ ⟨w, ⟨φ, rfl⟩⟩
[GOAL]
case mk.intro
K : Type u_1
inst✝ : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), ‖↑φ x‖ = r
φ : K →+* ℂ
⊢ ↑{ val := place φ, property := (_ : ∃ φ_1, place φ_1 = place φ) } x = r
[PROOFSTEP]
exact hφ φ
[GOAL]
K : Type u_1
inst✝ : Field K
x : K
r : ℝ
⊢ (∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r) → ∀ (w : InfinitePlace K), ↑w x ≤ r
[PROOFSTEP]
rintro hφ ⟨w, ⟨φ, rfl⟩⟩
[GOAL]
case mk.intro
K : Type u_1
inst✝ : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
φ : K →+* ℂ
⊢ ↑{ val := place φ, property := (_ : ∃ φ_1, place φ_1 = place φ) } x ≤ r
[PROOFSTEP]
exact hφ φ
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ mk φ = mk ψ ↔ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ mk φ = mk ψ → φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
intro h₀
[GOAL]
case mp
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
obtain ⟨j, hiφ⟩ := (φ.injective).hasLeftInverse
[GOAL]
case mp.intro
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
let ι := RingEquiv.ofLeftInverse hiφ
[GOAL]
case mp.intro
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
have hlip : LipschitzWith 1 (RingHom.comp ψ ι.symm.toRingHom) :=
  by
  change LipschitzWith 1 (ψ ∘ ι.symm)
  apply LipschitzWith.of_dist_le_mul
  intro x y
  rw [NNReal.coe_one, one_mul, NormedField.dist_eq, Function.comp_apply, Function.comp_apply, ← map_sub, ← map_sub]
  apply le_of_eq
  suffices ‖φ (ι.symm (x - y))‖ = ‖ψ (ι.symm (x - y))‖
    by
    rw [← this, ← RingEquiv.ofLeftInverse_apply hiφ _, RingEquiv.apply_symm_apply ι _]
    rfl
  exact congrFun (congrArg (↑) h₀) _
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
⊢ LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
[PROOFSTEP]
change LipschitzWith 1 (ψ ∘ ι.symm)
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
⊢ LipschitzWith 1 (↑ψ ∘ ↑(RingEquiv.symm ι))
[PROOFSTEP]
apply LipschitzWith.of_dist_le_mul
[GOAL]
case a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
⊢ ∀ (x y : { x // x ∈ RingHom.range φ }),
    dist ((↑ψ ∘ ↑(RingEquiv.symm ι)) x) ((↑ψ ∘ ↑(RingEquiv.symm ι)) y) ≤ ↑1 * dist x y
[PROOFSTEP]
intro x y
[GOAL]
case a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
x y : { x // x ∈ RingHom.range φ }
⊢ dist ((↑ψ ∘ ↑(RingEquiv.symm ι)) x) ((↑ψ ∘ ↑(RingEquiv.symm ι)) y) ≤ ↑1 * dist x y
[PROOFSTEP]
rw [NNReal.coe_one, one_mul, NormedField.dist_eq, Function.comp_apply, Function.comp_apply, ← map_sub, ← map_sub]
[GOAL]
case a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
x y : { x // x ∈ RingHom.range φ }
⊢ ‖↑ψ (↑(RingEquiv.symm ι) (x - y))‖ ≤ dist x y
[PROOFSTEP]
apply le_of_eq
[GOAL]
case a.a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
x y : { x // x ∈ RingHom.range φ }
⊢ ‖↑ψ (↑(RingEquiv.symm ι) (x - y))‖ = dist x y
[PROOFSTEP]
suffices ‖φ (ι.symm (x - y))‖ = ‖ψ (ι.symm (x - y))‖
  by
  rw [← this, ← RingEquiv.ofLeftInverse_apply hiφ _, RingEquiv.apply_symm_apply ι _]
  rfl
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
x y : { x // x ∈ RingHom.range φ }
this : ‖↑φ (↑(RingEquiv.symm ι) (x - y))‖ = ‖↑ψ (↑(RingEquiv.symm ι) (x - y))‖
⊢ ‖↑ψ (↑(RingEquiv.symm ι) (x - y))‖ = dist x y
[PROOFSTEP]
rw [← this, ← RingEquiv.ofLeftInverse_apply hiφ _, RingEquiv.apply_symm_apply ι _]
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
x y : { x // x ∈ RingHom.range φ }
this : ‖↑φ (↑(RingEquiv.symm ι) (x - y))‖ = ‖↑ψ (↑(RingEquiv.symm ι) (x - y))‖
⊢ ‖↑(x - y)‖ = dist x y
[PROOFSTEP]
rfl
[GOAL]
case a.a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
x y : { x // x ∈ RingHom.range φ }
⊢ ‖↑φ (↑(RingEquiv.symm ι) (x - y))‖ = ‖↑ψ (↑(RingEquiv.symm ι) (x - y))‖
[PROOFSTEP]
exact congrFun (congrArg (↑) h₀) _
[GOAL]
case mp.intro
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
cases Complex.uniformContinuous_ringHom_eq_id_or_conj φ.fieldRange hlip.uniformContinuous with
| inl h =>
  left; ext1 x
  conv_rhs => rw [← hiφ x]
  exact (congrFun h (ι x)).symm
| inr h =>
  right; ext1 x
  conv_rhs => rw [← hiφ x]
  exact (congrFun h (ι x)).symm
[GOAL]
case mp.intro
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
x✝ :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ)) ∨
    (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
      ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
cases Complex.uniformContinuous_ringHom_eq_id_or_conj φ.fieldRange hlip.uniformContinuous with
| inl h =>
  left; ext1 x
  conv_rhs => rw [← hiφ x]
  exact (congrFun h (ι x)).symm
| inr h =>
  right; ext1 x
  conv_rhs => rw [← hiφ x]
  exact (congrFun h (ι x)).symm
[GOAL]
case mp.intro.inl
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]

| inl h =>
  left; ext1 x
  conv_rhs => rw [← hiφ x]
  exact (congrFun h (ι x)).symm
[GOAL]
case mp.intro.inl
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
left
[GOAL]
case mp.intro.inl.h
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
⊢ φ = ψ
[PROOFSTEP]
ext1 x
[GOAL]
case mp.intro.inl.h.a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
⊢ ↑φ x = ↑ψ x
[PROOFSTEP]
conv_rhs => rw [← hiφ x]
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
| ↑ψ x
[PROOFSTEP]
rw [← hiφ x]
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
| ↑ψ x
[PROOFSTEP]
rw [← hiφ x]
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
| ↑ψ x
[PROOFSTEP]
rw [← hiφ x]
[GOAL]
case mp.intro.inl.h.a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
⊢ ↑φ x = ↑ψ (j (↑φ x))
[PROOFSTEP]
exact (congrFun h (ι x)).symm
[GOAL]
case mp.intro.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]

| inr h =>
  right; ext1 x
  conv_rhs => rw [← hiφ x]
  exact (congrFun h (ι x)).symm
[GOAL]
case mp.intro.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
right
[GOAL]
case mp.intro.inr.h
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
⊢ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
ext1 x
[GOAL]
case mp.intro.inr.h.a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
⊢ ↑(ComplexEmbedding.conjugate φ) x = ↑ψ x
[PROOFSTEP]
conv_rhs => rw [← hiφ x]
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
| ↑ψ x
[PROOFSTEP]
rw [← hiφ x]
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
| ↑ψ x
[PROOFSTEP]
rw [← hiφ x]
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
| ↑ψ x
[PROOFSTEP]
rw [← hiφ x]
[GOAL]
case mp.intro.inr.h.a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
⊢ ↑(ComplexEmbedding.conjugate φ) x = ↑ψ (j (↑φ x))
[PROOFSTEP]
exact (congrFun h (ι x)).symm
[GOAL]
case mpr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ → mk φ = mk ψ
[PROOFSTEP]
rintro (⟨h⟩ | ⟨h⟩)
[GOAL]
case mpr.inl
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h : φ = ψ
⊢ mk φ = mk ψ
[PROOFSTEP]
exact congr_arg mk h
[GOAL]
case mpr.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h : ComplexEmbedding.conjugate φ = ψ
⊢ mk φ = mk ψ
[PROOFSTEP]
rw [← mk_conjugate_eq]
[GOAL]
case mpr.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h : ComplexEmbedding.conjugate φ = ψ
⊢ mk (ComplexEmbedding.conjugate φ) = mk ψ
[PROOFSTEP]
exact congr_arg mk h
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
⊢ embedding (mk φ) = φ ∨ embedding (mk φ) = ComplexEmbedding.conjugate φ
[PROOFSTEP]
rw [@eq_comm _ _ φ, @eq_comm _ _ (ComplexEmbedding.conjugate φ), ← mk_eq_iff, mk_embedding]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
⊢ embedding (mk φ) = φ
[PROOFSTEP]
have := embedding_mk_eq φ
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
this : embedding (mk φ) = φ ∨ embedding (mk φ) = ComplexEmbedding.conjugate φ
⊢ embedding (mk φ) = φ
[PROOFSTEP]
rwa [ComplexEmbedding.isReal_iff.mp h, or_self] at this 
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ IsReal w ↔ ComplexEmbedding.IsReal (embedding w)
[PROOFSTEP]
refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ IsReal w → ComplexEmbedding.IsReal (embedding w)
[PROOFSTEP]
rintro ⟨φ, ⟨hφ, rfl⟩⟩
[GOAL]
case intro.intro
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ ComplexEmbedding.IsReal (embedding (mk φ))
[PROOFSTEP]
rwa [embedding_mk_eq_of_isReal hφ]
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ IsComplex w ↔ ¬ComplexEmbedding.IsReal (embedding w)
[PROOFSTEP]
refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ IsComplex w → ¬ComplexEmbedding.IsReal (embedding w)
[PROOFSTEP]
rintro ⟨φ, ⟨hφ, rfl⟩⟩
[GOAL]
case intro.intro
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
⊢ ¬ComplexEmbedding.IsReal (embedding (mk φ))
[PROOFSTEP]
contrapose! hφ
[GOAL]
case intro.intro
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (embedding (mk φ))
⊢ ComplexEmbedding.IsReal φ
[PROOFSTEP]
cases mk_eq_iff.mp (mk_embedding (mk φ)) with
| inl h => rwa [h] at hφ 
| inr h => rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ 
[GOAL]
case intro.intro
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (embedding (mk φ))
x✝ : embedding (mk φ) = φ ∨ ComplexEmbedding.conjugate (embedding (mk φ)) = φ
⊢ ComplexEmbedding.IsReal φ
[PROOFSTEP]
cases mk_eq_iff.mp (mk_embedding (mk φ)) with
| inl h => rwa [h] at hφ 
| inr h => rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ 
[GOAL]
case intro.intro.inl
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (embedding (mk φ))
h : embedding (mk φ) = φ
⊢ ComplexEmbedding.IsReal φ
[PROOFSTEP]

| inl h => rwa [h] at hφ 
[GOAL]
case intro.intro.inl
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (embedding (mk φ))
h : embedding (mk φ) = φ
⊢ ComplexEmbedding.IsReal φ
[PROOFSTEP]
rwa [h] at hφ 
[GOAL]
case intro.intro.inr
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (embedding (mk φ))
h : ComplexEmbedding.conjugate (embedding (mk φ)) = φ
⊢ ComplexEmbedding.IsReal φ
[PROOFSTEP]

| inr h => rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ 
[GOAL]
case intro.intro.inr
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (embedding (mk φ))
h : ComplexEmbedding.conjugate (embedding (mk φ)) = φ
⊢ ComplexEmbedding.IsReal φ
[PROOFSTEP]
rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ 
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ ¬IsReal w ↔ IsComplex w
[PROOFSTEP]
rw [isComplex_iff, isReal_iff]
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ IsReal w ∨ IsComplex w
[PROOFSTEP]
rw [← not_isReal_iff_isComplex]
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ IsReal w ∨ ¬IsReal w
[PROOFSTEP]
exact em _
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : IsReal (mk φ)
⊢ ComplexEmbedding.IsReal φ
[PROOFSTEP]
contrapose! h
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ¬ComplexEmbedding.IsReal φ
⊢ ¬IsReal (mk φ)
[PROOFSTEP]
rw [not_isReal_iff_isComplex]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ¬ComplexEmbedding.IsReal φ
⊢ IsComplex (mk φ)
[PROOFSTEP]
exact ⟨φ, h, rfl⟩
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : IsComplex (mk φ)
⊢ ¬ComplexEmbedding.IsReal φ
[PROOFSTEP]
contrapose! h
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
⊢ ¬IsComplex (mk φ)
[PROOFSTEP]
rw [← not_isReal_iff_isComplex.not, not_not]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
⊢ IsReal (mk φ)
[PROOFSTEP]
exact ⟨φ, h, rfl⟩
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ Finset.card (Finset.filter (fun φ => mk φ = w) Finset.univ) = mult w
[PROOFSTEP]
conv_lhs =>
  congr; congr; ext
  rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.card (Finset.filter (fun φ => mk φ = w) Finset.univ)
[PROOFSTEP]
  congr; congr; ext
  rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.card (Finset.filter (fun φ => mk φ = w) Finset.univ)
[PROOFSTEP]
  congr; congr; ext
  rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.card (Finset.filter (fun φ => mk φ = w) Finset.univ)
[PROOFSTEP]
congr
[GOAL]
case s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.filter (fun φ => mk φ = w) Finset.univ
[PROOFSTEP]
congr
[GOAL]
case s.p
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| fun φ => mk φ = w
case s.s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.univ
K : Type u_1 inst✝¹ : Field K inst✝ : NumberField K w : InfinitePlace K ⊢ DecidablePred ?m.1138470
[PROOFSTEP]
ext
[GOAL]
case s.p.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
x✝ : K →+* ℂ
| mk x✝ = w
case s.s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.univ
K : Type u_1 inst✝¹ : Field K inst✝ : NumberField K w : InfinitePlace K ⊢ DecidablePred ?m.1138470
[PROOFSTEP]
rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ Finset.card (Finset.filter (fun x => x = embedding w ∨ x = star (embedding w)) Finset.univ) = mult w
[PROOFSTEP]
simp_rw [Finset.filter_or, Finset.filter_eq' _ (embedding w),
  Finset.filter_eq' _ (ComplexEmbedding.conjugate (embedding w)), Finset.mem_univ, ite_true, mult]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ Finset.card ({embedding w} ∪ {ComplexEmbedding.conjugate (embedding w)}) = if IsReal w then 1 else 2
[PROOFSTEP]
split_ifs with hw
[GOAL]
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsReal w
⊢ Finset.card ({embedding w} ∪ {ComplexEmbedding.conjugate (embedding w)}) = 1
[PROOFSTEP]
rw [ComplexEmbedding.isReal_iff.mp (isReal_iff.mp hw), Finset.union_idempotent, Finset.card_singleton]
[GOAL]
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : ¬IsReal w
⊢ Finset.card ({embedding w} ∪ {ComplexEmbedding.conjugate (embedding w)}) = 2
[PROOFSTEP]
refine Finset.card_doubleton ?_
[GOAL]
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : ¬IsReal w
⊢ embedding w ≠ ComplexEmbedding.conjugate (embedding w)
[PROOFSTEP]
rwa [Ne.def, eq_comm, ← ComplexEmbedding.isReal_iff, ← isReal_iff]
[GOAL]
K : Type u_1
inst✝ : Field K
⊢ { φ // ComplexEmbedding.IsReal φ } ≃ { w // IsReal w }
[PROOFSTEP]
refine (Equiv.ofBijective (fun φ => ⟨mk φ, ?_⟩) ⟨fun φ ψ h => ?_, fun w => ?_⟩)
[GOAL]
case refine_1
K : Type u_1
inst✝ : Field K
φ : { φ // ComplexEmbedding.IsReal φ }
⊢ IsReal (mk ↑φ)
[PROOFSTEP]
exact ⟨φ, φ.prop, rfl⟩
[GOAL]
case refine_2
K : Type u_1
inst✝ : Field K
φ ψ : { φ // ComplexEmbedding.IsReal φ }
h :
  (fun φ => { val := mk ↑φ, property := (_ : ∃ φ_1, ComplexEmbedding.IsReal φ_1 ∧ mk φ_1 = mk ↑φ) }) φ =
    (fun φ => { val := mk ↑φ, property := (_ : ∃ φ_1, ComplexEmbedding.IsReal φ_1 ∧ mk φ_1 = mk ↑φ) }) ψ
⊢ φ = ψ
[PROOFSTEP]
rwa [Subtype.mk.injEq, mk_eq_iff, ComplexEmbedding.isReal_iff.mp φ.prop, or_self, ← Subtype.ext_iff] at h 
[GOAL]
case refine_3
K : Type u_1
inst✝ : Field K
w : { w // IsReal w }
⊢ ∃ a, (fun φ => { val := mk ↑φ, property := (_ : ∃ φ_1, ComplexEmbedding.IsReal φ_1 ∧ mk φ_1 = mk ↑φ) }) a = w
[PROOFSTEP]
exact ⟨⟨embedding w, isReal_iff.mp w.prop⟩, by simp⟩
[GOAL]
K : Type u_1
inst✝ : Field K
w : { w // IsReal w }
⊢ (fun φ => { val := mk ↑φ, property := (_ : ∃ φ_1, ComplexEmbedding.IsReal φ_1 ∧ mk φ_1 = mk ↑φ) })
      { val := embedding ↑w, property := (_ : ComplexEmbedding.IsReal (embedding ↑w)) } =
    w
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w : InfinitePlace K, ↑w x ^ mult w = ↑|↑(Algebra.norm ℚ) x|
[PROOFSTEP]
convert (congr_arg Complex.abs (@Algebra.norm_eq_prod_embeddings ℚ _ _ _ _ ℂ _ _ _ _ _ x)).symm
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w : InfinitePlace K, ↑w x ^ mult w = ↑Complex.abs (∏ σ : K →ₐ[ℚ] ℂ, ↑σ x)
[PROOFSTEP]
rw [map_prod, ←
  Equiv.prod_comp' RingHom.equivRatAlgHom (fun f => Complex.abs (f x)) (fun φ => Complex.abs (φ x)) fun _ => by
    simp [RingHom.equivRatAlgHom_apply]; rfl]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
x✝ : K →+* ℂ
⊢ (fun f => ↑Complex.abs (↑f x)) x✝ = (fun φ => ↑Complex.abs (↑φ x)) (↑RingHom.equivRatAlgHom x✝)
[PROOFSTEP]
simp [RingHom.equivRatAlgHom_apply]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
x✝ : K →+* ℂ
⊢ ↑Complex.abs (↑x✝ x) = ↑Complex.abs (↑(RingHom.toRatAlgHom x✝) x)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w : InfinitePlace K, ↑w x ^ mult w = ∏ i : K →+* ℂ, ↑Complex.abs (↑i x)
[PROOFSTEP]
rw [← Finset.prod_fiberwise Finset.univ (fun φ => mk φ) (fun φ => Complex.abs (φ x))]
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w : InfinitePlace K, ↑w x ^ mult w =
    ∏ b : InfinitePlace K, ∏ a in Finset.filter (fun a => mk a = b) Finset.univ, ↑Complex.abs (↑a x)
[PROOFSTEP]
have : ∀ w : InfinitePlace K, ∀ φ ∈ Finset.filter (fun a ↦ mk a = w) Finset.univ, Complex.abs (φ x) = w x :=
  by
  intro _ _ hφ
  rw [← (Finset.mem_filter.mp hφ).2]
  rfl
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∀ (w : InfinitePlace K) (φ : K →+* ℂ), φ ∈ Finset.filter (fun a => mk a = w) Finset.univ → ↑Complex.abs (↑φ x) = ↑w x
[PROOFSTEP]
intro _ _ hφ
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
w✝ : InfinitePlace K
φ✝ : K →+* ℂ
hφ : φ✝ ∈ Finset.filter (fun a => mk a = w✝) Finset.univ
⊢ ↑Complex.abs (↑φ✝ x) = ↑w✝ x
[PROOFSTEP]
rw [← (Finset.mem_filter.mp hφ).2]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
w✝ : InfinitePlace K
φ✝ : K →+* ℂ
hφ : φ✝ ∈ Finset.filter (fun a => mk a = w✝) Finset.univ
⊢ ↑Complex.abs (↑φ✝ x) = ↑(mk φ✝) x
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
this :
  ∀ (w : InfinitePlace K) (φ : K →+* ℂ), φ ∈ Finset.filter (fun a => mk a = w) Finset.univ → ↑Complex.abs (↑φ x) = ↑w x
⊢ ∏ w : InfinitePlace K, ↑w x ^ mult w =
    ∏ b : InfinitePlace K, ∏ a in Finset.filter (fun a => mk a = b) Finset.univ, ↑Complex.abs (↑a x)
[PROOFSTEP]
simp_rw [Finset.prod_congr rfl (this _), Finset.prod_const, card_filter_mk_eq]
[GOAL]
case h.e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ↑|↑(Algebra.norm ℚ) x| = ↑Complex.abs (↑(algebraMap ℚ ℂ) (↑(Algebra.norm ℚ) x))
[PROOFSTEP]
rw [eq_ratCast, Rat.cast_abs, ← Complex.abs_ofReal, Complex.ofReal_rat_cast]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card { φ // ¬ComplexEmbedding.IsReal φ } = 2 * card { w // IsComplex w }
[PROOFSTEP]
suffices
  ∀ w : { w : InfinitePlace K // IsComplex w },
    (Finset.univ.filter fun φ : { φ // ¬ComplexEmbedding.IsReal φ } => mkComplex φ = w).card = 2
  by
  rw [Fintype.card, Finset.card_eq_sum_ones, ← Finset.sum_fiberwise _ (fun φ => mkComplex φ)]
  simp_rw [Finset.sum_const, this, smul_eq_mul, mul_one, Fintype.card, Finset.card_eq_sum_ones, Finset.mul_sum]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : ∀ (w : { w // IsComplex w }), Finset.card (Finset.filter (fun φ => mkComplex φ = w) Finset.univ) = 2
⊢ card { φ // ¬ComplexEmbedding.IsReal φ } = 2 * card { w // IsComplex w }
[PROOFSTEP]
rw [Fintype.card, Finset.card_eq_sum_ones, ← Finset.sum_fiberwise _ (fun φ => mkComplex φ)]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : ∀ (w : { w // IsComplex w }), Finset.card (Finset.filter (fun φ => mkComplex φ = w) Finset.univ) = 2
⊢ ∑ b : { w // IsComplex w }, ∑ a in Finset.filter (fun a => mkComplex a = b) Finset.univ, 1 =
    2 * card { w // IsComplex w }
[PROOFSTEP]
simp_rw [Finset.sum_const, this, smul_eq_mul, mul_one, Fintype.card, Finset.card_eq_sum_ones, Finset.mul_sum]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∀ (w : { w // IsComplex w }), Finset.card (Finset.filter (fun φ => mkComplex φ = w) Finset.univ) = 2
[PROOFSTEP]
rintro ⟨w, hw⟩
[GOAL]
case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
⊢ Finset.card (Finset.filter (fun φ => mkComplex φ = { val := w, property := hw }) Finset.univ) = 2
[PROOFSTEP]
convert card_filter_mk_eq w
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
⊢ Finset.card (Finset.filter (fun φ => mkComplex φ = { val := w, property := hw }) Finset.univ) =
    Finset.card (Finset.filter (fun φ => mk φ = w) Finset.univ)
[PROOFSTEP]
rw [← Fintype.card_subtype, ← Fintype.card_subtype]
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
⊢ card { x // mkComplex x = { val := w, property := hw } } = card { x // mk x = w }
[PROOFSTEP]
refine Fintype.card_congr (Equiv.ofBijective ?_ ⟨fun _ _ h => ?_, fun ⟨φ, hφ⟩ => ?_⟩)
[GOAL]
case h.e'_2.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
⊢ { x // mkComplex x = { val := w, property := hw } } → { x // mk x = w }
[PROOFSTEP]
exact fun ⟨φ, hφ⟩ => ⟨φ.val, by rwa [Subtype.ext_iff] at hφ ⟩
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
x✝ : { x // mkComplex x = { val := w, property := hw } }
φ : { φ // ¬ComplexEmbedding.IsReal φ }
hφ : mkComplex φ = { val := w, property := hw }
⊢ mk ↑φ = w
[PROOFSTEP]
rwa [Subtype.ext_iff] at hφ 
[GOAL]
case h.e'_2.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
x✝¹ x✝ : { x // mkComplex x = { val := w, property := hw } }
h :
  (match x✝¹ with
    | { val := φ, property := hφ } => { val := ↑φ, property := (_ : ↑(mkComplex φ) = ↑{ val := w, property := hw }) }) =
    match x✝ with
    | { val := φ, property := hφ } => { val := ↑φ, property := (_ : ↑(mkComplex φ) = ↑{ val := w, property := hw }) }
⊢ x✝¹ = x✝
[PROOFSTEP]
rwa [Subtype.mk_eq_mk, ← Subtype.ext_iff, ← Subtype.ext_iff] at h 
[GOAL]
case h.e'_2.refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
x✝ : { x // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
⊢ ∃ a,
    (match a with
      | { val := φ, property := hφ } =>
        { val := ↑φ, property := (_ : ↑(mkComplex φ) = ↑{ val := w, property := hw }) }) =
      { val := φ, property := hφ }
[PROOFSTEP]
refine ⟨⟨⟨φ, not_isReal_of_mk_isComplex (hφ.symm ▸ hw)⟩, ?_⟩, rfl⟩
[GOAL]
case h.e'_2.refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
x✝ : { x // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
⊢ mkComplex { val := φ, property := (_ : ¬ComplexEmbedding.IsReal φ) } = { val := w, property := hw }
[PROOFSTEP]
rwa [Subtype.ext_iff, mkComplex_coe]
[GOAL]
case h.e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
⊢ 2 = mult w
[PROOFSTEP]
simp_rw [mult, not_isReal_iff_isComplex.mpr hw]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card { w // IsReal w } + 2 * card { w // IsComplex w } = finrank ℚ K
[PROOFSTEP]
rw [← card_real_embeddings, ← card_complex_embeddings]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card { φ // ComplexEmbedding.IsReal φ } + card { φ // ¬ComplexEmbedding.IsReal φ } = finrank ℚ K
[PROOFSTEP]
rw [Fintype.card_subtype_compl, ← Embeddings.card K ℂ, Nat.add_sub_of_le]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card { φ // ComplexEmbedding.IsReal φ } ≤ card (K →+* ℂ)
[PROOFSTEP]
exact Fintype.card_subtype_le _
