awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R ℚ
v : HeightOneSpectrum R
y : ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]
hy :
  y ∈
    (↑(subring (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)) :
      Set ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
x : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)
hx :
  (adicCompletionIntegers.padicIntEquiv v :
        (a : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)) →
          ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
      x =
    Subtype.mk (p :=
      fun
        (x :
          ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) ↦
      ‖x‖ ≤ 1) y hy
rw :
  (↑((adicCompletionIntegers.padicIntEquiv v :
            (a : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)) →
              ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
          x) :
      ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) =
    y
rw₁ rw₂ :
  (↑(Subtype.mk (p :=
          fun
            (x :
              ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) :
                  ℕ)]) ↦
          ‖x‖ ≤ 1) y hy) :
      ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) =
    y
⊢ (padicEquiv v :
        (a : HeightOneSpectrum.adicCompletion ℚ v) →
          ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
      (↑x : HeightOneSpectrum.adicCompletion ℚ v) =
    y

Tactic:
rw [← adicCompletionIntegers.coe_padicIntEquiv_apply, hx]

Premises used: Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R ℚ
v : HeightOneSpectrum R
y : ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]
hy :
  y ∈
    (↑(subring (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)) :
      Set ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
x : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)
hx :
  (adicCompletionIntegers.padicIntEquiv v :
        (a : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)) →
          ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
      x =
    Subtype.mk (p :=
      fun
        (x :
          ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) ↦
      ‖x‖ ≤ 1) y hy
⊢ Membership.mem (γ :=
    Set ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
    ((⇑(padicEquiv v) :
        (a : HeightOneSpectrum.adicCompletion ℚ v) →
          ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) ''
      (↑(HeightOneSpectrum.adicCompletionIntegers ℚ v) : Set (HeightOneSpectrum.adicCompletion ℚ v)))
    y

Tactic:
refine ⟨x, x.2, by rw [← adicCompletionIntegers.coe_padicIntEquiv_apply, hx]⟩
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : Algebra R_1 ℚ
inst_2 : IsIntegralClosure R_1 ℤ ℚ
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDedekindDomain R
inst_5 : Algebra R ℚ
inst_6 : IsFractionRing R ℚ
inst_7 : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
⊢ ℚ_[(↑p : ℕ)] ≃A[ℚ]
    HeightOneSpectrum.adicCompletion.{u_2, 0} (R := R) ℚ
      ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)

Tactic:
apply (ContinuousAlgEquiv.cast (primesEquiv.apply_symm_apply p).symm).trans
    (adicCompletion.padicEquiv (primesEquiv.symm p)).symm

Premises used: Equiv.apply_symm_apply, Rat.HeightOneSpectrum.primesEquiv, ContinuousAlgEquiv.trans, ContinuousAlgEquiv.cast, Eq.symm
-- Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : Algebra R_1 ℚ
inst_2 : IsIntegralClosure R_1 ℤ ℚ
R : Type u_2
inst_3 : CommRing R
inst_4 : IsDedekindDomain R
inst_5 : Algebra R ℚ
inst_6 : IsFractionRing R ℚ
inst_7 : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
⊢ ℤ_[(↑p : ℕ)] ≃A[ℤ]
    ↥(HeightOneSpectrum.adicCompletionIntegers ℚ ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p))

Tactic:
apply (ContinuousAlgEquiv.cast (primesEquiv.apply_symm_apply p).symm).trans
    (adicCompletionIntegers.padicIntEquiv (primesEquiv.symm p)).symm

Premises used: Equiv.apply_symm_apply, Rat.HeightOneSpectrum.primesEquiv, ContinuousAlgEquiv.trans, ContinuousAlgEquiv.cast, Eq.symm
-- 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 : ℤ_[(↑p : ℕ)]
simp :
  HEq (α :=
    ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
            ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
        ℕ)])
    (↑(cast ⋯ x) :
      ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes)
              ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
          ℕ)])
    (↑x : ℚ_[(↑p : ℕ)])
