awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ} (hle : padicValRat p q ≤ padicValRat p r), padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (r + q) ≤ max (padicNorm p r) (padicNorm p q)

Tactic:
exact this (le_of_not_ge hle)

Premises used: le_of_not_ge
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hle : padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
nonarchimedean_aux hle

Premises used: _private.0.padicNorm.nonarchimedean_aux
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hle : padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
exact nonarchimedean_aux hle

Premises used: _private.0.padicNorm.nonarchimedean_aux
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q + r) ≤ padicNorm p q + padicNorm p r

Tactic:
calc
    padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r) := padicNorm.nonarchimedean
    _ ≤ padicNorm p q + padicNorm p r :=
      max_le_add_of_nonneg (padicNorm.nonneg _) (padicNorm.nonneg _)

Premises used: Trans.trans, padicNorm.nonarchimedean, padicNorm.nonneg, max_le_add_of_nonneg
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
rw : padicNorm p (q + -r) ≤ max (padicNorm p q) (padicNorm p (-r))
⊢ padicNorm p (q - r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
rw [sub_eq_add_neg, ← padicNorm.neg r]

Premises used: sub_eq_add_neg, padicNorm.neg
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q + -r) ≤ max (padicNorm p q) (padicNorm p (-r))

Tactic:
padicNorm.nonarchimedean

Premises used: padicNorm.nonarchimedean
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q + -r) ≤ max (padicNorm p q) (padicNorm p (-r))

Tactic:
exact padicNorm.nonarchimedean

Premises used: padicNorm.nonarchimedean
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ
hx : x = 0
⊢ padicNorm p x = 0

Tactic:
simp [hx]
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
⊢ padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)

Tactic:
IsNonarchimedean.add_eq_max_of_ne (f := IsAbsoluteValue.toAbsoluteValue (padicNorm p))
    (fun _ _ ↦ padicNorm.nonarchimedean) hne

Premises used: padicNorm.nonarchimedean, IsNonarchimedean.add_eq_max_of_ne, padicNorm, ite
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
pos : ∀ (hz : Eq (α := ℚ) (↑z : ℚ) 0), (↑(p ^ n) : ℤ) ∣ z ↔ 0 ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
neg :
  ∀ (hz : ¬Eq (α := ℚ) (↑z : ℚ) 0),
    (↑(p ^ n) : ℤ) ∣ z ↔
      HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑z : ℚ)) ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
⊢ (↑(p ^ n) : ℤ) ∣ z ↔
    (if Eq (α := ℚ) (↑z : ℚ) 0 then 0 else HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑z : ℚ))) ≤
      HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))

Tactic:
split_ifs with hz
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : Eq (α := ℚ) (↑z : ℚ) 0
⊢ z = 0

Tactic:
norm_cast at hz
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : z = 0
⊢ (↑(p ^ n) : ℤ) ∣ z ↔ 0 ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))

Tactic:
simp [hz]
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬Eq (α := ℚ) (↑z : ℚ) 0
neg : (↑(p ^ n) : ℤ) ∣ z ↔ LE.le (α := ℤ) (↑n : ℤ) (↑(multiplicity (↑p : ℤ) z) : ℤ)
rw : z ≠ 0
neg₁ : LT.lt (α := ℚ) 1 (↑p : ℚ)
⊢ (↑(p ^ n) : ℤ) ∣ z ↔
    HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑z : ℚ)) ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))

Tactic:
rw [zpow_le_zpow_iff_right₀, neg_le_neg_iff, padicValRat.of_int,
      padicValInt.of_ne_one_ne_zero hp.1.ne_one _]

