-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
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))
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)) :
            ℕ)])
        ⋯
        ((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)) :
          ℕ)])
⊢ 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)) :
          ℕ)])

Tactic:
rw [← Subtype.heq_iff_coe_heq (by rw [primesEquiv.apply_symm_apply])
    (by rw [primesEquiv.apply_symm_apply])]

Premises used: Subtype.heq_iff_coe_heq