awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])‖ <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
H : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
H' :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p])‖ < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
hN₁ : norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p]) < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
H₁ : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
⊢ ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p])‖ < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])

Tactic:
rw [Padic.add_eq_max_of_ne H'.ne, sup_eq_right.mpr H'.le] at hN

Premises used: Iff.mpr, LT.lt.le, sup_eq_right, Padic.add_eq_max_of_ne, LT.lt.ne
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN : norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p]) < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
H : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
H' :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p])‖ < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
⊢ False

Tactic:
lt_asymm hN H

Premises used: lt_asymm
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN : norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p]) < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
H : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
H' :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p])‖ < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
⊢ False

Tactic:
exact lt_asymm hN H

Premises used: lt_asymm
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])‖ <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
⊢ norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p]) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
have : ‖(((x.appr n) - f (N + n) : ℤ) : ℚ_[p])‖ ≤ ↑p ^ (-n : ℤ) := by
    by_contra! H
    have H' : ‖(p ^ n * e : ℚ_[p])‖ < ‖(((x.appr n) - f (N + n) : ℤ) : ℚ_[p])‖ := by
      refine LE.le.trans_lt ?_ H
      simpa using mul_le_mul_of_nonneg le_rfl e.2 (show 0 ≤ (↑p ^ n)⁻¹ by simp) zero_le_one
    rw [Padic.add_eq_max_of_ne H'.ne, sup_eq_right.mpr H'.le] at hN
    exact lt_asymm hN H
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])‖ <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
this : norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p]) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
⊢ Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(x.appr n) : ZMod (p ^ n))

Tactic:
rw [Padic.norm_int_le_pow_iff_dvd, ← Nat.cast_pow,
    ← ZMod.intCast_eq_intCast_iff_dvd_sub, Int.cast_natCast] at this

Premises used: ZMod.intCast_eq_intCast_iff_dvd_sub, Int.cast_natCast, Nat.cast_pow, Padic.norm_int_le_pow_iff_dvd
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])‖ <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
this : Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(x.appr n) : ZMod (p ^ n))
⊢ Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))

Tactic:
this.symm.trans ?_

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])‖ <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
this : Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(x.appr n) : ZMod (p ^ n))
refine : Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))
⊢ Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))

Tactic:
refine this.symm.trans ?_

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
⊢ Eq (α := ZMod (p ^ n)) (↑(f (0 + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n N : ℕ
IH : Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))
succ : (↑(p ^ n) : ℤ) ∣ f (N + n + 1) - f (N + n)
⊢ Eq (α := ZMod (p ^ n)) (↑(f (N + 1 + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))

Tactic:
rw [← IH, eq_comm, add_right_comm, ZMod.intCast_eq_intCast_iff_dvd_sub]

Premises used: ZMod.intCast_eq_intCast_iff_dvd_sub, add_right_comm, eq_comm
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n N : ℕ
IH : Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) (N + n) = (↑(p ^ n) : ℤ) * HPow.hPow (α := ℤ) (↑p : ℤ) N

Tactic:
simp [pow_add, mul_comm]

Premises used: pow_add, mul_comm
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n N : ℕ
IH : Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))
⊢ (↑(p ^ n) : ℤ) ∣ f (N + n + 1) - f (N + n)

Tactic:
exact .trans ⟨p ^ N, by simp [pow_add, mul_comm]⟩ (hi _)
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n N : ℕ
zero : Eq (α := ZMod (p ^ n)) (↑(f (0 + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))
succ :
  ∀ (N : ℕ) (IH : Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))),
    Eq (α := ZMod (p ^ n)) (↑(f (N + 1 + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))
⊢ Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))

Tactic:
induction N with
  | zero => simp
  | succ N IH =>
    rw [← IH, eq_comm, add_right_comm, ZMod.intCast_eq_intCast_iff_dvd_sub]
    exact .trans ⟨p ^ N, by simp [pow_add, mul_comm]⟩ (hi _)

Premises used: ZMod.intCast_eq_intCast_iff_dvd_sub, add_right_comm, eq_comm, Nat.zero, Nat.succ
-- Module: Mathlib.NumberTheory.Padics.ValuativeRel
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
Γ₀ : Type u_1
inst : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation ℚ_[p] Γ₀
⊢ Valuation.Compatible (R := ℚ_[p]) mulValuation