Premises used: zpow_le_zpow_iff_right₀, padicValRat.of_int, Nat.Prime.ne_one, padicValInt.of_ne_one_ne_zero, Fact.out, neg_le_neg_iff
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬Eq (α := ℚ) (↑z : ℚ) 0
neg : (↑(p ^ n) : ℤ) ∣ z ↔ n ≤ multiplicity (↑p : ℤ) z
⊢ (↑(p ^ n) : ℤ) ∣ z ↔ LE.le (α := ℤ) (↑n : ℤ) (↑(multiplicity (↑p : ℤ) z) : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬Eq (α := ℚ) (↑z : ℚ) 0
neg : (↑(p ^ n) : ℤ) ∣ z ↔ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ z
neg₁ : FiniteMultiplicity (↑p : ℤ) z
⊢ (↑(p ^ n) : ℤ) ∣ z ↔ n ≤ multiplicity (↑p : ℤ) z

Tactic:
rw [← FiniteMultiplicity.pow_dvd_iff_le_multiplicity]

Premises used: FiniteMultiplicity.pow_dvd_iff_le_multiplicity
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬Eq (α := ℚ) (↑z : ℚ) 0
neg neg₁ neg₂ neg₃ : (↑(p ^ n) : ℤ) ∣ z ↔ (↑(p ^ n) : ℤ) ∣ z
⊢ (↑(p ^ n) : ℤ) ∣ z ↔ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ z

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬Eq (α := ℚ) (↑z : ℚ) 0
⊢ Int.natAbs (↑p : ℤ) ≠ 1

Tactic:
simp [hp.out.ne_one]

Premises used: Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬Eq (α := ℚ) (↑z : ℚ) 0
⊢ FiniteMultiplicity (↑p : ℤ) z

Tactic:
apply Int.finiteMultiplicity_iff.2 ⟨by simp [hp.out.ne_one], mod_cast hz⟩

Premises used: Iff.mpr, Int.finiteMultiplicity_iff, And.intro
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬Eq (α := ℚ) (↑z : ℚ) 0
⊢ z ≠ 0

Tactic:
exact_mod_cast hz
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬Eq (α := ℚ) (↑z : ℚ) 0
⊢ LT.lt (α := ℚ) 1 (↑p : ℚ)

Tactic:
exact_mod_cast hp.out.one_lt

Premises used: Nat.Prime.one_lt, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
nth_rw : padicNorm p (↑m : ℚ) = 1 ↔ ¬(↑(HPow.hPow (β := ℕ) p 1) : ℤ) ∣ m
⊢ padicNorm p (↑m : ℚ) = 1 ↔ ¬(↑p : ℤ) ∣ m

Tactic:
nth_rw 2 [← pow_one p]

Premises used: pow_one
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
simp : padicNorm p (↑m : ℚ) = 1 ↔ (↑p : ℚ)⁻¹ < padicNorm p (↑m : ℚ)
⊢ padicNorm p (↑m : ℚ) = 1 ↔ ¬(↑(HPow.hPow (β := ℕ) p 1) : ℤ) ∣ m

Tactic:
simp only [dvd_iff_norm_le, Nat.cast_one, zpow_neg, zpow_one, not_le]

Premises used: not_le, zpow_one, padicNorm.dvd_iff_norm_le, zpow_neg, Nat.cast_one
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
mp : padicNorm p (↑m : ℚ) = 1 → (↑p : ℚ)⁻¹ < padicNorm p (↑m : ℚ)
mpr : (↑p : ℚ)⁻¹ < padicNorm p (↑m : ℚ) → padicNorm p (↑m : ℚ) = 1
⊢ padicNorm p (↑m : ℚ) = 1 ↔ (↑p : ℚ)⁻¹ < padicNorm p (↑m : ℚ)

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p (↑m : ℚ) = 1
mp : LT.lt (α := ℚ) 1 (↑p : ℚ)
mp₁ : LT.lt (α := ℚ) 0 (↑p : ℚ)
⊢ (↑p : ℚ)⁻¹ < padicNorm p (↑m : ℚ)

Tactic:
rw [h, inv_lt_one₀]

Premises used: inv_lt_one₀
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p (↑m : ℚ) = 1
mp : 1 < p
⊢ LT.lt (α := ℚ) 1 (↑p : ℚ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p (↑m : ℚ) = 1
mp : 0 < p
⊢ LT.lt (α := ℚ) 0 (↑p : ℚ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p (↑m : ℚ) = 1
⊢ 1 < p

Tactic:
Nat.Prime.one_lt Fact.out

Premises used: Nat.Prime.one_lt, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p (↑m : ℚ) = 1
⊢ 1 < p

Tactic:
exact Nat.Prime.one_lt Fact.out

Premises used: Nat.Prime.one_lt, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p (↑m : ℚ) = 1
⊢ 0 < p

Tactic:
Nat.Prime.pos Fact.out

Premises used: Nat.Prime.pos, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p (↑m : ℚ) = 1
⊢ 0 < p

Tactic:
exact Nat.Prime.pos Fact.out

Premises used: Nat.Prime.pos, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
pos : Eq (α := ℚ) (↑m : ℚ) 0 → LT.lt (α := ℚ) (↑p : ℚ)⁻¹ 0 → Eq (α := ℚ) 0 1
neg :
  ¬Eq (α := ℚ) (↑m : ℚ) 0 →
    (↑p : ℚ)⁻¹ < HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) →
      HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) = 1
⊢ ((↑p : ℚ)⁻¹ < if Eq (α := ℚ) (↑m : ℚ) 0 then 0 else HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ))) →
    (if Eq (α := ℚ) (↑m : ℚ) 0 then 0 else HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ))) = 1

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : Eq (α := ℚ) (↑m : ℚ) 0
pos : p < 0 → Eq (α := ℚ) (↑0 : ℚ) 1
⊢ LT.lt (α := ℚ) (↑p : ℚ)⁻¹ 0 → Eq (α := ℚ) 0 1

