awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
a b : ℤ_[p]
F : C(ℤ_[p], R) := mahlerSeries fun (x : ℕ) ↦ r ^ x
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range (n + 1), n.choose i • r ^ i)
    (∑ m ∈ Finset.range (n + 1), r ^ m * HPow.hPow (α := R) 1 (n - m) * (↑(n.choose m) : R))

Tactic:
Finset.sum_congr rfl fun i hi ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
a b : ℤ_[p]
F : C(ℤ_[p], R) := mahlerSeries fun (x : ℕ) ↦ r ^ x
n : ℕ
refine :
  ∀ (i : ℕ) (hi : i ∈ Finset.range (n + 1)),
    n.choose i • r ^ i = r ^ i * HPow.hPow (α := R) 1 (n - i) * (↑(n.choose i) : R)
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range (n + 1), n.choose i • r ^ i)
    (∑ m ∈ Finset.range (n + 1), r ^ m * HPow.hPow (α := R) 1 (n - m) * (↑(n.choose m) : R))

Tactic:
refine Finset.sum_congr rfl fun i hi ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
a b : ℤ_[p]
F : C(ℤ_[p], R) := mahlerSeries fun (x : ℕ) ↦ r ^ x
n i : ℕ
hi : i ∈ Finset.range (n + 1)
rw : n.choose i • r ^ i = r ^ i * 1 * (↑(n.choose i) : R)
rw₁ : n.choose i • r ^ i = r ^ i * (↑(n.choose i) : R)
rw₂ : (↑(n.choose i) : R) * r ^ i = r ^ i * (↑(n.choose i) : R)
rw₃ rw₄ : r ^ i * (↑(n.choose i) : R) = r ^ i * (↑(n.choose i) : R)
⊢ n.choose i • r ^ i = r ^ i * HPow.hPow (α := R) 1 (n - i) * (↑(n.choose i) : R)

Tactic:
rw [one_pow, mul_one, nsmul_eq_mul, Nat.cast_comm]

Premises used: Nat.cast_comm, one_pow, nsmul_eq_mul, mul_one
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
a b : ℤ_[p]
F : C(ℤ_[p], R) := mahlerSeries fun (x : ℕ) ↦ r ^ x
⊢ ∀ (n : ℕ), (F : (a : ℤ_[p]) → R) (↑n : ℤ_[p]) = (r + 1) ^ n

Tactic:
have hF (n : ℕ) : F n = (r + 1) ^ n := by
      rw [mahlerSeries_apply_nat hr le_rfl, (Commute.one_right _).add_pow]
      refine Finset.sum_congr rfl fun i hi ↦ ?_
      rw [one_pow, mul_one, nsmul_eq_mul, Nat.cast_comm]
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
a b : ℤ_[p]
F : C(ℤ_[p], R) := mahlerSeries fun (x : ℕ) ↦ r ^ x
hF : ∀ (n : ℕ), (F : (a : ℤ_[p]) → R) (↑n : ℤ_[p]) = (r + 1) ^ n
⊢ (F : (a : ℤ_[p]) → R) (a + b) =
    HMul.hMul (α := R) (β := R) ((F : (a : ℤ_[p]) → R) a : R) ((F : (a : ℤ_[p]) → R) b : R)

Tactic:
congr_fun ((denseRange_natCast.prodMap denseRange_natCast).equalizer
      ((map_continuous F).comp continuous_add)
      (continuous_mul.comp (map_continuous <| F.prodMap F)) (funext fun ⟨m, n⟩ ↦ ?_)) (a, b)

Premises used: DenseRange.equalizer, HMul.hMul, continuous_mul, DenseRange.prodMap, Continuous.comp, _private.0.PadicInt.addChar_of_value_at_one.match_1, Function.comp, Prod.mk, PadicInt.denseRange_natCast, Prod.map, Nat.cast, Prod.fst, funext, HAdd.hAdd, continuous_add, ContinuousMap.prodMap, ContinuousMapClass.map_continuous, congr_fun, Eq, Prod.snd, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
a b : ℤ_[p]
F : C(ℤ_[p], R) := mahlerSeries fun (x : ℕ) ↦ r ^ x
hF : ∀ (n : ℕ), (F : (a : ℤ_[p]) → R) (↑n : ℤ_[p]) = (r + 1) ^ n
refine :
  ∀ (x : ℕ × ℕ) (m n : ℕ),
    Eq (α := R)
      (Function.comp (β := ℤ_[p] × ℤ_[p])
        (Function.comp (β := ℤ_[p]) (⇑F : (a : ℤ_[p]) → R) fun (p_1 : ℤ_[p] × ℤ_[p]) ↦ p_1.1 + p_1.2)
        (Prod.map Nat.cast Nat.cast) (m, n))
      (Function.comp (β := ℤ_[p] × ℤ_[p])
        ((fun (p : R × R) ↦ p.1 * p.2) ∘ (⇑(F.prodMap F) : (a : ℤ_[p] × ℤ_[p]) → R × R)) (Prod.map Nat.cast Nat.cast)
        (m, n))
