awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x 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)
have pos : x * y = 0 → x = 0 → y = 0 → 0 = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
pos : x * y = 0 → x = 0 → y = 0 → 0 = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
⊢ (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)
have neg : x * y = 0 → x = 0 → ¬y = 0 → 0 = 0 * exp (-padicValRat p y)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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)
⊢ (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)
have pos₁ : x * y = 0 → ¬x = 0 → y = 0 → 0 = exp (-padicValRat p x) * 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ (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)
have neg₁ : x * y = 0 → ¬x = 0 → ¬y = 0 → 0 = exp (-padicValRat p x) * exp (-padicValRat p y)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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)
⊢ (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)
have pos₂ : ¬x * y = 0 → x = 0 → y = 0 → exp (-padicValRat p (x * y)) = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ (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)
have neg₂ : ¬x * y = 0 → x = 0 → ¬y = 0 → exp (-padicValRat p (x * y)) = 0 * exp (-padicValRat p y)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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)
⊢ (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)
have pos₃ : ¬x * y = 0 → ¬x = 0 → y = 0 → exp (-padicValRat p (x * y)) = exp (-padicValRat p x) * 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ (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)
have neg₃ : ¬x * y = 0 → ¬x = 0 → ¬y = 0 → exp (-padicValRat p (x * y)) = exp (-padicValRat p x) * exp (-padicValRat p y)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
⊢ (if x + y = 0 then 0 else exp (-padicValRat p (x + y))) ≤
    max (if x = 0 then 0 else exp (-padicValRat p x)) (if y = 0 then 0 else exp (-padicValRat p y))
have pos : x + y = 0 → x = 0 → y = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
pos : x + y = 0 → x = 0 → y = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)
⊢ (if x + y = 0 then 0 else exp (-padicValRat p (x + y))) ≤
    max (if x = 0 then 0 else exp (-padicValRat p x)) (if y = 0 then 0 else exp (-padicValRat p y))
have neg : x + y = 0 → x = 0 → ¬y = 0 → 0 ≤ max 0 (exp (-padicValRat p y))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
pos : x + y = 0 → x = 0 → y = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)
neg : x + y = 0 → x = 0 → ¬y = 0 → 0 ≤ max 0 (exp (-padicValRat p y))
⊢ (if x + y = 0 then 0 else exp (-padicValRat p (x + y))) ≤
    max (if x = 0 then 0 else exp (-padicValRat p x)) (if y = 0 then 0 else exp (-padicValRat p y))
have pos₁ : x + y = 0 → ¬x = 0 → y = 0 → 0 ≤ max (exp (-padicValRat p x)) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
pos : x + y = 0 → x = 0 → y = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)
neg : x + y = 0 → x = 0 → ¬y = 0 → 0 ≤ max 0 (exp (-padicValRat p y))
pos₁ : x + y = 0 → ¬x = 0 → y = 0 → 0 ≤ max (exp (-padicValRat p x)) 0
⊢ (if x + y = 0 then 0 else exp (-padicValRat p (x + y))) ≤
    max (if x = 0 then 0 else exp (-padicValRat p x)) (if y = 0 then 0 else exp (-padicValRat p y))
have neg₁ : x + y = 0 → ¬x = 0 → ¬y = 0 → 0 ≤ max (exp (-padicValRat p x)) (exp (-padicValRat p y))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
pos : x + y = 0 → x = 0 → y = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)
neg : x + y = 0 → x = 0 → ¬y = 0 → 0 ≤ max 0 (exp (-padicValRat p y))
pos₁ : x + y = 0 → ¬x = 0 → y = 0 → 0 ≤ max (exp (-padicValRat p x)) 0
neg₁ : x + y = 0 → ¬x = 0 → ¬y = 0 → 0 ≤ max (exp (-padicValRat p x)) (exp (-padicValRat p y))
⊢ (if x + y = 0 then 0 else exp (-padicValRat p (x + y))) ≤
    max (if x = 0 then 0 else exp (-padicValRat p x)) (if y = 0 then 0 else exp (-padicValRat p y))