Tactic:
rw [inv_lt_zero, ← Nat.cast_zero, Nat.cast_lt]

Premises used: inv_lt_zero, Nat.cast_zero, Nat.cast_lt
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h_1 : Eq (α := ℚ) (↑m : ℚ) 0
h : p < 0
⊢ Eq (α := ℚ) (↑0 : ℚ) 1

Tactic:
(Nat.not_lt_zero p h).elim

Premises used: False.elim, Nat.not_lt_zero
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h_1 : Eq (α := ℚ) (↑m : ℚ) 0
h : p < 0
⊢ Eq (α := ℚ) (↑0 : ℚ) 1

Tactic:
exact (Nat.not_lt_zero p h).elim

Premises used: False.elim, Nat.not_lt_zero
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : ¬Eq (α := ℚ) (↑m : ℚ) 0
norm_cast : 1 < p
⊢ LT.lt (α := ℚ) 1 (↑p : ℚ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : ¬Eq (α := ℚ) (↑m : ℚ) 0
⊢ 1 < p

Tactic:
Nat.Prime.one_lt (Fact.out : Nat.Prime p)

Premises used: Nat.Prime.one_lt, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : ¬Eq (α := ℚ) (↑m : ℚ) 0
⊢ 1 < p

Tactic:
exact Nat.Prime.one_lt (Fact.out : Nat.Prime p)

Premises used: Nat.Prime.one_lt, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : ¬Eq (α := ℚ) (↑m : ℚ) 0
⊢ LT.lt (α := ℚ) 1 (↑p : ℚ)

Tactic:
have : 1 < (p : ℚ) := by norm_cast; exact Nat.Prime.one_lt (Fact.out : Nat.Prime p)
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : ¬Eq (α := ℚ) (↑m : ℚ) 0
this : LT.lt (α := ℚ) 1 (↑p : ℚ)
neg : -1 < -padicValRat p (↑m : ℚ) → HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) = 1
⊢ (↑p : ℚ)⁻¹ < HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) →
    HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) = 1

Tactic:
rw [← zpow_neg_one, zpow_lt_zpow_iff_right₀ this]

Premises used: zpow_neg_one, zpow_lt_zpow_iff_right₀
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : ¬Eq (α := ℚ) (↑m : ℚ) 0
this : LT.lt (α := ℚ) 1 (↑p : ℚ)
⊢ 0 ≤ padicValRat p (↑m : ℚ)

Tactic:
simp only [of_int, Nat.cast_nonneg]

Premises used: Nat.cast_nonneg, padicValRat.of_int
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : ¬Eq (α := ℚ) (↑m : ℚ) 0
this : LT.lt (α := ℚ) 1 (↑p : ℚ)
⊢ 0 ≤ padicValRat p (↑m : ℚ)