⊢ (F : (a : ℤ_[p]) → R) (a + b) =
    HMul.hMul (α := R) (β := R) ((F : (a : ℤ_[p]) → R) a : R) ((F : (a : ℤ_[p]) → R) b : R)

Tactic:
refine congr_fun ((denseRange_natCast.prodMap denseRange_natCast).equalizer
      ((map_continuous F).comp continuous_add)
      (continuous_mul.comp (map_continuous <| F.prodMap F)) (funext fun ⟨m, n⟩ ↦ ?_)) (a, b)

Premises used: DenseRange.equalizer, HMul.hMul, continuous_mul, DenseRange.prodMap, Continuous.comp, _private.0.PadicInt.addChar_of_value_at_one.match_1, Function.comp, Prod.mk, PadicInt.denseRange_natCast, Prod.map, Nat.cast, Prod.fst, funext, HAdd.hAdd, continuous_add, ContinuousMap.prodMap, ContinuousMapClass.map_continuous, congr_fun, Eq, Prod.snd, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
a b : ℤ_[p]
F : C(ℤ_[p], R) := mahlerSeries fun (x : ℕ) ↦ r ^ x
hF : ∀ (n : ℕ), (F : (a : ℤ_[p]) → R) (↑n : ℤ_[p]) = (r + 1) ^ n
x : ℕ × ℕ
m n : ℕ
⊢ Eq (α := R)
    (Function.comp (β := ℤ_[p] × ℤ_[p])
      (Function.comp (β := ℤ_[p]) (⇑F : (a : ℤ_[p]) → R) fun (p_1 : ℤ_[p] × ℤ_[p]) ↦ p_1.1 + p_1.2)
      (Prod.map Nat.cast Nat.cast) (m, n))
    (Function.comp (β := ℤ_[p] × ℤ_[p]) ((fun (p : R × R) ↦ p.1 * p.2) ∘ (⇑(F.prodMap F) : (a : ℤ_[p] × ℤ_[p]) → R × R))
      (Prod.map Nat.cast Nat.cast) (m, n))

Tactic:
simp [← Nat.cast_add, hF, ContinuousMap.prodMap_apply, pow_add]

Premises used: pow_add, ContinuousMap.prodMap_apply, Nat.cast_add
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑(addChar_of_value_at_one r hr) : (a : ℤ_[p]) → R)

Tactic:
map_continuous (mahlerSeries (r ^ ·))

Premises used: PadicInt.mahlerSeries, HPow.hPow, ContinuousMapClass.map_continuous
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
⊢ Eq (α := (a : ℤ_[p]) → R) (⇑(addChar_of_value_at_one r hr) : (a : ℤ_[p]) → R)
    (⇑(mahlerSeries fun (x : ℕ) ↦ r ^ x) : (a : ℤ_[p]) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
change : (mahlerSeries fun (x : ℕ) ↦ r ^ x : (a : ℤ_[p]) → R) (↑1 : ℤ_[p]) = 1 + r
⊢ (addChar_of_value_at_one r hr : (a : ℤ_[p]) → R) 1 = 1 + r

Tactic:
change mahlerSeries (r ^ ·) ↑(1 : ℕ) = _

Premises used: Nat.cast, PadicInt.mahlerSeries, HPow.hPow, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
rw : ∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 1 1), Nat.choose 1 i • r ^ i = 1 + r
rw₁ : ∑ x ∈ Finset.range 1, Nat.choose 1 x • r ^ x + Nat.choose 1 1 • HPow.hPow (β := ℕ) r 1 = 1 + r
rw₂ : Nat.choose 1 0 • HPow.hPow (β := ℕ) r 0 + Nat.choose 1 1 • HPow.hPow (β := ℕ) r 1 = 1 + r
rw₃ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) r 0) + Nat.choose 1 1 • HPow.hPow (β := ℕ) r 1 = 1 + r
rw₄ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) r 0) + HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) r 1) = 1 + r
rw₅ : HPow.hPow (β := ℕ) r 0 + HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) r 1) = 1 + r
rw₆ : HPow.hPow (β := ℕ) r 0 + HPow.hPow (β := ℕ) r 1 = 1 + r
rw₇ : 1 + HPow.hPow (β := ℕ) r 1 = 1 + r
rw₈ rw₉ : 1 + r = 1 + r
⊢ (mahlerSeries fun (x : ℕ) ↦ r ^ x : (a : ℤ_[p]) → R) (↑1 : ℤ_[p]) = 1 + r