Tactic:
.ofValuation _

Premises used: Valuation.Compatible.ofValuation
-- Module: Mathlib.NumberTheory.Padics.ValuativeRel
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
Γ₀ : Type u_1
inst : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation ℚ_[p] Γ₀
inst_1 : v.Compatible
⊢ Ne (α := Γ₀) ((v : (a : ℚ_[p]) → Γ₀) (↑p : ℚ_[p]) : Γ₀) (0 : Γ₀)

Tactic:
simp [(isEquiv v (Padic.mulValuation)).eq_zero, hp.out.ne_zero]

Premises used: Valuation.IsEquiv.eq_zero, ValuativeRel.isEquiv, Nat.Prime.ne_zero, Padic.mulValuation, Fact.out
-- Module: Mathlib.NumberTheory.Padics.ValuativeRel
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
Γ₀ : Type u_1
inst : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation ℚ_[p] Γ₀
inst_1 : v.Compatible
⊢ LT.lt (α := Γ₀) ((v : (a : ℚ_[p]) → Γ₀) (↑p : ℚ_[p]) : Γ₀) (1 : Γ₀)

Tactic:
simp [(isEquiv v (Padic.mulValuation)).lt_one_iff_lt_one, hp.out.ne_zero, inv_lt_one₀,
    ← log_lt_iff_lt_exp]

Premises used: inv_lt_one₀, ValuativeRel.isEquiv, Nat.Prime.ne_zero, Valuation.IsEquiv.lt_one_iff_lt_one, WithZero.log_lt_iff_lt_exp, Padic.mulValuation, Fact.out
-- Module: Mathlib.NumberTheory.Padics.ValuativeRel
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
Γ₀ : Type u_1
inst : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation ℚ_[p] Γ₀
inst_1 : v.Compatible
⊢ IsRankLeOne ℚ_[p]

Tactic:
.of_compatible_mulArchimedean mulValuation

Premises used: ValuativeRel.IsRankLeOne.of_compatible_mulArchimedean, Padic.mulValuation
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ LT.lt (α := ℚ) 0 (↑p : ℚ)

Tactic:
simp [Nat.Prime.pos Fact.out]

Premises used: Nat.Prime.pos, Fact.out
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ LT.lt (α := ℚ) 0 (↑p : ℚ)

Tactic:
have hp0' : 0 < (p : ℚ) := by simp [Nat.Prime.pos Fact.out]
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
⊢ LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹

Tactic:
simp [Nat.Prime.pos Fact.out]

Premises used: Nat.Prime.pos, Fact.out
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
⊢ LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹

Tactic:
have hp0 : 0 < (p : ℝ)⁻¹ := by simp [Nat.Prime.pos Fact.out]
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
⊢ LT.lt (α := ℚ) 1 (↑p : ℚ)

Tactic:
simp [Nat.Prime.one_lt Fact.out]

Premises used: Nat.Prime.one_lt, Fact.out
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
⊢ LT.lt (α := ℚ) 1 (↑p : ℚ)

Tactic:
have hp1' : 1 < (p : ℚ) := by simp [Nat.Prime.one_lt Fact.out]
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
⊢ LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1

Tactic:
simp [inv_lt_one_iff₀, Nat.Prime.one_lt Fact.out]

Premises used: Nat.Prime.one_lt, inv_lt_one_iff₀, Fact.out
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
⊢ LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1

Tactic:
have hp1 : (p : ℝ)⁻¹ < 1 := by simp [inv_lt_one_iff₀, Nat.Prime.one_lt Fact.out]
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
n : ℕ
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))

Tactic:
simp only [← WithVal.val_apply_equiv, map_pow, map_natCast, Rat.padicValuation_self,
        Int.reduceNeg, exp_neg, inv_pow, ← exp_nsmul, nsmul_eq_mul, mul_one]

Premises used: Rat.padicValuation_self, Int.reduceNeg, WithVal.val_apply_equiv, map_pow, inv_pow, WithZero.exp_nsmul, map_natCast, nsmul_eq_mul, mul_one, WithZero.exp_neg
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
n : ℕ
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))