Tactic:
have : 0 ≤ padicValRat p m := by simp only [of_int, Nat.cast_nonneg]
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h_1 : ¬Eq (α := ℚ) (↑m : ℚ) 0
this_1 : LT.lt (α := ℚ) 1 (↑p : ℚ)
this : 0 ≤ padicValRat p (↑m : ℚ)
h : -1 < -padicValRat p (↑m : ℚ)
neg : -padicValRat p (↑m : ℚ) = 0
neg₁ : LT.lt (α := ℚ) 0 (↑p : ℚ)
neg₂ : Ne (α := ℚ) (↑p : ℚ) 1
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) = 1

Tactic:
rw [← zpow_zero (p : ℚ), zpow_right_inj₀]

Premises used: zpow_right_inj₀, zpow_zero, Nat.cast
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h_1 : ¬Eq (α := ℚ) (↑m : ℚ) 0
this_1 : LT.lt (α := ℚ) 1 (↑p : ℚ)
this : 0 ≤ padicValRat p (↑m : ℚ)
h : -1 < -padicValRat p (↑m : ℚ)
linarith :
  -padicValRat p (↑m : ℚ) < 0 →
    -1 + (HAdd.hAdd (α := ℤ) (-1) 1 - -padicValRat p (↑m : ℚ)) + (-padicValRat p (↑m : ℚ) + 1 - 0) = 0
linarith₁ :
  0 < -padicValRat p (↑m : ℚ) →
    -1 + (0 - padicValRat p (↑m : ℚ)) + (HAdd.hAdd (α := ℤ) 0 1 - -padicValRat p (↑m : ℚ)) = 0
⊢ -padicValRat p (↑m : ℚ) = 0

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h_1 : ¬Eq (α := ℚ) (↑m : ℚ) 0
this_1 : LT.lt (α := ℚ) 1 (↑p : ℚ)
this : 0 ≤ padicValRat p (↑m : ℚ)
h : -1 < -padicValRat p (↑m : ℚ)
linarith : LE.le (α := ℚ) (↑p : ℚ) 0 → -1 + HSub.hSub (α := ℚ) 1 (↑p : ℚ) + HSub.hSub (α := ℚ) (↑p : ℚ) 0 = 0
⊢ LT.lt (α := ℚ) 0 (↑p : ℚ)

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h_1 : ¬Eq (α := ℚ) (↑m : ℚ) 0
this_1 : LT.lt (α := ℚ) 1 (↑p : ℚ)
this : 0 ≤ padicValRat p (↑m : ℚ)
h : -1 < -padicValRat p (↑m : ℚ)
linarith : Eq (α := ℚ) (↑p : ℚ) 1 → HSub.hSub (α := ℚ) 1 (↑p : ℚ) + HSub.hSub (α := ℚ) (↑p : ℚ) 1 = 0
⊢ Ne (α := ℚ) (↑p : ℚ) 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
rw : ¬padicNorm p (↑m : ℚ) < 1 ↔ padicNorm p (↑m : ℚ) ≤ 1 ∧ ¬padicNorm p (↑m : ℚ) < 1
⊢ padicNorm p (↑m : ℚ) < 1 ↔ (↑p : ℤ) ∣ m

Tactic:
rw [← not_iff_not, ← int_eq_one_iff, eq_iff_le_not_lt]

Premises used: not_iff_not, padicNorm.int_eq_one_iff, eq_iff_le_not_lt
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ ¬padicNorm p (↑m : ℚ) < 1 ↔ padicNorm p (↑m : ℚ) ≤ 1 ∧ ¬padicNorm p (↑m : ℚ) < 1

Tactic:
simp only [padicNorm.of_int, true_and]

Premises used: padicNorm.of_int, true_and
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p (↑m : ℚ) ≤ 1

Tactic:
padicNorm.of_int (m : ℤ)

Premises used: Nat.cast, padicNorm.of_int
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
rw : padicNorm p (↑m : ℚ) = 1 ↔ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑m : ℤ)
rw₁ : padicNorm p (↑m : ℚ) = 1 ↔ padicNorm p (↑(↑m : ℤ) : ℚ) = 1
rw₂ rw₃ : padicNorm p (↑m : ℚ) = 1 ↔ padicNorm p (↑m : ℚ) = 1
⊢ padicNorm p (↑m : ℚ) = 1 ↔ ¬p ∣ m

