-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Algebra R ℚ
inst_3 : IsFractionRing R ℚ
inst_4 : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
x : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p))
⊢ HEq (α := ℚ_[(↑p : ℕ)])
    (↑(cast (α :=
          ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
                  ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
              ℕ)])
          ⋯
          ((adicCompletionIntegers.padicIntEquiv ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p) :
                (a :
                    ↥(HeightOneSpectrum.adicCompletionIntegers ℚ
                        ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p))) →
                  ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes)
                          ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
                      ℕ)])
              x :
            ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
                    ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
                ℕ)])) :
      ℚ_[(↑p : ℕ)])
    (β :=
    ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
            ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
        ℕ)])
    (↑((adicCompletionIntegers.padicIntEquiv ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p) :
            (a :
                ↥(HeightOneSpectrum.adicCompletionIntegers ℚ
                    ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p))) →
              ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes)
                      ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
                  ℕ)])
          x) :
      ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes)
              ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
          ℕ)])
have rw : HEq (α := { x : ℚ_[(↑p : ℕ)] // ‖x‖ ≤ 1 })
  (cast (α :=
      ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
              ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
          ℕ)])
      sorry
      ((adicCompletionIntegers.padicIntEquiv ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p) :
            (a :
                ↥(HeightOneSpectrum.adicCompletionIntegers ℚ
                    ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p))) →
              ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes)
                      ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
                  ℕ)])
          x :
        ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
                ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
            ℕ)]) :
    ℤ_[(↑p : ℕ)])
  (β :=
  { y :
    ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
            ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
        ℕ)] //
    ‖y‖ ≤ 1 })
  ((adicCompletionIntegers.padicIntEquiv ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p) :
        (a :
            ↥(HeightOneSpectrum.adicCompletionIntegers ℚ
                ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p))) →
          ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes)
                  ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
              ℕ)])
      x :
    ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
            ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
        ℕ)])
Tactic: rw [← Subtype.heq_iff_coe_heq (by rw [primesEquiv.apply_symm_apply])
    (by rw [primesEquiv.apply_symm_apply])]