Tactic:
have hn : Valued.v (R := (WithVal (Rat.padicValuation p))) (p ^ n) =
      exp (-n : ℤ) := by
      simp only [← WithVal.val_apply_equiv, map_pow, map_natCast, Rat.padicValuation_self,
        Int.reduceNeg, exp_neg, inv_pow, ← exp_nsmul, nsmul_eq_mul, mul_one]
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
n : ℕ
hn :
  Eq (α := WithZero (Multiplicative ℤ))
    ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
rw : ¬Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ))) 0
⊢ Ne (α :=
    MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
      Valued.v)
    ((Valuation.restrict Valued.v :
          (a : WithVal (Rat.padicValuation p)) →
            MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
        (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n) :
      MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
    (0 :
      MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
        Valued.v)

Tactic:
rw [ne_eq, Valuation.restrict_def, restrict₀_eq_zero_iff, hn]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff, ne_eq, Valuation.restrict_def
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
n : ℕ
hn :
  Eq (α := WithZero (Multiplicative ℤ))
    ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
⊢ ¬Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ))) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
n : ℕ
hn :
  Eq (α := WithZero (Multiplicative ℤ))
    ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
h :
  ∀ (x y : WithVal (Rat.padicValuation p)),
    LT.lt (α :=
        MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
        ((Valuation.restrict Valued.v :
              (a : WithVal (Rat.padicValuation p)) →
                MonoidWithZeroHom.ValueGroup₀
                  (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
            (y - x) :
          MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
            (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
        ((↑(Units.mk0
                ((Valuation.restrict Valued.v :
                    (a : WithVal (Rat.padicValuation p)) →
                      MonoidWithZeroHom.ValueGroup₀
                        (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
                  (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n))
                ⋯) :
            MonoidWithZeroHom.ValueGroup₀ (F :=
              Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ))) Valued.v) :
          MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
            Valued.v) →
      (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
        (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹
⊢ ∃ (j :
    (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
        Valued.v)ˣ),
    ∀ (x y : WithVal (Rat.padicValuation p)),
      (Valuation.restrict Valued.v :
              (a : WithVal (Rat.padicValuation p)) →
                MonoidWithZeroHom.ValueGroup₀
                  (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
            (y - x) <
          (↑j : MonoidWithZeroHom.ValueGroup₀ Valued.v) →
        (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) :
            ℝ) ≤
          (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹

Tactic:
use Units.mk0 (Valued.v.restrict (p ^ n)) (by
      rw [ne_eq, Valuation.restrict_def, restrict₀_eq_zero_iff, hn]; simp)
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
n : ℕ
hn :
  Eq (α := WithZero (Multiplicative ℤ))
    ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
x y : WithVal (Rat.padicValuation p)
h :
  LT.lt (α :=
    MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
      (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
    ((Valuation.restrict Valued.v :
          (a : WithVal (Rat.padicValuation p)) →
            MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
        (y - x) :
      MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
    ((↑(Units.mk0
            ((Valuation.restrict Valued.v :
                (a : WithVal (Rat.padicValuation p)) →
                  MonoidWithZeroHom.ValueGroup₀
                    (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
              (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n))
            ⋯) :
        MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
          Valued.v) :
      MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
        Valued.v)
⊢ let x' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x;
  x' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x

Tactic:
set x' := (WithVal.equiv (Rat.padicValuation p)) x with hx

Premises used: WithVal.equiv, Rat.padicValuation, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
n : ℕ
hn :
  Eq (α := WithZero (Multiplicative ℤ))
    ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
x y : WithVal (Rat.padicValuation p)
h :
  LT.lt (α :=
    MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
      (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
    ((Valuation.restrict Valued.v :
          (a : WithVal (Rat.padicValuation p)) →
            MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
        (y - x) :
      MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
    ((↑(Units.mk0
            ((Valuation.restrict Valued.v :
                (a : WithVal (Rat.padicValuation p)) →
                  MonoidWithZeroHom.ValueGroup₀
                    (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
              (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n))
            ⋯) :
        MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
          Valued.v) :
      MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
        Valued.v)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
hx : x' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
⊢ let y' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y;
  y' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y

Tactic:
set y' := (WithVal.equiv (Rat.padicValuation p)) y with hy

Premises used: WithVal.equiv, Rat.padicValuation, DFunLike.coe