Tactic:
rw [← Int.natCast_dvd_natCast, ← int_eq_one_iff, Int.cast_natCast]

Premises used: Int.cast_natCast, padicNorm.int_eq_one_iff, Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
rw : padicNorm p (↑m : ℚ) < 1 ↔ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑m : ℤ)
rw₁ : padicNorm p (↑m : ℚ) < 1 ↔ padicNorm p (↑(↑m : ℤ) : ℚ) < 1
rw₂ rw₃ : padicNorm p (↑m : ℚ) < 1 ↔ padicNorm p (↑m : ℚ) < 1
⊢ padicNorm p (↑m : ℚ) < 1 ↔ p ∣ m

Tactic:
rw [← Int.natCast_dvd_natCast, ← int_lt_one_iff, Int.cast_natCast]

Premises used: Int.cast_natCast, padicNorm.int_lt_one_iff, Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
a : ℚ
hp : Fact (Nat.Prime p)
H : 1 < padicNorm p a
contrapose! : ∀ (H : a.isInt = true), padicNorm p a ≤ 1
⊢ ¬a.isInt = true

Tactic:
contrapose! H
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
a : ℚ
hp : Fact (Nat.Prime p)
H : a.isInt = true
rw : padicNorm p (↑a.num : ℚ) ≤ 1
⊢ padicNorm p a ≤ 1

Tactic:
rw [Rat.eq_num_of_isInt H]

Premises used: Rat.eq_num_of_isInt
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
a : ℚ
hp : Fact (Nat.Prime p)
H : a.isInt = true
⊢ padicNorm p (↑a.num : ℚ) ≤ 1

Tactic:
apply padicNorm.of_int

Premises used: padicNorm.of_int
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hs : s.Nonempty
hF : ∀ i ∈ s, padicNorm p (F i) < t
⊢ padicNorm p (∑ i ∈ s, F i) < t

Tactic:
lt_of_le_of_lt (IsNonarchimedean.apply_sum_le_sup (fun _ _ ↦ padicNorm.nonarchimedean) hs) <|
    (Finset.sup'_lt_iff hs).2 hF

Premises used: Iff.mpr, lt_of_le_of_lt, padicNorm.nonarchimedean, Finset.sup'_lt_iff, IsNonarchimedean.apply_sum_le_sup
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hs : s.Nonempty
hF : ∀ i ∈ s, padicNorm p (F i) ≤ t
⊢ padicNorm p (∑ i ∈ s, F i) ≤ t

Tactic:
(IsNonarchimedean.apply_sum_le_sup (fun _ _ ↦ padicNorm.nonarchimedean) hs).trans <|
    (Finset.sup'_le_iff hs (fun i ↦ padicNorm p (F i))).2 hF

Premises used: Iff.mpr, padicNorm.nonarchimedean, IsNonarchimedean.apply_sum_le_sup, Finset.sup'_le_iff, LE.le.trans, padicNorm
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) < t
ht : 0 < t
inl : ∀ (hF : ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → padicNorm p (F i) < t), padicNorm p (∑ i ∈ ∅, F i) < t
inr : ∀ (hs : s.Nonempty), padicNorm p (∑ i ∈ s, F i) < t
⊢ padicNorm p (∑ i ∈ s, F i) < t

Tactic:
obtain rfl | hs := Finset.eq_empty_or_nonempty s

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 < t
hF : ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → padicNorm p (F i) < t
⊢ padicNorm p (∑ i ∈ ∅, F i) < t

Tactic:
simp [ht]
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) < t
ht : 0 < t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) < t

Tactic:
sum_lt hs hF

Premises used: padicNorm.sum_lt
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) < t
ht : 0 < t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) < t

Tactic:
exact sum_lt hs hF

Premises used: padicNorm.sum_lt
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) ≤ t
ht : 0 ≤ t
inl : ∀ (hF : ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → padicNorm p (F i) ≤ t), padicNorm p (∑ i ∈ ∅, F i) ≤ t
inr : ∀ (hs : s.Nonempty), padicNorm p (∑ i ∈ s, F i) ≤ t
⊢ padicNorm p (∑ i ∈ s, F i) ≤ t

