awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q) = 0
hq : ¬q = 0
⊢ ¬HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q) = 0
have a : Ne (α := ℚ) (↑p : ℚ) 0
Tactic: apply zpow_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r
have this : Ne (α := ℚ) (↑p : ℚ) 0
Tactic: have : (p : ℚ) ≠ 0 := by simp [hp.1.ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hr : ¬r = 0
⊢ padicNorm p (q / r) * padicNorm p r = padicNorm p q
have rw : padicNorm p (q / r * r) = padicNorm p q
Tactic: rw [← padicNorm.mul, div_mul_cancel₀ _ hr]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hr : ¬r = 0
rw : padicNorm p (q / r * r) = padicNorm p q
⊢ padicNorm p (q / r) * padicNorm p r = padicNorm p q
have rw₁ : padicNorm p q = padicNorm p q
Tactic: rw [← padicNorm.mul, div_mul_cancel₀ _ hr]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ padicNorm p (↑z : ℚ) ≤ 1
have inl : padicNorm p (↑0 : ℚ) ≤ 1
Tactic: obtain rfl | hz := eq_or_ne z 0
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
inl : padicNorm p (↑0 : ℚ) ≤ 1
⊢ padicNorm p (↑z : ℚ) ≤ 1
have inr : ∀ (hz : z ≠ 0), padicNorm p (↑z : ℚ) ≤ 1
Tactic: obtain rfl | hz := eq_or_ne z 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ padicNorm p (↑z : ℚ) ≤ 1
have inr : HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑z : ℚ)) ≤ 1
Tactic: rw [padicNorm, if_neg (mod_cast hz)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ (if q + r = 0 then 0 else HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r))) ≤
    max (if q = 0 then 0 else HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q))
      (if r = 0 then 0 else HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p r))
have split_ifs : HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤
  max (HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)) (HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p r))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤
    max (HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)) (HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p r))
have apply : HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q) ∨
  HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p r)
Tactic: apply le_max_iff.2
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q) ∨
    HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p r)
have h₁ : HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)
Tactic: left
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)
have h₁ : LE.le (α := ℚ) 1 (↑p : ℚ)
Tactic: apply zpow_le_zpow_right₀
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
h₁ : LE.le (α := ℚ) 1 (↑p : ℚ)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)
have h₂ : -padicValRat p (q + r) ≤ -padicValRat p q
Tactic: apply zpow_le_zpow_right₀
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ -padicValRat p (q + r) ≤ -padicValRat p q
have h₁ : padicValRat p q ≤ padicValRat p (q + r)
Tactic: apply neg_le_neg
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
have this : padicValRat p q = min (padicValRat p q) (padicValRat p r)
Tactic: have : padicValRat p q = min (padicValRat p q) (padicValRat p r) := (min_eq_left h).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
this : padicValRat p q = min (padicValRat p q) (padicValRat p r)
⊢ padicValRat p q ≤ padicValRat p (q + r)
have h₁ : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
have inr : ∀
  (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 (q + r) ≤ max (padicNorm p q) (padicNorm p r)
Tactic: wlog hle : padicValRat p q ≤ padicValRat p r generalizing q r
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
inr :
  ∀
    (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 (q + r) ≤ max (padicNorm p q) (padicNorm p r)
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
have wlog : ∀ {q r : ℚ} (hle : padicValRat p q ≤ padicValRat p r), padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
Tactic: wlog hle : padicValRat p q ≤ padicValRat p r generalizing q r
Cleared hypotheses: q, r
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
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 (q + r) ≤ max (padicNorm p q) (padicNorm p r)
have inr : padicNorm p (r + q) ≤ max (padicNorm p r) (padicNorm p q)
Tactic: rw [add_comm, max_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q - r) ≤ max (padicNorm p q) (padicNorm p r)
have rw : padicNorm p (q + -r) ≤ max (padicNorm p q) (padicNorm p (-r))
Tactic: rw [sub_eq_add_neg, ← padicNorm.neg r]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
⊢ (↑(p ^ n) : ℤ) ∣ z ↔
    (if Eq (α := ℚ) (↑z : ℚ) 0 then 0 else HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑z : ℚ))) ≤
      HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
have pos : ∀ (hz : Eq (α := ℚ) (↑z : ℚ) 0), (↑(p ^ n) : ℤ) ∣ z ↔ 0 ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
Tactic: split_ifs with hz
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
pos : ∀ (hz : Eq (α := ℚ) (↑z : ℚ) 0), (↑(p ^ n) : ℤ) ∣ z ↔ 0 ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
⊢ (↑(p ^ n) : ℤ) ∣ z ↔
    (if Eq (α := ℚ) (↑z : ℚ) 0 then 0 else HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑z : ℚ))) ≤
      HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
