-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem mk_eq_iff {φ ψ : K →+* ℂ} : mk φ = mk ψ ↔ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

Proof state:
case mp.intro.inl.h
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑φ.fieldRange.subtype
⊢ φ = ψ

Tactic:
ext1 x

Result:
case mp.intro.inl.h.a
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑φ.fieldRange.subtype
x : K
⊢ φ x = ψ x

Proof state:
case mp
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ mk φ = mk ψ → φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

Tactic:
intro h₀

Result:
case mp
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

Proof state:
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ mk φ = mk ψ ↔ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

Tactic:
constructor

Result:
case mp
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ mk φ = mk ψ → φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

case mpr
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ → mk φ = mk ψ

Proof state:
case a
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
⊢ ∀ (x y : ↥φ.range), dist ((⇑ψ ∘ ⇑ι.symm) x) ((⇑ψ ∘ ⇑ι.symm) y) ≤ ↑1 * dist x y

Tactic:
intro x y

Result:
case a
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
x y : ↥φ.range
⊢ dist ((⇑ψ ∘ ⇑ι.symm) x) ((⇑ψ ∘ ⇑ι.symm) y) ≤ ↑1 * dist x y

Proof state:
case a.hab
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
x y : ↥φ.range
⊢ ‖φ (ι.symm (x - y))‖ = ‖ψ (ι.symm (x - y))‖

Tactic:
exact congrFun (congrArg (↑) h₀) _

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
⊢ LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)

Tactic:
change LipschitzWith 1 (ψ ∘ ι.symm)

Result:
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
⊢ LipschitzWith 1 (⇑ψ ∘ ⇑ι.symm)

Proof state:
case mp.intro.inl.h.a
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑φ.fieldRange.subtype
x : K
⊢ φ x = ψ (j (φ x))

Tactic:
exact (congrFun h (ι x)).symm

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
⊢ LipschitzWith 1 (⇑ψ ∘ ⇑ι.symm)

Tactic:
apply LipschitzWith.of_dist_le_mul

Result:
case a
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
⊢ ∀ (x y : ↥φ.range), dist ((⇑ψ ∘ ⇑ι.symm) x) ((⇑ψ ∘ ⇑ι.symm) y) ≤ ↑1 * dist x y

Proof state:
case a
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
x y : ↥φ.range
⊢ ‖ψ (ι.symm (x - y))‖ ≤ dist x y

Tactic:
apply le_of_eq

Result:
case a.hab
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
x y : ↥φ.range
⊢ ‖ψ (ι.symm (x - y))‖ = dist x y

Proof state:
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
x y : ↥φ.range
this : ‖φ (ι.symm (x - y))‖ = ‖ψ (ι.symm (x - y))‖
⊢ ‖ψ (ι.symm (x - y))‖ = dist x y

Tactic:
rw [← this, ← RingEquiv.ofLeftInverse_apply hiφ _, RingEquiv.apply_symm_apply ι _]

Result:
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
x y : ↥φ.range
this : ‖φ (ι.symm (x - y))‖ = ‖ψ (ι.symm (x - y))‖
⊢ ‖↑(x - y)‖ = dist x y

Proof state:
case mp.intro
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

Tactic:
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₀) _

Result:
case mp.intro
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

Proof state:
case mp.intro.inl.h.a
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑φ.fieldRange.subtype
x : K
⊢ φ x = ψ x

Tactic:
conv_rhs => rw [← hiφ x]

Result:
case mp.intro.inl.h.a
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑φ.fieldRange.subtype
x : K
⊢ φ x = ψ (j (φ x))

Proof state:
case mp.intro
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

Tactic:
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

Result:
no goals

Proof state:
case mpr.inr
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h : ComplexEmbedding.conjugate φ = ψ
⊢ mk (ComplexEmbedding.conjugate φ) = mk ψ

Tactic:
exact congr_arg mk h

Result:
no goals

Proof state:
case mpr
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ → mk φ = mk ψ

Tactic:
rintro (⟨h⟩ | ⟨h⟩)

Result:
case mpr.inl
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h : φ = ψ
⊢ mk φ = mk ψ

case mpr.inr
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h : ComplexEmbedding.conjugate φ = ψ
⊢ mk φ = mk ψ

Proof state:
case mp.intro.inr.h.a
K : Type u_2
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑(starRingEnd ℂ) ∘ ⇑φ.fieldRange.subtype
x : K
⊢ (ComplexEmbedding.conjugate φ) x = ψ (j (φ x))

Tactic:
exact (congrFun h (ι x)).symm

Result:
no goals