-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0
inr :
  ∀ (h : 1 ≤ norm (E := ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ))
    (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
    (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
    1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
inr₁ :
  ∀
    (h :
      1 ≤
        ‖(↑(Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))) : ℂ) +
            (↑(Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K))) : ℂ) * Complex.I‖)
    (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
    (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
    1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
inr₂ :
  ∀ (h : 1 ≤ ‖(↑(Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))) : ℂ) + (↑0 : ℂ) * Complex.I‖)
    (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
    (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
    1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
inr₃ :
  ∀ (h : 1 ≤ ‖(↑(Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))) : ℂ) + 0 * Complex.I‖)
    (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
    (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
    1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
inr₄ :
  ∀ (h : 1 ≤ ‖(↑(Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))) : ℂ) + 0‖)
    (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
    (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
    1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
⊢ 1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
have inr₅ : ∀ (h : 1 ≤ ‖(↑(Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))) : ℂ)‖)
  (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
  (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
  (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
  (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
  1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
Tactic: rwa [← norm_embedding_eq, ← Complex.re_add_im (embedding w x), this, Complex.ofReal_zero,
        zero_mul, add_zero, Complex.norm_real] at h
Cleared hypotheses: h, main, hw, h', this