⊢ Eq (α :=
    HeightOneSpectrum.adicCompletion.{u_2, 0} (R := R) ℚ
      ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p))
    ((↑((adicCompletionIntegersEquiv R p :
              (a : ℤ_[(↑p : ℕ)]) →
                ↥(HeightOneSpectrum.adicCompletionIntegers ℚ
                    ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)))
            x) :
        HeightOneSpectrum.adicCompletion.{u_2, 0} (R := R) ℚ
          ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
      HeightOneSpectrum.adicCompletion.{u_2, 0} (R := R) ℚ
        ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p))
    ((adicCompletionEquiv R p :
          (a : ℚ_[(↑p : ℕ)]) →
            HeightOneSpectrum.adicCompletion ℚ ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p))
        (↑x : ℚ_[(↑p : ℕ)]) :
      HeightOneSpectrum.adicCompletion.{u_2, 0} (R := R) ℚ
        ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p))

Tactic:
simp only [adicCompletionIntegersEquiv, ContinuousAlgEquiv.trans_apply,
    adicCompletionIntegers.coe_padicIntEquiv_symm_apply,
    adicCompletionEquiv, ContinuousAlgEquiv.trans_apply, ContinuousAlgEquiv.cast_apply,
    EmbeddingLike.apply_eq_iff_eq, Equiv.cast_apply, eq_cast_iff_heq]

Premises used: Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, Padic.adicCompletionEquiv, eq_cast_iff_heq, PadicInt.adicCompletionIntegersEquiv, EmbeddingLike.apply_eq_iff_eq, ContinuousAlgEquiv.trans_apply, Equiv.cast_apply, ContinuousAlgEquiv.cast_apply
-- 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 : ℤ_[(↑p : ℕ)]
rw rw₁ : ℚ_[(↑p : ℕ)] = ℚ_[(↑p : ℕ)]
⊢ ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
            ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
        ℕ)] =
    ℚ_[(↑p : ℕ)]

Tactic:
rw [primesEquiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Rat.HeightOneSpectrum.primesEquiv
-- 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 : ℤ_[(↑p : ℕ)]
rw rw₁ :
  HEq (α := ℚ_[(↑p : ℕ)] → Prop) fun (x : ℚ_[(↑p : ℕ)]) ↦ ‖x‖ ≤ 1 (β := ℚ_[(↑p : ℕ)] → Prop) fun (x : ℚ_[(↑p : ℕ)]) ↦
    ‖x‖ ≤ 1
⊢ HEq (α :=
    ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
              ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
          ℕ)] →
      Prop)
    fun
      (x :
        ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
                ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
            ℕ)]) ↦
    ‖x‖ ≤ 1 (β := ℚ_[(↑p : ℕ)] → Prop) fun (x : ℚ_[(↑p : ℕ)]) ↦ ‖x‖ ≤ 1

Tactic:
rw [primesEquiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Rat.HeightOneSpectrum.primesEquiv
-- 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 : ℤ_[(↑p : ℕ)]
rw :
  HEq (α :=
    { x :
      ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
              ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
          ℕ)] //
      ‖x‖ ≤ 1 })
    (cast ⋯ x :
      ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
              ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
          ℕ)])
    x
⊢ HEq (α :=
    ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
            ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
        ℕ)])
    (↑(cast ⋯ x) :
      ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes)
              ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
          ℕ)])
    (↑x : ℚ_[(↑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
-- 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 : ℤ_[(↑p : ℕ)]
⊢ HEq (α :=
    { x :
      ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
              ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
          ℕ)] //
      ‖x‖ ≤ 1 })
    (cast ⋯ x :
      ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
              ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
          ℕ)])
    x

Tactic:
cast_heq _ _

Premises used: PadicInt, cast_heq
-- 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 : ℤ_[(↑p : ℕ)]
⊢ HEq (α :=
    { x :
      ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
              ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
          ℕ)] //
      ‖x‖ ≤ 1 })
    (cast ⋯ x :
      ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
              ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
          ℕ)])
    x

Tactic:
exact cast_heq _ _

Premises used: cast_heq
-- 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 rw₁ : ℚ_[(↑p : ℕ)] = ℚ_[(↑p : ℕ)]
⊢ ℚ_[(↑p : ℕ)] =
    ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
            ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
        ℕ)]