have pos₂ : ¬x + y = 0 → x = 0 → y = 0 → exp (-padicValRat p (x + y)) ≤ max 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
pos : x + y = 0 → x = 0 → y = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)
neg : x + y = 0 → x = 0 → ¬y = 0 → 0 ≤ max 0 (exp (-padicValRat p y))
pos₁ : x + y = 0 → ¬x = 0 → y = 0 → 0 ≤ max (exp (-padicValRat p x)) 0
neg₁ : x + y = 0 → ¬x = 0 → ¬y = 0 → 0 ≤ max (exp (-padicValRat p x)) (exp (-padicValRat p y))
pos₂ : ¬x + y = 0 → x = 0 → y = 0 → exp (-padicValRat p (x + y)) ≤ max 0 0
⊢ (if x + y = 0 then 0 else exp (-padicValRat p (x + y))) ≤
    max (if x = 0 then 0 else exp (-padicValRat p x)) (if y = 0 then 0 else exp (-padicValRat p y))
have neg₂ : ¬x + y = 0 → x = 0 → ¬y = 0 → exp (-padicValRat p (x + y)) ≤ max 0 (exp (-padicValRat p y))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
pos : x + y = 0 → x = 0 → y = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)
neg : x + y = 0 → x = 0 → ¬y = 0 → 0 ≤ max 0 (exp (-padicValRat p y))
pos₁ : x + y = 0 → ¬x = 0 → y = 0 → 0 ≤ max (exp (-padicValRat p x)) 0
neg₁ : x + y = 0 → ¬x = 0 → ¬y = 0 → 0 ≤ max (exp (-padicValRat p x)) (exp (-padicValRat p y))
pos₂ : ¬x + y = 0 → x = 0 → y = 0 → exp (-padicValRat p (x + y)) ≤ max 0 0
neg₂ : ¬x + y = 0 → x = 0 → ¬y = 0 → exp (-padicValRat p (x + y)) ≤ max 0 (exp (-padicValRat p y))
⊢ (if x + y = 0 then 0 else exp (-padicValRat p (x + y))) ≤
    max (if x = 0 then 0 else exp (-padicValRat p x)) (if y = 0 then 0 else exp (-padicValRat p y))
have pos₃ : ¬x + y = 0 → ¬x = 0 → y = 0 → exp (-padicValRat p (x + y)) ≤ max (exp (-padicValRat p x)) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
pos : x + y = 0 → x = 0 → y = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)
neg : x + y = 0 → x = 0 → ¬y = 0 → 0 ≤ max 0 (exp (-padicValRat p y))
pos₁ : x + y = 0 → ¬x = 0 → y = 0 → 0 ≤ max (exp (-padicValRat p x)) 0
neg₁ : x + y = 0 → ¬x = 0 → ¬y = 0 → 0 ≤ max (exp (-padicValRat p x)) (exp (-padicValRat p y))
pos₂ : ¬x + y = 0 → x = 0 → y = 0 → exp (-padicValRat p (x + y)) ≤ max 0 0
neg₂ : ¬x + y = 0 → x = 0 → ¬y = 0 → exp (-padicValRat p (x + y)) ≤ max 0 (exp (-padicValRat p y))
pos₃ : ¬x + y = 0 → ¬x = 0 → y = 0 → exp (-padicValRat p (x + y)) ≤ max (exp (-padicValRat p x)) 0
⊢ (if x + y = 0 then 0 else exp (-padicValRat p (x + y))) ≤
    max (if x = 0 then 0 else exp (-padicValRat p x)) (if y = 0 then 0 else exp (-padicValRat p y))
