-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst :
  ∀ {z w : 𝕜},
    z ≤ w ↔
      LE.le (α := ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    re)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              z :
            ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    re)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              w :
            ℝ) ∧
        Eq (α := ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    im)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              z :
            ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    im)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              w :
            ℝ)
⊢ ∀ {z w : 𝕜},
    z ≤ w ↔
      LE.le (α := ℝ)
          (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    re)
                    ⋯ :
                  let __spread.0 := hk;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              z :
            ℝ)
          (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    re)
                    ⋯ :
                  let __spread.0 := hk;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              w :
            ℝ) ∧
        Eq (α := ℝ)
          (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    im)
                    ⋯ :
                  let __spread.0 := hk;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              z :
            ℝ)
          (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    im)
                    ⋯ :
                  let __spread.0 := hk;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              w :
            ℝ)

Tactic:
subst h''