-- 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))
simp :
  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)) :
          ℕ)])
⊢ Eq (α := ℚ_[(↑p : ℕ)])
    ((↑((ContinuousAlgEquiv.symm (adicCompletionIntegersEquiv R p) :
              (a :
                  ↥(HeightOneSpectrum.adicCompletionIntegers ℚ
                      ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p))) →
                ℤ_[(↑p : ℕ)])
            x) :
        ℚ_[(↑p : ℕ)]) :
      ℚ_[(↑p : ℕ)])
    ((ContinuousAlgEquiv.symm (adicCompletionEquiv R p) :
          (a : HeightOneSpectrum.adicCompletion ℚ ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) →
            ℚ_[(↑p : ℕ)])
        (↑x : HeightOneSpectrum.adicCompletion ℚ ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
      ℚ_[(↑p : ℕ)])

Tactic:
simp only [adicCompletionIntegersEquiv, ContinuousAlgEquiv.symm_trans_apply,
    ContinuousAlgEquiv.symm_symm, adicCompletionEquiv, Equiv.cast_apply, eq_cast_iff_heq,
    ← adicCompletionIntegers.coe_padicIntEquiv_apply, ContinuousAlgEquiv.cast_symm_apply]

Premises used: Padic.adicCompletionEquiv, eq_cast_iff_heq, ContinuousAlgEquiv.symm_trans_apply, PadicInt.adicCompletionIntegersEquiv, ContinuousAlgEquiv.cast_symm_apply, Equiv.cast_apply, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, ContinuousAlgEquiv.symm_symm