have neg : ∀ (hz : ¬Eq (α := ℚ) (↑z : ℚ) 0),
  (↑(p ^ n) : ℤ) ∣ z ↔
    HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑z : ℚ)) ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
Tactic: split_ifs with hz
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : Eq (α := ℚ) (↑z : ℚ) 0
⊢ (↑(p ^ n) : ℤ) ∣ z ↔ 0 ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
have hz₁ : z = 0
Tactic: norm_cast at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬Eq (α := ℚ) (↑z : ℚ) 0
⊢ (↑(p ^ n) : ℤ) ∣ z ↔
    HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑z : ℚ)) ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
have neg : (↑(p ^ n) : ℤ) ∣ z ↔ LE.le (α := ℤ) (↑n : ℤ) (↑(multiplicity (↑p : ℤ) z) : ℤ)
Tactic: rw [zpow_le_zpow_iff_right₀, neg_le_neg_iff, padicValRat.of_int,
      padicValInt.of_ne_one_ne_zero hp.1.ne_one _]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬Eq (α := ℚ) (↑z : ℚ) 0
neg : (↑(p ^ n) : ℤ) ∣ z ↔ LE.le (α := ℤ) (↑n : ℤ) (↑(multiplicity (↑p : ℤ) z) : ℤ)
⊢ (↑(p ^ n) : ℤ) ∣ z ↔
    HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑z : ℚ)) ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
have rw : z ≠ 0
Tactic: rw [zpow_le_zpow_iff_right₀, neg_le_neg_iff, padicValRat.of_int,
      padicValInt.of_ne_one_ne_zero hp.1.ne_one _]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
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
⊢ (↑(p ^ n) : ℤ) ∣ z ↔
    HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑z : ℚ)) ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
have neg₁ : LT.lt (α := ℚ) 1 (↑p : ℚ)
Tactic: rw [zpow_le_zpow_iff_right₀, neg_le_neg_iff, padicValRat.of_int,
      padicValInt.of_ne_one_ne_zero hp.1.ne_one _]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬Eq (α := ℚ) (↑z : ℚ) 0