Tactic:
rw [mahlerSeries_apply_nat hr le_rfl, Finset.sum_range_succ, Finset.sum_range_one,
    Nat.choose_zero_right, Nat.choose_self, one_smul, one_smul, pow_zero, pow_one]

Premises used: le_rfl, PadicInt.mahlerSeries_apply_nat, Finset.sum_range_one, pow_zero, one_smul, pow_one, Finset.sum_range_succ, Nat.choose_zero_right, Nat.choose_self
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
κ : AddChar ℤ_[p] R
hκ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R)
hκ' : (κ : (a : ℤ_[p]) → R) 1 = 1 + r
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑(addChar_of_value_at_one r hr) : (a : ℤ_[p]) → R)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
κ : AddChar ℤ_[p] R
hκ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R)
hκ' : (κ : (a : ℤ_[p]) → R) 1 = 1 + r
⊢ Eq (α := R) ((κ : (a : ℤ_[p]) → R) 1 : R) ((addChar_of_value_at_one r hr : (a : ℤ_[p]) → R) 1 : R)

Tactic:
simp [hκ']
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
x : { κ : AddChar ℤ_[p] R // Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R) }
κ : AddChar ℤ_[p] R
hκ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R)
⊢ (κ : (a : ℤ_[p]) → R) 1 = 1 + HSub.hSub (α := R) (β := R) ((κ : (a : ℤ_[p]) → R) 1 : R) (1 : R)

Tactic:
abel
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
x : { κ : AddChar ℤ_[p] R // Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R) }
κ : AddChar ℤ_[p] R
hκ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R)
⊢ Eq (α :=
    { κ : AddChar ℤ_[p] R //
      Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R) })
    ((fun (x : { r : R // Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0) }) ↦
        (match (motive :=
            { r : R // Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0) } →
              { κ : AddChar ℤ_[p] R //
                Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R) })
            x with
          | ⟨r, hr⟩ =>
            Subtype.mk (p := fun (κ : AddChar ℤ_[p] R) ↦
              Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R))
              (addChar_of_value_at_one r hr) ⋯ :
          { κ : AddChar ℤ_[p] R //
            Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R) }))
      ((fun
            (x :
              { κ : AddChar ℤ_[p] R //
                Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R) }) ↦
          (match (motive :=
              { κ : AddChar ℤ_[p] R //
                  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R) } →
                { r : R // Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0) })
              x with
            | ⟨κ, hκ⟩ =>
              Subtype.mk (p := fun (r : R) ↦ Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0))
                (HSub.hSub (α := R) (β := R) ((κ : (a : ℤ_[p]) → R) 1 : R) (1 : R)) ⋯ :
            { r : R // Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0) }))
        (Subtype.mk (p := fun (κ : AddChar ℤ_[p] R) ↦
          Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R)) κ hκ)))
    (Subtype.mk (p := fun (κ : AddChar ℤ_[p] R) ↦
      Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R)) κ hκ)

Tactic:
simpa using (eq_addChar_of_value_at_one _ hκ (by abel)).symm