Tactic:
rw [primesEquiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Rat.HeightOneSpectrum.primesEquiv
-- 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 rw₁ :
  HEq (α := ℚ_[(↑p : ℕ)] → Prop) fun (x : ℚ_[(↑p : ℕ)]) ↦ ‖x‖ ≤ 1 (β := ℚ_[(↑p : ℕ)] → Prop) fun (x : ℚ_[(↑p : ℕ)]) ↦
    ‖x‖ ≤ 1
⊢ HEq (α := ℚ_[(↑p : ℕ)] → Prop) fun (x : ℚ_[(↑p : ℕ)]) ↦ ‖x‖ ≤ 1 (β :=
    ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
              ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
          ℕ)] →
      Prop)
    fun
      (x :
        ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
                ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
            ℕ)]) ↦
    ‖x‖ ≤ 1

Tactic:
rw [primesEquiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Rat.HeightOneSpectrum.primesEquiv
-- 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))
⊢ 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)) :
          ℕ)])

Tactic:
cast_heq _ _

Premises used: PadicInt, cast_heq
-- 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))
⊢ 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)) :
          ℕ)])

Tactic:
exact cast_heq _ _

Premises used: cast_heq
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
x y : ℤ_[p]
let :
  ∀ (z : ℤ_[p])
    (hz :
      Polynomial.eval x (Polynomial.map (algebraMap R ℤ_[p]) F) -
          Polynomial.eval y (Polynomial.map (algebraMap R ℤ_[p]) F) =
        z * (x - y)),
    ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
          (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
          (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])‖ ≤
      ‖x - y‖
⊢ ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])‖ ≤
    ‖x - y‖

Tactic:
let ⟨z, hz⟩ := (F.map (algebraMap R ℤ_[p])).evalSubFactor x y
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
x y z : ℤ_[p]
hz :
  Polynomial.eval x (Polynomial.map (algebraMap R ℤ_[p]) F) -
      Polynomial.eval y (Polynomial.map (algebraMap R ℤ_[p]) F) =
    z * (x - y)
⊢ HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
      (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
      (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) =
    z * (x - y)

Tactic:
simp only [Polynomial.eval_map_algebraMap] at hz

Premises used: Polynomial.eval_map_algebraMap
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
x y z : ℤ_[p]
hz :
  HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
      (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
      (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) =
    z * (x - y)
⊢ ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])‖ =
    ‖z‖ * ‖x - y‖

Tactic:
simp [hz]
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
x y z : ℤ_[p]
hz :
  HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
      (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
      (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) =
    z * (x - y)
hbc : ‖z‖ ≤ 1
⊢ ‖z‖ * ‖x - y‖ ≤ 1 * ‖x - y‖

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
x y z : ℤ_[p]
hz :
  HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
      (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
      (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) =
    z * (x - y)
⊢ ‖z‖ ≤ 1

Tactic:
apply PadicInt.norm_le_one

Premises used: PadicInt.norm_le_one
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
x y z : ℤ_[p]
hz :
  HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
      (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
      (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) =
    z * (x - y)
⊢ 1 * ‖x - y‖ = ‖x - y‖

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
x y z : ℤ_[p]
hz :
  HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
      (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
      (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) =
    z * (x - y)
x₁ :
  ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])‖ =
    ‖z‖ * ‖x - y‖
x₂ : ‖z‖ * ‖x - y‖ ≤ 1 * ‖x - y‖
x₃ : 1 * ‖x - y‖ = ‖x - y‖
⊢ ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])‖ ≤
    ‖x - y‖

Tactic:
calc
    ‖F.aeval x - F.aeval y‖ = ‖z‖ * ‖x - y‖ := by simp [hz]
    _ ≤ 1 * ‖x - y‖ := by gcongr; apply PadicInt.norm_le_one
    _ = ‖x - y‖ := by simp

Premises used: Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
ncs : CauSeq ℤ_[p] norm
⊢ Tendsto (fun (i : ℕ) ↦ Polynomial.eval ((↑ncs : ℕ → ℤ_[p]) i) F) atTop (𝓝 (Polynomial.eval ncs.lim F))

Tactic:
Filter.Tendsto.comp (@Polynomial.continuousAt _ _ _ _ F _) ncs.tendsto_limit

Premises used: Polynomial.eval, CauSeq.tendsto_limit, Polynomial.continuousAt, Filter.Tendsto.comp