⊢ (↑(p ^ n) : ℤ) ∣ z ↔ LE.le (α := ℤ) (↑n : ℤ) (↑(multiplicity (↑p : ℤ) z) : ℤ)
have neg : (↑(p ^ n) : ℤ) ∣ z ↔ n ≤ multiplicity (↑p : ℤ) z
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬Eq (α := ℚ) (↑z : ℚ) 0
⊢ (↑(p ^ n) : ℤ) ∣ z ↔ n ≤ multiplicity (↑p : ℤ) z
have neg : (↑(p ^ n) : ℤ) ∣ z ↔ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ z
Tactic: rw [← FiniteMultiplicity.pow_dvd_iff_le_multiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬Eq (α := ℚ) (↑z : ℚ) 0
neg : (↑(p ^ n) : ℤ) ∣ z ↔ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ z
⊢ (↑(p ^ n) : ℤ) ∣ z ↔ n ≤ multiplicity (↑p : ℤ) z
have neg₁ : FiniteMultiplicity (↑p : ℤ) z
Tactic: rw [← FiniteMultiplicity.pow_dvd_iff_le_multiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬Eq (α := ℚ) (↑z : ℚ) 0
⊢ (↑(p ^ n) : ℤ) ∣ z ↔ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ z
have neg : (↑(p ^ n) : ℤ) ∣ z ↔ (↑(p ^ n) : ℤ) ∣ z
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p (↑m : ℚ) = 1 ↔ ¬(↑p : ℤ) ∣ m
have nth_rw : padicNorm p (↑m : ℚ) = 1 ↔ ¬(↑(HPow.hPow (β := ℕ) p 1) : ℤ) ∣ m
Tactic: nth_rw 2 [← pow_one p]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p (↑m : ℚ) = 1 ↔ ¬(↑(HPow.hPow (β := ℕ) p 1) : ℤ) ∣ m
have simp : padicNorm p (↑m : ℚ) = 1 ↔ (↑p : ℚ)⁻¹ < padicNorm p (↑m : ℚ)
Tactic: simp only [dvd_iff_norm_le, Nat.cast_one, zpow_neg, zpow_one, not_le]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p (↑m : ℚ) = 1 ↔ (↑p : ℚ)⁻¹ < padicNorm p (↑m : ℚ)
have mp : padicNorm p (↑m : ℚ) = 1 → (↑p : ℚ)⁻¹ < padicNorm p (↑m : ℚ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
mp : padicNorm p (↑m : ℚ) = 1 → (↑p : ℚ)⁻¹ < padicNorm p (↑m : ℚ)
⊢ padicNorm p (↑m : ℚ) = 1 ↔ (↑p : ℚ)⁻¹ < padicNorm p (↑m : ℚ)
have mpr : (↑p : ℚ)⁻¹ < padicNorm p (↑m : ℚ) → padicNorm p (↑m : ℚ) = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p (↑m : ℚ) = 1
⊢ (↑p : ℚ)⁻¹ < padicNorm p (↑m : ℚ)
have mp : LT.lt (α := ℚ) 1 (↑p : ℚ)
Tactic: rw [h, inv_lt_one₀]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p (↑m : ℚ) = 1
mp : LT.lt (α := ℚ) 1 (↑p : ℚ)
⊢ (↑p : ℚ)⁻¹ < padicNorm p (↑m : ℚ)
have mp₁ : LT.lt (α := ℚ) 0 (↑p : ℚ)
Tactic: rw [h, inv_lt_one₀]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p (↑m : ℚ) = 1
⊢ LT.lt (α := ℚ) 1 (↑p : ℚ)
have mp : 1 < p
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p (↑m : ℚ) = 1
⊢ LT.lt (α := ℚ) 0 (↑p : ℚ)
have mp : 0 < p
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ ((↑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
have pos : Eq (α := ℚ) (↑m : ℚ) 0 → LT.lt (α := ℚ) (↑p : ℚ)⁻¹ 0 → Eq (α := ℚ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
pos : Eq (α := ℚ) (↑m : ℚ) 0 → LT.lt (α := ℚ) (↑p : ℚ)⁻¹ 0 → Eq (α := ℚ) 0 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
have neg : ¬Eq (α := ℚ) (↑m : ℚ) 0 →
  (↑p : ℚ)⁻¹ < HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) →
    HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) = 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : Eq (α := ℚ) (↑m : ℚ) 0
⊢ LT.lt (α := ℚ) (↑p : ℚ)⁻¹ 0 → Eq (α := ℚ) 0 1
have pos : p < 0 → Eq (α := ℚ) (↑0 : ℚ) 1
Tactic: rw [inv_lt_zero, ← Nat.cast_zero, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : ¬Eq (α := ℚ) (↑m : ℚ) 0
⊢ LT.lt (α := ℚ) 1 (↑p : ℚ)
have norm_cast : 1 < p
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : ¬Eq (α := ℚ) (↑m : ℚ) 0
⊢ (↑p : ℚ)⁻¹ < HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) →
    HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) = 1
have this : LT.lt (α := ℚ) 1 (↑p : ℚ)
Tactic: have : 1 < (p : ℚ) := by norm_cast; exact Nat.Prime.one_lt (Fact.out : Nat.Prime p)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : ¬Eq (α := ℚ) (↑m : ℚ) 0
this : LT.lt (α := ℚ) 1 (↑p : ℚ)
⊢ (↑p : ℚ)⁻¹ < HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) →
    HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) = 1
have neg : -1 < -padicValRat p (↑m : ℚ) → HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) = 1
Tactic: rw [← zpow_neg_one, zpow_lt_zpow_iff_right₀ this]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : ¬Eq (α := ℚ) (↑m : ℚ) 0
this : LT.lt (α := ℚ) 1 (↑p : ℚ)
⊢ -1 < -padicValRat p (↑m : ℚ) → HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) = 1
have this₁ : 0 ≤ padicValRat p (↑m : ℚ)
Tactic: have : 0 ≤ padicValRat p m := by simp only [of_int, Nat.cast_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
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 : ℚ)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) = 1
have neg : -padicValRat p (↑m : ℚ) = 0
Tactic: rw [← zpow_zero (p : ℚ), zpow_right_inj₀]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
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
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) = 1
have neg₁ : LT.lt (α := ℚ) 0 (↑p : ℚ)
Tactic: rw [← zpow_zero (p : ℚ), zpow_right_inj₀]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
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 : ℚ)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑m : ℚ)) = 1
have neg₂ : Ne (α := ℚ) (↑p : ℚ) 1
Tactic: rw [← zpow_zero (p : ℚ), zpow_right_inj₀]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
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 : ℚ)
⊢ -padicValRat p (↑m : ℚ) = 0
have linarith : -padicValRat p (↑m : ℚ) < 0 →
  -1 + (HAdd.hAdd (α := ℤ) (-1) 1 - -padicValRat p (↑m : ℚ)) + (-padicValRat p (↑m : ℚ) + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
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
⊢ -padicValRat p (↑m : ℚ) = 0
have linarith₁ : 0 < -padicValRat p (↑m : ℚ) → -1 + (0 - padicValRat p (↑m : ℚ)) + (HAdd.hAdd (α := ℤ) 0 1 - -padicValRat p (↑m : ℚ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
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 : ℚ)
⊢ LT.lt (α := ℚ) 0 (↑p : ℚ)
have linarith : LE.le (α := ℚ) (↑p : ℚ) 0 → -1 + HSub.hSub (α := ℚ) 1 (↑p : ℚ) + HSub.hSub (α := ℚ) (↑p : ℚ) 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
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 : ℚ)
⊢ Ne (α := ℚ) (↑p : ℚ) 1
have linarith : Eq (α := ℚ) (↑p : ℚ) 1 → HSub.hSub (α := ℚ) 1 (↑p : ℚ) + HSub.hSub (α := ℚ) (↑p : ℚ) 1 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p (↑m : ℚ) < 1 ↔ (↑p : ℤ) ∣ m
have rw : ¬padicNorm p (↑m : ℚ) < 1 ↔ padicNorm p (↑m : ℚ) ≤ 1 ∧ ¬padicNorm p (↑m : ℚ) < 1
Tactic: rw [← not_iff_not, ← int_eq_one_iff, eq_iff_le_not_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p (↑m : ℚ) = 1 ↔ ¬p ∣ m
have rw : padicNorm p (↑m : ℚ) = 1 ↔ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑m : ℤ)
Tactic: rw [← Int.natCast_dvd_natCast, ← int_eq_one_iff, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
rw : padicNorm p (↑m : ℚ) = 1 ↔ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑m : ℤ)
⊢ padicNorm p (↑m : ℚ) = 1 ↔ ¬p ∣ m
have rw₁ : padicNorm p (↑m : ℚ) = 1 ↔ padicNorm p (↑(↑m : ℤ) : ℚ) = 1
Tactic: rw [← Int.natCast_dvd_natCast, ← int_eq_one_iff, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
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
⊢ padicNorm p (↑m : ℚ) = 1 ↔ ¬p ∣ m
have rw₂ : padicNorm p (↑m : ℚ) = 1 ↔ padicNorm p (↑m : ℚ) = 1
Tactic: rw [← Int.natCast_dvd_natCast, ← int_eq_one_iff, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p (↑m : ℚ) < 1 ↔ p ∣ m
have rw : padicNorm p (↑m : ℚ) < 1 ↔ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑m : ℤ)
Tactic: rw [← Int.natCast_dvd_natCast, ← int_lt_one_iff, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
rw : padicNorm p (↑m : ℚ) < 1 ↔ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑m : ℤ)
⊢ padicNorm p (↑m : ℚ) < 1 ↔ p ∣ m
have rw₁ : padicNorm p (↑m : ℚ) < 1 ↔ padicNorm p (↑(↑m : ℤ) : ℚ) < 1
Tactic: rw [← Int.natCast_dvd_natCast, ← int_lt_one_iff, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
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
⊢ padicNorm p (↑m : ℚ) < 1 ↔ p ∣ m
have rw₂ : padicNorm p (↑m : ℚ) < 1 ↔ padicNorm p (↑m : ℚ) < 1
Tactic: rw [← Int.natCast_dvd_natCast, ← int_lt_one_iff, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
a : ℚ
hp : Fact (Nat.Prime p)
H : 1 < padicNorm p a
⊢ ¬a.isInt = true
have contrapose! : ∀ (H : a.isInt = true), padicNorm p a ≤ 1
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
Goal:
p : ℕ
a : ℚ
hp : Fact (Nat.Prime p)
H : a.isInt = true
⊢ padicNorm p a ≤ 1
have rw : padicNorm p (↑a.num : ℚ) ≤ 1
Tactic: rw [Rat.eq_num_of_isInt H]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
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
⊢ padicNorm p (∑ i ∈ s, F i) < t
have inl : ∀ (hF : ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → padicNorm p (F i) < t), padicNorm p (∑ i ∈ ∅, F i) < t
Tactic: obtain rfl | hs := Finset.eq_empty_or_nonempty s
Cleared hypotheses: s, hF
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
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
⊢ padicNorm p (∑ i ∈ s, F i) < t
have inr : ∀ (hs : s.Nonempty), padicNorm p (∑ i ∈ s, F i) < t
Tactic: obtain rfl | hs := Finset.eq_empty_or_nonempty s
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNorm (goal)
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
⊢ padicNorm p (∑ i ∈ s, F i) ≤ t
have inl : ∀ (hF : ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → padicNorm p (F i) ≤ t), padicNorm p (∑ i ∈ ∅, F i) ≤ t
Tactic: obtain rfl | hs := Finset.eq_empty_or_nonempty s
Cleared hypotheses: s, hF