awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a_1 : E
n : ℕ
x : ℤ_[p]
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
a₁ :
  norm.{u_1} (E := BoundedContinuousFunction ℕ E)
      (ZeroAtInftyContinuousMap.toBCF
        (({
              toFun := fun (f : C(ℤ_[p], E)) ↦
                { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                  zero_at_infty' := ⋯ : ℕ →C₀ E },
              map_add' := ⋯, map_smul' := ⋯ : LinearMap (R := ℤ_[p]) (RingHom.id ℤ_[p]) C(ℤ_[p], E) (ℕ →C₀ E) } :
            (a : C(ℤ_[p], E)) → ℕ →C₀ E)
          f)) ≤
    ‖f‖
a₂ :
  ‖f‖ ≤
    norm.{u_1} (E := BoundedContinuousFunction ℕ E)
      (ZeroAtInftyContinuousMap.toBCF
        (({
              toFun := fun (f : C(ℤ_[p], E)) ↦
                { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                  zero_at_infty' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : C(ℤ_[p], E)) → ℕ →C₀ E)
          f))
⊢ norm.{u_1} (E := BoundedContinuousFunction ℕ E)
      (ZeroAtInftyContinuousMap.toBCF
        (({
              toFun := fun (f : C(ℤ_[p], E)) ↦
                { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                  zero_at_infty' := ⋯ : ℕ →C₀ E },
              map_add' := ⋯, map_smul' := ⋯ : LinearMap (R := ℤ_[p]) (RingHom.id ℤ_[p]) C(ℤ_[p], E) (ℕ →C₀ E) } :
            (a : C(ℤ_[p], E)) → ℕ →C₀ E)
          f)) =
    ‖f‖

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a_1 : E
n : ℕ
x : ℤ_[p]
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
⊢ norm.{u_1} (E := BoundedContinuousFunction ℕ E)
      (ZeroAtInftyContinuousMap.toBCF
        (({
              toFun := fun (f : C(ℤ_[p], E)) ↦
                { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                  zero_at_infty' := ⋯ : ℕ →C₀ E },
              map_add' := ⋯, map_smul' := ⋯ : LinearMap (R := ℤ_[p]) (RingHom.id ℤ_[p]) C(ℤ_[p], E) (ℕ →C₀ E) } :
            (a : C(ℤ_[p], E)) → ℕ →C₀ E)
          f)) ≤
    ‖f‖

Tactic:
BoundedContinuousFunction.norm_le_of_nonempty.mpr
        (fun n ↦ norm_fwdDiff_iter_apply_le 1 f 0 n)

Premises used: Iff.mpr, IsUltrametricDist.norm_fwdDiff_iter_apply_le, BoundedContinuousFunction.norm_le_of_nonempty, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a_1 : E
n : ℕ
x : ℤ_[p]
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
⊢ norm.{u_1} (E := BoundedContinuousFunction ℕ E)
      (ZeroAtInftyContinuousMap.toBCF
        (({
              toFun := fun (f : C(ℤ_[p], E)) ↦
                { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                  zero_at_infty' := ⋯ : ℕ →C₀ E },
              map_add' := ⋯, map_smul' := ⋯ : LinearMap (R := ℤ_[p]) (RingHom.id ℤ_[p]) C(ℤ_[p], E) (ℕ →C₀ E) } :
            (a : C(ℤ_[p], E)) → ℕ →C₀ E)
          f)) ≤
    ‖f‖

Tactic:
exact BoundedContinuousFunction.norm_le_of_nonempty.mpr
        (fun n ↦ norm_fwdDiff_iter_apply_le 1 f 0 n)

Premises used: Iff.mpr, BoundedContinuousFunction.norm_le_of_nonempty
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a_1 : E
n : ℕ
x : ℤ_[p]
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
a₁ :
  norm.{u_1} (E := C(ℤ_[p], E)) (∑' (b : ℕ), mahlerTerm (Δ_[1]^[b] (⇑f : (a : ℤ_[p]) → E) 0) b) ≤
    norm.{u_1} (E := BoundedContinuousFunction ℕ E)
      (ZeroAtInftyContinuousMap.toBCF
        (({
              toFun := fun (f : C(ℤ_[p], E)) ↦
                { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                  zero_at_infty' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : C(ℤ_[p], E)) → ℕ →C₀ E)
          (∑' (b : ℕ), mahlerTerm (Δ_[1]^[b] (⇑f : (a : ℤ_[p]) → E) 0) b)))
⊢ ‖f‖ ≤
    norm.{u_1} (E := BoundedContinuousFunction ℕ E)
      (ZeroAtInftyContinuousMap.toBCF
        (({
              toFun := fun (f : C(ℤ_[p], E)) ↦
                { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                  zero_at_infty' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : C(ℤ_[p], E)) → ℕ →C₀ E)
          f))

Tactic:
rw [← (hasSum_mahler f).tsum_eq]

Premises used: HasSum.tsum_eq, PadicInt.hasSum_mahler
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a_1 : E
n : ℕ
x : ℤ_[p]
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
⊢ norm.{u_1} (E := C(ℤ_[p], E)) (∑' (b : ℕ), mahlerTerm (Δ_[1]^[b] (⇑f : (a : ℤ_[p]) → E) 0) b) ≤
    norm.{u_1} (E := BoundedContinuousFunction ℕ E)
      (ZeroAtInftyContinuousMap.toBCF
        (({
              toFun := fun (f : C(ℤ_[p], E)) ↦
                { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                  zero_at_infty' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : C(ℤ_[p], E)) → ℕ →C₀ E)
          (∑' (b : ℕ), mahlerTerm (Δ_[1]^[b] (⇑f : (a : ℤ_[p]) → E) 0) b)))

Tactic:
(norm_tsum_le _).trans (ciSup_le fun n ↦ ?_)

Premises used: IsUltrametricDist.norm_tsum_le, setOf, LE.le.trans, ciSup_le
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a_1 : E
n : ℕ
x : ℤ_[p]
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
a₁ :
  ∀ (n : ℕ),
    norm (E := C(ℤ_[p], E)) (mahlerTerm (Δ_[1]^[n] (⇑f : (a : ℤ_[p]) → E) 0) n : C(ℤ_[p], E)) ≤
      norm.{u_1} (E := BoundedContinuousFunction ℕ E)
        (ZeroAtInftyContinuousMap.toBCF
          (({
                toFun := fun (f : C(ℤ_[p], E)) ↦
                  { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                    zero_at_infty' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ } :
              (a : C(ℤ_[p], E)) → ℕ →C₀ E)
            (∑' (b : ℕ), mahlerTerm (Δ_[1]^[b] (⇑f : (a : ℤ_[p]) → E) 0) b)))
⊢ norm.{u_1} (E := C(ℤ_[p], E)) (∑' (b : ℕ), mahlerTerm (Δ_[1]^[b] (⇑f : (a : ℤ_[p]) → E) 0) b) ≤
    norm.{u_1} (E := BoundedContinuousFunction ℕ E)
      (ZeroAtInftyContinuousMap.toBCF
        (({
              toFun := fun (f : C(ℤ_[p], E)) ↦
                { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                  zero_at_infty' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : C(ℤ_[p], E)) → ℕ →C₀ E)
          (∑' (b : ℕ), mahlerTerm (Δ_[1]^[b] (⇑f : (a : ℤ_[p]) → E) 0) b)))

Tactic:
refine (norm_tsum_le _).trans (ciSup_le fun n ↦ ?_)

Premises used: IsUltrametricDist.norm_tsum_le, LE.le.trans, ciSup_le
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a_1 : E
n_1 : ℕ
x : ℤ_[p]
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
n : ℕ
⊢ norm (E := C(ℤ_[p], E)) (mahlerTerm (Δ_[1]^[n] (⇑f : (a : ℤ_[p]) → E) 0) n : C(ℤ_[p], E)) ≤
    norm.{u_1} (E := BoundedContinuousFunction ℕ E)
      (ZeroAtInftyContinuousMap.toBCF
        (({
              toFun := fun (f : C(ℤ_[p], E)) ↦
                { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                  zero_at_infty' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : C(ℤ_[p], E)) → ℕ →C₀ E)
          (∑' (b : ℕ), mahlerTerm (Δ_[1]^[b] (⇑f : (a : ℤ_[p]) → E) 0) b)))

Tactic:
le_trans (le_of_eq ?_) (BoundedContinuousFunction.norm_coe_le_norm _ n)

Premises used: BoundedContinuousFunction.norm_coe_le_norm, le_of_eq, le_trans
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a_1 : E
n_1 : ℕ
x : ℤ_[p]
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
n : ℕ
a₁ :
  norm (E := C(ℤ_[p], E)) (mahlerTerm (Δ_[1]^[n] (⇑f : (a : ℤ_[p]) → E) 0) n : C(ℤ_[p], E)) =
    norm.{u_1} (E := E)
      ((ZeroAtInftyContinuousMap.toBCF
              (({
                    toFun := fun (f : C(ℤ_[p], E)) ↦
                      { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                        zero_at_infty' := ⋯ },
                    map_add' := ⋯, map_smul' := ⋯ } :
                  (a : C(ℤ_[p], E)) → ℕ →C₀ E)
                (∑' (b : ℕ), mahlerTerm (Δ_[1]^[b] (⇑f : (a : ℤ_[p]) → E) 0) b)) :
            (a : ℕ) → E)
          n :
        E)
⊢ norm (E := C(ℤ_[p], E)) (mahlerTerm (Δ_[1]^[n] (⇑f : (a : ℤ_[p]) → E) 0) n : C(ℤ_[p], E)) ≤
    norm.{u_1} (E := BoundedContinuousFunction ℕ E)
      (ZeroAtInftyContinuousMap.toBCF
        (({
              toFun := fun (f : C(ℤ_[p], E)) ↦
                { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                  zero_at_infty' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : C(ℤ_[p], E)) → ℕ →C₀ E)
          (∑' (b : ℕ), mahlerTerm (Δ_[1]^[b] (⇑f : (a : ℤ_[p]) → E) 0) b)))

Tactic:
refine le_trans (le_of_eq ?_) (BoundedContinuousFunction.norm_coe_le_norm _ n)

Premises used: BoundedContinuousFunction.norm_coe_le_norm, le_of_eq, le_trans
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
a_1 : E
n_1 : ℕ
x : ℤ_[p]
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
n : ℕ
⊢ norm (E := C(ℤ_[p], E)) (mahlerTerm (Δ_[1]^[n] (⇑f : (a : ℤ_[p]) → E) 0) n : C(ℤ_[p], E)) =
    norm.{u_1} (E := E)
      ((ZeroAtInftyContinuousMap.toBCF
              (({
                    toFun := fun (f : C(ℤ_[p], E)) ↦
                      { toFun := fun (x : ℕ) ↦ Δ_[1]^[x] (⇑f : (a : ℤ_[p]) → E) 0, continuous_toFun := ⋯,
                        zero_at_infty' := ⋯ },
                    map_add' := ⋯, map_smul' := ⋯ } :
                  (a : C(ℤ_[p], E)) → ℕ →C₀ E)
                (∑' (b : ℕ), mahlerTerm (Δ_[1]^[b] (⇑f : (a : ℤ_[p]) → E) 0) b)) :
            (a : ℕ) → E)
          n :
        E)

Tactic:
simp [(hasSum_mahler f).tsum_eq]

Premises used: HasSum.tsum_eq, PadicInt.hasSum_mahler
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
f : C(ℤ_[p], E)
⊢ Eq (α := (a : ℕ) → E)
    (⇑(((mahlerEquiv E : C(ℤ_[p], E) ≃ₗᵢ[ℤ_[p]] ℕ →C₀ E) : (a : C(ℤ_[p], E)) → ℕ →C₀ E) f : ℕ →C₀ E) : (a : ℕ) → E)
    fun (n : ℕ) ↦ Δ_[1]^[n] (⇑f : (a : ℤ_[p]) → E) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.MahlerBasis
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : Module ℤ_[p] E
inst_2 : IsBoundedSMul ℤ_[p] E
inst_3 : IsUltrametricDist E
inst_4 : CompleteSpace E
a : ℕ →C₀ E
⊢ Eq (α := C(ℤ_[p], E))
    (((LinearIsometryEquiv.symm (mahlerEquiv E) : (ℕ →C₀ E) ≃ₗᵢ[ℤ_[p]] C(ℤ_[p], E)) : (a : ℕ →C₀ E) → C(ℤ_[p], E)) a :
      C(ℤ_[p], E))
    (mahlerSeries (⇑a : (a : ℕ) → E) : C(ℤ_[p], E))

Tactic:
rfl

Premises used: PadicInt.mahlerSeries, tsum, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ (↑x : ℚ_[p]) = (↑y : ℚ_[p]) → x = y

Tactic:
Subtype.ext

Premises used: PadicInt, Subtype.ext
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ Membership.mem (γ := Set ℚ_[p]) {x : ℚ_[p] | ‖x‖ ≤ 1} 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ Membership.mem (γ := Set ℚ_[p]) {x : ℚ_[p] | ‖x‖ ≤ 1} 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ Membership.mem (γ := Subring ℚ_[p]) (subring p) x ↔ ‖x‖ ≤ 1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h : norm (E := ℚ_[p]) 0 ≤ 1
⊢ Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) 0 h = 0

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
⊢ (↑(z1 + z2) : ℚ_[p]) = (↑z1 : ℚ_[p]) + (↑z2 : ℚ_[p])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
⊢ (↑(z1 * z2) : ℚ_[p]) = (↑z1 : ℚ_[p]) * (↑z2 : ℚ_[p])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 : ℤ_[p]
⊢ (↑(-z1) : ℚ_[p]) = -(↑z1 : ℚ_[p])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
⊢ (↑(z1 - z2) : ℚ_[p]) = (↑z1 : ℚ_[p]) - (↑z2 : ℚ_[p])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := ℚ_[p]) (↑1 : ℚ_[p]) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := ℚ_[p]) (↑0 : ℚ_[p]) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
rw : (↑x : ℚ_[p]) = (↑0 : ℚ_[p]) ↔ x = 0
rw₁ rw₂ : x = 0 ↔ x = 0
⊢ (↑x : ℚ_[p]) = 0 ↔ x = 0

Tactic:
rw [← coe_zero, Subtype.coe_inj]

Premises used: PadicInt.coe_zero, Subtype.coe_inj
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ (↑x : ℚ_[p]) ≠ 0 ↔ x ≠ 0

Tactic:
coe_eq_zero.not

Premises used: PadicInt.coe_eq_zero, Iff.not
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Eq (α := ℚ_[p]) (↑(↑n : ℤ_[p]) : ℚ_[p]) (↑n : ℚ_[p])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ Eq (α := ℚ_[p]) (↑(↑z : ℤ_[p]) : ℚ_[p]) (↑z : ℚ_[p])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ (↑(x ^ n) : ℚ_[p]) = (↑x : ℚ_[p]) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ_[p]
⊢ Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (↑k : ℚ_[p]) ⋯ = k

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
s : Finset α
f : α → ℤ_[p]
⊢ Eq (α := ℚ_[p]) (↑(∑ z ∈ s, f z) : ℚ_[p]) (∑ z ∈ s, (↑(f z) : ℚ_[p]))

Tactic:
simp [← Coe.ringHom_apply, map_sum PadicInt.Coe.ringHom f s]

Premises used: PadicInt.Coe.ringHom, PadicInt.Coe.ringHom_apply, map_sum
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsOpenEmbedding (X := { x : ℚ_[p] // ‖x‖ ≤ 1 }) (Subtype.val (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1))

Tactic:
(?_ : IsOpen {y : ℚ_[p] | ‖y‖ ≤ 1}).isOpenEmbedding_subtypeVal

Premises used: IsOpen.isOpenEmbedding_subtypeVal, Set.Mem
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
refine : IsOpen (X := ℚ_[p]) {y : ℚ_[p] | ‖y‖ ≤ 1}
⊢ IsOpenEmbedding (X := { x : ℚ_[p] // ‖x‖ ≤ 1 }) (Subtype.val (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1))

Tactic:
refine (?_ : IsOpen {y : ℚ_[p] | ‖y‖ ≤ 1}).isOpenEmbedding_subtypeVal

Premises used: IsOpen.isOpenEmbedding_subtypeVal
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsOpen (X := ℚ_[p]) {y : ℚ_[p] | ‖y‖ ≤ 1}

Tactic:
simpa only [Metric.closedBall, dist_eq_norm_sub, sub_zero] using
    IsUltrametricDist.isOpen_closedBall (0 : ℚ_[p]) one_ne_zero

Premises used: dist_eq_norm_sub, sub_zero, IsUltrametricDist.isOpen_closedBall, Metric.closedBall, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
k : ℚ_[p]
property : ‖k‖ ≤ 1
h : ‖k‖ = 1
⊢ ‖k⁻¹‖ ≤ 1

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
m n : ℕ
h : Eq (α := ℤ_[p]) (↑m : ℤ_[p]) (↑n : ℤ_[p])
⊢ Eq (α := ℚ_[p]) (↑(↑m : ℤ_[p]) : ℚ_[p]) (↑(↑n : ℤ_[p]) : ℚ_[p])

Tactic:
rw [Subtype.ext_iff] at h

Premises used: Subtype.ext_iff
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
m n : ℕ
h : Eq (α := ℚ_[p]) (↑(↑m : ℤ_[p]) : ℚ_[p]) (↑(↑n : ℤ_[p]) : ℚ_[p])
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℚ_[p]) (↑m : ℚ_[p]) (↑n : ℚ_[p])
⊢ Eq (α := ℚ_[p]) (↑m : ℚ_[p]) (↑n : ℚ_[p])

Tactic:
norm_cast at h
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ
⊢ Eq (α := ℤ_[p]) (↑z1 : ℤ_[p]) (↑z2 : ℤ_[p]) ↔ z1 = z2

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun (n : ℕ) ↦ (↑(seq n) : ℚ)
pos :
  ∀ (hne : Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (n : ℕ) ↦ (↑(seq n) : ℚ)) h ≈ 0),
    LE.le (α := ℝ) (↑0 : ℝ) 1
neg :
  ∀ (hne : ¬Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (n : ℕ) ↦ (↑(seq n) : ℚ)) h ≈ 0),
    LE.le (α := ℝ)
      (↑(padicNorm p
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (n : ℕ) ↦ (↑(seq n) : ℚ)) h) : ℕ → ℚ)
              (PadicSeq.stationaryPoint hne))) :
        ℝ)
      1
⊢ LE.le (α := ℝ)
    (↑(if hf : Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (n : ℕ) ↦ (↑(seq n) : ℚ)) h ≈ 0 then 0
        else
          padicNorm p
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (n : ℕ) ↦ (↑(seq n) : ℚ)) h) : ℕ → ℚ)
              (PadicSeq.stationaryPoint hf))) :
      ℝ)
    1

Tactic:
split_ifs with hne
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun (n : ℕ) ↦ (↑(seq n) : ℚ)
hne : Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (n : ℕ) ↦ (↑(seq n) : ℚ)) h ≈ 0
pos pos₁ pos₂ pos₃ : LE.le (α := ℕ) 0 1
⊢ LE.le (α := ℝ) (↑0 : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun (n : ℕ) ↦ (↑(seq n) : ℚ)
hne : ¬Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (n : ℕ) ↦ (↑(seq n) : ℚ)) h ≈ 0
neg :
  padicNorm p
      ((↑(Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (n : ℕ) ↦ (↑(seq n) : ℚ)) h) : ℕ → ℚ)
        (PadicSeq.stationaryPoint hne)) ≤
    1
⊢ LE.le (α := ℝ)
    (↑(padicNorm p
          ((↑(Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (n : ℕ) ↦ (↑(seq n) : ℚ)) h) : ℕ → ℚ)
            (PadicSeq.stationaryPoint hne))) :
      ℝ)
    1

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun (n : ℕ) ↦ (↑(seq n) : ℚ)
hne : ¬Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (n : ℕ) ↦ (↑(seq n) : ℚ)) h ≈ 0
⊢ padicNorm p
      ((↑(Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (n : ℕ) ↦ (↑(seq n) : ℚ)) h) : ℕ → ℚ)
        (PadicSeq.stationaryPoint hne)) ≤
    1

Tactic:
apply padicNorm.of_int

Premises used: padicNorm.of_int
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ IsUltrametricDist ℤ_[p]

Tactic:
IsUltrametricDist.subtype _

Premises used: PadicInt, IsUltrametricDist.subtype
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ CompleteSpace ℤ_[p]

Tactic:
have : IsClosed { x : ℚ_[p] | ‖x‖ ≤ 1 } := isClosed_le continuous_norm continuous_const
  this.completeSpace_coe

Premises used: PadicInt, Set.Mem, continuous_const, isClosed_le, IsClosed.completeSpace_coe, continuous_norm
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ‖z‖ = ‖(↑z : ℚ_[p])‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y_1 : ℤ_[p]
x : ℚ_[p]
hx : ‖x‖ ≤ 1
y : ℚ_[p]
hy : ‖y‖ ≤ 1
⊢ dist (α := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) x hx)
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) y hy) =
    ‖HAdd.hAdd (α := ℤ_[p]) (-Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) x hx)
        (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) y hy)‖

Tactic:
dist_eq_norm_neg_add x y

Premises used: dist_eq_norm_neg_add
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y_1 : ℤ_[p]
x : ℚ_[p]
hx : ‖x‖ ≤ 1
y : ℚ_[p]
hy : ‖y‖ ≤ 1
⊢ dist (α := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) x hx)
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) y hy) =
    ‖HAdd.hAdd (α := ℤ_[p]) (-Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) x hx)
        (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) y hy)‖

Tactic:
exact dist_eq_norm_neg_add x y

Premises used: dist_eq_norm_neg_add
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ ∀ (a b : ℤ_[p]), ‖a * b‖ ≤ ‖a‖ * ‖b‖

Tactic:
simp [norm_def]

Premises used: PadicInt.norm_def
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ NormOneClass ℤ_[p]

Tactic:
⟨norm_def.trans norm_one⟩

Premises used: NormOneClass.mk, NormOneClass.norm_one, PadicInt.norm_def, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y_1 x y : ℤ_[p]
⊢ ‖x * y‖ = ‖x‖ * ‖y‖

Tactic:
simp [norm_def]

Premises used: PadicInt.norm_def
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ IsDomain ℤ_[p]

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ‖z‖ ≤ 1

Tactic:
z.2

Premises used: Subtype.property
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℤ_[p]
⊢ ‖q + r‖ ≤ max ‖q‖ ‖r‖

Tactic:
Padic.nonarchimedean _ _

Premises used: Padic.nonarchimedean
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℤ_[p]
⊢ ‖q‖ ≠ ‖r‖ → ‖q + r‖ = max ‖q‖ ‖r‖

Tactic:
Padic.add_eq_max_of_ne

Premises used: Padic.add_eq_max_of_ne
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
rw : ‖z2‖ ≤ max ‖z1‖ ‖z2‖
⊢ ‖z2‖ ≤ ‖z1 + z2‖

Tactic:
rw [norm_add_eq_max_of_ne hne]

Premises used: PadicInt.norm_add_eq_max_of_ne
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z2‖ ≤ max ‖z1‖ ‖z2‖

Tactic:
apply le_max_right

Premises used: le_max_right
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
rw : ‖z1‖ ≤ max ‖z1‖ ‖z2‖
⊢ ‖z1‖ ≤ ‖z1 + z2‖

Tactic:
rw [norm_add_eq_max_of_ne hne]

Premises used: PadicInt.norm_add_eq_max_of_ne