-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem nnnorm_eq_sup_normAtPlace (x : mixedSpace K) :
    ‖x‖₊ = univ.sup fun w ↦ ⟨normAtPlace w x, normAtPlace_nonneg w x⟩

Proof state:
case e_a.e_f
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ
⊢ (fun b => ‖x.2 b‖₊) = (fun w => ⟨(normAtPlace w) x, ⋯⟩) ∘ fun w => ↑w

Tactic:
ext w

Result:
case e_a.e_f.h.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ
w : { w // w.IsComplex }
⊢ ↑‖x.2 w‖₊ = ↑(((fun w => ⟨(normAtPlace w) x, ⋯⟩) ∘ fun w => ↑w) w)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ‖x‖₊ = univ.sup fun w => ⟨(normAtPlace w) x, ⋯⟩

Tactic:
have :
    (univ : Finset (InfinitePlace K)) =
    (univ.image (fun w : {w : InfinitePlace K // IsReal w} ↦ w.1)) ∪
    (univ.image (fun w : {w : InfinitePlace K // IsComplex w} ↦ w.1)) := by
  ext; simp [isReal_or_isComplex]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ
⊢ ‖x‖₊ = univ.sup fun w => ⟨(normAtPlace w) x, ⋯⟩

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ
⊢ ‖x‖₊ = univ.sup fun w => ⟨(normAtPlace w) x, ⋯⟩

Tactic:
rw [this, sup_union, univ.sup_image, univ.sup_image,
  Prod.nnnorm_def, Pi.nnnorm_def, Pi.nnnorm_def]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ
⊢ ((univ.sup fun b => ‖x.1 b‖₊) ⊔ univ.sup fun b => ‖x.2 b‖₊) =
    univ.sup ((fun w => ⟨(normAtPlace w) x, ⋯⟩) ∘ fun w => ↑w) ⊔
      univ.sup ((fun w => ⟨(normAtPlace w) x, ⋯⟩) ∘ fun w => ↑w)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ univ = image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ

Tactic:
ext

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
a✝ : InfinitePlace K
⊢ a✝ ∈ univ ↔ a✝ ∈ image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ

Proof state:
case e_a.e_f
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ
⊢ (fun b => ‖x.1 b‖₊) = (fun w => ⟨(normAtPlace w) x, ⋯⟩) ∘ fun w => ↑w

Tactic:
ext w

Result:
case e_a.e_f.h.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ
w : { w // w.IsReal }
⊢ ↑‖x.1 w‖₊ = ↑(((fun w => ⟨(normAtPlace w) x, ⋯⟩) ∘ fun w => ↑w) w)

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
a✝ : InfinitePlace K
⊢ a✝ ∈ univ ↔ a✝ ∈ image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ

Tactic:
simp [isReal_or_isComplex]

Result:
no goals

Proof state:
case e_a.e_f.h.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ
w : { w // w.IsComplex }
⊢ ↑‖x.2 w‖₊ = ↑(((fun w => ⟨(normAtPlace w) x, ⋯⟩) ∘ fun w => ↑w) w)

Tactic:
simp [normAtPlace_apply_of_isComplex w.prop]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ
⊢ ((univ.sup fun b => ‖x.1 b‖₊) ⊔ univ.sup fun b => ‖x.2 b‖₊) =
    univ.sup ((fun w => ⟨(normAtPlace w) x, ⋯⟩) ∘ fun w => ↑w) ⊔
      univ.sup ((fun w => ⟨(normAtPlace w) x, ⋯⟩) ∘ fun w => ↑w)

Tactic:
congr

Result:
case e_a.e_f
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ
⊢ (fun b => ‖x.1 b‖₊) = (fun w => ⟨(normAtPlace w) x, ⋯⟩) ∘ fun w => ↑w

case e_a.e_f
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ
⊢ (fun b => ‖x.2 b‖₊) = (fun w => ⟨(normAtPlace w) x, ⋯⟩) ∘ fun w => ↑w

Proof state:
case e_a.e_f.h.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ
w : { w // w.IsReal }
⊢ ↑‖x.1 w‖₊ = ↑(((fun w => ⟨(normAtPlace w) x, ⋯⟩) ∘ fun w => ↑w) w)

Tactic:
simp [normAtPlace_apply_of_isReal w.prop]

Result:
no goals