Premises used: PadicInt.eq_addChar_of_value_at_one, Eq.symm
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
x : { r : R // Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0) }
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
⊢ Eq (α := { r : R // Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0) })
    ((fun
          (x :
            { κ : AddChar ℤ_[p] R //
              Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R) }) ↦
        (match (motive :=
            { κ : AddChar ℤ_[p] R //
                Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R) } →
              { r : R // Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0) })
            x with
          | ⟨κ, hκ⟩ =>
            Subtype.mk (p := fun (r : R) ↦ Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0))
              (HSub.hSub (α := R) (β := R) ((κ : (a : ℤ_[p]) → R) 1 : R) (1 : R)) ⋯ :
          { r : R // Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0) }))
      ((fun (x : { r : R // Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0) }) ↦
          (match (motive :=
              { r : R // Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0) } →
                { κ : AddChar ℤ_[p] R //
                  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R) })
              x with
            | ⟨r, hr⟩ =>
              Subtype.mk (p := fun (κ : AddChar ℤ_[p] R) ↦
                Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R))
                (addChar_of_value_at_one r hr) ⋯ :
            { κ : AddChar ℤ_[p] R //
              Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R) }))
        (Subtype.mk (p := fun (r : R) ↦ Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)) r hr)))
    (Subtype.mk (p := fun (r : R) ↦ Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)) r hr)

Tactic:
simp [addChar_of_value_at_one_def hr]

Premises used: PadicInt.addChar_of_value_at_one_def
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
κ : AddChar ℤ_[p] R
hκ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R)
⊢ (↑((continuousAddCharEquiv p R :
            (a :
                { κ : AddChar ℤ_[p] R //
                  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R) }) →
              { r : R // Tendsto (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0) })
          (Subtype.mk (p := fun (κ : AddChar ℤ_[p] R) ↦
            Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R)) κ hκ)) :
      R) =
    HSub.hSub (α := R) (β := R) ((κ : (a : ℤ_[p]) → R) 1 : R) (1 : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
⊢ Eq (α := AddChar ℤ_[p] R)
    (↑((Equiv.symm (continuousAddCharEquiv p R) :
            (a : { r : R // Tendsto (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0) }) →
              { κ : AddChar ℤ_[p] R //
                Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R) })
          (Subtype.mk (p := fun (r : R) ↦ Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)) r hr)) :
      AddChar ℤ_[p] R)
    (addChar_of_value_at_one r hr)

Tactic:
rfl

Premises used: PadicInt.addChar_of_value_at_one, rfl
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
inst_6 : NormMulClass R
⊢ Eq.{max 1 (u_1 + 1)} (α := R → Prop) (fun (r : R) ↦ Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0))
    fun (r : R) ↦ ‖r‖ < 1

Tactic:
simp only [tendsto_pow_atTop_nhds_zero_iff_norm_lt_one]

Premises used: tendsto_pow_atTop_nhds_zero_iff_norm_lt_one
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
inst_6 : NormMulClass R
κ : AddChar ℤ_[p] R
hκ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R)
⊢ (↑((continuousAddCharEquiv_of_norm_mul p R :
            (a :
                { κ : AddChar ℤ_[p] R //
                  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R) }) →
              { r : R // ‖r‖ < 1 })
          (Subtype.mk (p := fun (κ : AddChar ℤ_[p] R) ↦
            Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R)) κ hκ)) :
      R) =
    HSub.hSub (α := R) (β := R) ((κ : (a : ℤ_[p]) → R) 1 : R) (1 : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
inst_6 : NormMulClass R
r : R
hr : ‖r‖ < 1
⊢ Eq (α := AddChar ℤ_[p] R)
    (↑((Equiv.symm (continuousAddCharEquiv_of_norm_mul p R) :
            (a : { r : R // ‖r‖ < 1 }) →
              { κ : AddChar ℤ_[p] R //
                Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R) })
          (Subtype.mk (p := fun (r : R) ↦ ‖r‖ < 1) r hr)) :
      AddChar ℤ_[p] R)
    (addChar_of_value_at_one r ⋯)

Tactic:
rfl

Premises used: PadicInt.addChar_of_value_at_one, rfl
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Algebra.IsAlgebraic ℚ_[p] (PadicAlgCl p)

Tactic:
AlgebraicClosure.isAlgebraic _

Premises used: AlgebraicClosure.isAlgebraic
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Eq (α := ℚ_[p] → PadicAlgCl p) Coe.coe (⇑(algebraMap ℚ_[p] (PadicAlgCl p)) : (a : ℚ_[p]) → PadicAlgCl p)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsNonarchimedean (α := PadicAlgCl p) Norm.norm

Tactic:
isNonarchimedean_spectralNorm (K := ℚ_[p]) (L := PadicAlgCl p)

Premises used: iSup, spectralNorm, isNonarchimedean_spectralNorm, spectralValue
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : PadicAlgCl p
⊢ spectralNorm ℚ_[p] (PadicAlgCl p) x = ‖x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ Norm.norm (E := PadicAlgCl p) ((algebraMap ℚ_[p] (PadicAlgCl p) : (a : ℚ_[p]) → PadicAlgCl p) x : PadicAlgCl p) = ‖x‖

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsUltrametricDist (PadicAlgCl p)

Tactic:
IsUltrametricDist.isUltrametricDist_of_forall_norm_add_le_max_norm (PadicAlgCl.isNonarchimedean p)

Premises used: IsUltrametricDist.isUltrametricDist_of_forall_norm_add_le_max_norm, PadicAlgCl.isNonarchimedean
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : PadicAlgCl p
⊢ (Valued.v : (a : PadicAlgCl p) → ℝ≥0) x = ‖x‖₊

Tactic:
rfl

Premises used: NNReal.mk, rfl
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : PadicAlgCl p
⊢ (↑((Valued.v : (a : PadicAlgCl p) → ℝ≥0) x) : ℝ) = ‖x‖

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a :
  (↑((Valued.v : (a : PadicAlgCl p) → ℝ≥0)
          ((algebraMap ℚ_[p] (PadicAlgCl p) : (a : ℚ_[p]) → PadicAlgCl p) (↑p : ℚ_[p]))) :
      ℝ) =
    (↑(HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)) : ℝ)
⊢ (Valued.v : (a : PadicAlgCl p) → ℝ≥0) ((algebraMap ℚ_[p] (PadicAlgCl p) : (a : ℚ_[p]) → PadicAlgCl p) (↑p : ℚ_[p])) =
    HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)

Tactic:
ext
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a :
  Norm.norm (E := PadicAlgCl p) ((algebraMap ℚ_[p] (PadicAlgCl p) : (a : ℚ_[p]) → PadicAlgCl p) (↑p : ℚ_[p])) =
    (↑(HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)) : ℝ)