Tactic:
obtain rfl | hs := Finset.eq_empty_or_nonempty s

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 ≤ t
hF : ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → padicNorm p (F i) ≤ t
⊢ padicNorm p (∑ i ∈ ∅, F i) ≤ t

Tactic:
simp [ht]
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) ≤ t
ht : 0 ≤ t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) ≤ t

Tactic:
sum_le hs hF

Premises used: padicNorm.sum_le
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) ≤ t
ht : 0 ≤ t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) ≤ t

Tactic:
exact sum_le hs hF

Premises used: padicNorm.sum_le
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ (if Eq (α := ℚ) 0 0 then 0 else exp (-padicValRat p 0)) = 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ (if Eq (α := ℚ) 1 0 then 0 else exp (-padicValRat p 1)) = 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
pos : x * y = 0 → x = 0 → y = 0 → 0 = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
neg : x * y = 0 → x = 0 → ¬y = 0 → 0 = 0 * exp (-padicValRat p y)
pos₁ : x * y = 0 → ¬x = 0 → y = 0 → 0 = exp (-padicValRat p x) * 0
neg₁ : x * y = 0 → ¬x = 0 → ¬y = 0 → 0 = exp (-padicValRat p x) * exp (-padicValRat p y)
pos₂ : ¬x * y = 0 → x = 0 → y = 0 → exp (-padicValRat p (x * y)) = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
neg₂ : ¬x * y = 0 → x = 0 → ¬y = 0 → exp (-padicValRat p (x * y)) = 0 * exp (-padicValRat p y)
pos₃ : ¬x * y = 0 → ¬x = 0 → y = 0 → exp (-padicValRat p (x * y)) = exp (-padicValRat p x) * 0
neg₃ : ¬x * y = 0 → ¬x = 0 → ¬y = 0 → exp (-padicValRat p (x * y)) = exp (-padicValRat p x) * exp (-padicValRat p y)
⊢ (if x * y = 0 then 0 else exp (-padicValRat p (x * y))) =
    (if x = 0 then 0 else exp (-padicValRat p x)) * if y = 0 then 0 else exp (-padicValRat p y)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : x * y = 0
h_1 : x = 0
h_2 : y = 0
⊢ 0 = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

Premises used: WithZero.exp_add, mul_comm, padicValRat.mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : x * y = 0
h_1 : x = 0
h_2 : ¬y = 0
⊢ 0 = 0 * exp (-padicValRat p y)

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

Premises used: WithZero.exp_add, mul_comm, padicValRat.mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : x * y = 0
h_1 : ¬x = 0
h_2 : y = 0
⊢ 0 = exp (-padicValRat p x) * 0

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

Premises used: WithZero.exp_add, mul_comm, padicValRat.mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : x * y = 0
h_1 : ¬x = 0
h_2 : ¬y = 0
⊢ 0 = exp (-padicValRat p x) * exp (-padicValRat p y)

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

Premises used: WithZero.exp_add, mul_comm, padicValRat.mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : ¬x * y = 0
h_1 : x = 0
h_2 : y = 0
⊢ exp (-padicValRat p (x * y)) = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

Premises used: WithZero.exp_add, mul_comm, padicValRat.mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : ¬x * y = 0
h_1 : x = 0
h_2 : ¬y = 0
⊢ exp (-padicValRat p (x * y)) = 0 * exp (-padicValRat p y)

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

Premises used: WithZero.exp_add, mul_comm, padicValRat.mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : ¬x * y = 0
h_1 : ¬x = 0
h_2 : y = 0
⊢ exp (-padicValRat p (x * y)) = exp (-padicValRat p x) * 0

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

Premises used: WithZero.exp_add, mul_comm, padicValRat.mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : ¬x * y = 0
h_1 : ¬x = 0
h_2 : ¬y = 0
⊢ exp (-padicValRat p (x * y)) = exp (-padicValRat p x) * exp (-padicValRat p y)

Tactic:
simp_all [padicValRat.mul, exp_add, mul_comm]

Premises used: WithZero.exp_add, mul_comm, padicValRat.mul