have neg₃ : ¬x + y = 0 → ¬x = 0 → ¬y = 0 → exp (-padicValRat p (x + y)) ≤ max (exp (-padicValRat p x)) (exp (-padicValRat p y))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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)) ≤ max (exp (-padicValRat p x)) (exp (-padicValRat p y))
have neg : padicValRat p x ≤ padicValRat p (x + y) ∨ padicValRat p y ≤ padicValRat p (x + y)
Tactic: simp_all [-exp_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : ¬x + y = 0
h_1 : ¬x = 0
h_2 : ¬y = 0
⊢ padicValRat p x ≤ padicValRat p (x + y) ∨ padicValRat p y ≤ padicValRat p (x + y)
have neg : min (padicValRat p x) (padicValRat p y) ≤ padicValRat p (x + y)
Tactic: rw [← min_le_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have simp : LE.le (α := WithZero (Multiplicative ℤ)) (if x = 0 then 0 else exp (-(↑(padicValInt p x) : ℤ))) 1
Tactic: simp only [← Rat.padicValuation_cast, Rat.padicValuation, Valuation.coe_mk,
    MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, Rat.intCast_eq_zero_iff, padicValRat.of_int]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (if x = 0 then 0 else exp (-(↑(padicValInt p x) : ℤ))) 1
have pos : x = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
pos : x = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 1
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (if x = 0 then 0 else exp (-(↑(padicValInt p x) : ℤ))) 1
have neg : ¬x = 0 → LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑(padicValInt p x) : ℤ))) 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
h : ¬x = 0
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑(padicValInt p x) : ℤ))) 1
have neg : LE.le (α := ℤ) (-(↑(padicValInt p x) : ℤ)) (log 1)
Tactic: rw [← le_log_iff_exp_le]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
h : ¬x = 0
neg : LE.le (α := ℤ) (-(↑(padicValInt p x) : ℤ)) (log 1)
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑(padicValInt p x) : ℤ))) 1
have neg₁ : Ne (α := WithZero (Multiplicative ℤ)) 1 0
Tactic: rw [← le_log_iff_exp_le]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
⊢ Eq (α := WithZero (Multiplicative ℤ))
      ((padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    ¬(↑p : ℤ) ∣ x
have simp : Eq (α := WithZero (Multiplicative ℤ)) (if x = 0 then 0 else exp (-(↑(padicValInt p x) : ℤ))) 1 ↔ ¬(↑p : ℤ) ∣ x
Tactic: simp only [← Rat.padicValuation_cast, Rat.padicValuation, Valuation.coe_mk,
    MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, Rat.intCast_eq_zero_iff, padicValRat.of_int]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
⊢ Eq (α := WithZero (Multiplicative ℤ)) (if x = 0 then 0 else exp (-(↑(padicValInt p x) : ℤ))) 1 ↔ ¬(↑p : ℤ) ∣ x
have pos : x = 0 → (Eq (α := WithZero (Multiplicative ℤ)) 0 1 ↔ ¬(↑p : ℤ) ∣ x)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
pos : x = 0 → (Eq (α := WithZero (Multiplicative ℤ)) 0 1 ↔ ¬(↑p : ℤ) ∣ x)
⊢ Eq (α := WithZero (Multiplicative ℤ)) (if x = 0 then 0 else exp (-(↑(padicValInt p x) : ℤ))) 1 ↔ ¬(↑p : ℤ) ∣ x
have neg : ¬x = 0 → (Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(padicValInt p x) : ℤ))) 1 ↔ ¬(↑p : ℤ) ∣ x)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
h : ¬x = 0
⊢ Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(padicValInt p x) : ℤ))) 1 ↔ ¬(↑p : ℤ) ∣ x
have neg : Eq (α := ℤ) (-(↑(padicValInt p x) : ℤ)) 0 ↔ ¬(↑p : ℤ) ∣ x
Tactic: rw [← exp_zero, exp_injective.eq_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    ¬p ∣ x.den
have nth_rw : LE.le (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ)) ↔
  Eq (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
Tactic: nth_rw 1 [← x.num_div_den, map_div₀, ← Int.natCast_dvd_natCast, ← Int.padicValuation_eq_one_iff,
    Rat.padicValuation_cast, ← Int.cast_natCast, Rat.padicValuation_cast, div_le_one₀]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
nth_rw :
  LE.le (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ)) ↔
    Eq (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    ¬p ∣ x.den
have nth_rw₁ : LT.lt (α := WithZero (Multiplicative ℤ)) (0 : WithZero (Multiplicative ℤ))
  ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
Tactic: nth_rw 1 [← x.num_div_den, map_div₀, ← Int.natCast_dvd_natCast, ← Int.padicValuation_eq_one_iff,
    Rat.padicValuation_cast, ← Int.cast_natCast, Rat.padicValuation_cast, div_le_one₀]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ)) ↔
    Eq (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
have inl : ∀
  (h :
    Eq (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))),
  LE.le (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ)) ↔
    Eq (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
Tactic: rcases (Int.padicValuation_le_one p x.den).eq_or_lt with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
inl :
  ∀
    (h :
      Eq (α := WithZero (Multiplicative ℤ))
        ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))),
    LE.le (α := WithZero (Multiplicative ℤ))
        ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
        ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ)) ↔
      Eq (α := WithZero (Multiplicative ℤ))
        ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ)) ↔
    Eq (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
have inr : ∀
  (h :
    LT.lt (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))),
  LE.le (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ)) ↔
    Eq (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
Tactic: rcases (Int.padicValuation_le_one p x.den).eq_or_lt with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
h :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ)) ↔
    Eq (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
have inr : LT.lt (α := WithZero (Multiplicative ℤ))
  ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
  ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
Tactic: simp only [h.ne, iff_false, not_le]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
h :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
have inr : ∀
  (h' :
    Eq (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))),
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
Tactic: rcases (Int.padicValuation_le_one p x.num).eq_or_lt with h' | h'