a₁ : Norm.norm (E := ℚ_[p]) (↑p : ℚ_[p]) = (↑(HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)) : ℝ)
a₂ : (↑p : ℝ)⁻¹ = (↑(HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)) : ℝ)
a₃ : (↑p : ℝ)⁻¹ = (↑(↑p : ℝ≥0)⁻¹ : ℝ)
a₄ : (↑p : ℝ)⁻¹ = (↑(↑p : ℝ≥0) : ℝ)⁻¹
a₅ a₆ : Eq (α := ℝ) (↑p : ℝ)⁻¹ (↑p : ℝ)⁻¹
⊢ (↑((Valued.v : (a : PadicAlgCl p) → ℝ≥0)
          ((algebraMap ℚ_[p] (PadicAlgCl p) : (a : ℚ_[p]) → PadicAlgCl p) (↑p : ℚ_[p]))) :
      ℝ) =
    (↑(HDiv.hDiv (α := ℝ≥0) 1 (↑p : ℝ≥0)) : ℝ)

Tactic:
rw [valuation_coe, norm_extends, Padic.norm_p, one_div, NNReal.coe_inv,
    NNReal.coe_natCast]

Premises used: PadicAlgCl.norm_extends, NNReal.coe_natCast, NNReal.coe_inv, PadicAlgCl.valuation_coe, one_div, Padic.norm_p
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h :
  Ne (α := ℝ≥0) ((Valued.v : (a : PadicAlgCl p) → ℝ≥0) (↑p : PadicAlgCl p)) 0 ∧
    Ne (α := ℝ≥0) ((Valued.v : (a : PadicAlgCl p) → ℝ≥0) (↑p : PadicAlgCl p)) 1
⊢ ∃ (x : PadicAlgCl p),
    Ne (α := ℝ≥0) ((Valued.v : (a : PadicAlgCl p) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0) ∧
      Ne (α := ℝ≥0) ((Valued.v : (a : PadicAlgCl p) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)

Tactic:
use p
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Nat.Prime p

Tactic:
have hp : Nat.Prime p := hp.1
-- Module: Mathlib.NumberTheory.Padics.Complex
Goal:
p : ℕ
hp_1 : Fact (Nat.Prime p)
hp : Nat.Prime p
h : ¬p = 0 ∧ ¬p = 1
⊢ Ne (α := ℝ≥0) ((Valued.v : (a : PadicAlgCl p) → ℝ≥0) (↑p : PadicAlgCl p)) 0 ∧
    Ne (α := ℝ≥0) ((Valued.v : (a : PadicAlgCl p) → ℝ≥0) (↑p : PadicAlgCl p)) 1

Tactic:
simp only [valuation_p, one_div, ne_eq, inv_eq_zero, Nat.cast_eq_zero, inv_eq_one,
      Nat.cast_eq_one]

Premises used: inv_eq_zero, inv_eq_one, PadicAlgCl.valuation_p, ne_eq, Nat.cast_eq_zero, Nat.cast_eq_one, one_div