awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)
rwa :
  ∀ (h_norm : ‖x * y‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * ‖y‖) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
    (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), (x * y).valuation = x.valuation + y.valuation
⊢ (x * y).valuation = x.valuation + y.valuation
have rwa₁ : ∀ (h_norm : ‖x * y‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * HPow.hPow (α := ℝ) (↑p : ℝ) (-y.valuation))
  (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
  (x * y).valuation = x.valuation + y.valuation
Tactic: rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation hy,
    norm_eq_zpow_neg_valuation (mul_ne_zero hx hy), ← zpow_add₀ hp_pos.ne',
    zpow_right_inj₀ hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm
Cleared hypotheses: h_norm, hp_ne_one, hp_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)
rwa :
  ∀ (h_norm : ‖x * y‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * ‖y‖) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
    (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), (x * y).valuation = x.valuation + y.valuation
rwa₁ :
  ∀ (h_norm : ‖x * y‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * HPow.hPow (α := ℝ) (↑p : ℝ) (-y.valuation))
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
    (x * y).valuation = x.valuation + y.valuation
⊢ (x * y).valuation = x.valuation + y.valuation
have rwa₂ : ∀
  (h_norm :
    HPow.hPow (α := ℝ) (↑p : ℝ) (-(x * y).valuation) =
      HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * HPow.hPow (α := ℝ) (↑p : ℝ) (-y.valuation))
  (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
  (x * y).valuation = x.valuation + y.valuation
Tactic: rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation hy,
    norm_eq_zpow_neg_valuation (mul_ne_zero hx hy), ← zpow_add₀ hp_pos.ne',
    zpow_right_inj₀ hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm
Cleared hypotheses: h_norm, hp_ne_one, hp_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)
rwa :
  ∀ (h_norm : ‖x * y‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * ‖y‖) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
    (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), (x * y).valuation = x.valuation + y.valuation
rwa₁ :
  ∀ (h_norm : ‖x * y‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * HPow.hPow (α := ℝ) (↑p : ℝ) (-y.valuation))
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
    (x * y).valuation = x.valuation + y.valuation
rwa₂ :
  ∀
    (h_norm :
      HPow.hPow (α := ℝ) (↑p : ℝ) (-(x * y).valuation) =
        HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * HPow.hPow (α := ℝ) (↑p : ℝ) (-y.valuation))
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
    (x * y).valuation = x.valuation + y.valuation
⊢ (x * y).valuation = x.valuation + y.valuation
have rwa₃ : ∀
  (h_norm :
    HPow.hPow (α := ℝ) (↑p : ℝ) (-(x * y).valuation) = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation + -y.valuation))
  (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
  (x * y).valuation = x.valuation + y.valuation
Tactic: rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation hy,
    norm_eq_zpow_neg_valuation (mul_ne_zero hx hy), ← zpow_add₀ hp_pos.ne',
    zpow_right_inj₀ hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm
Cleared hypotheses: h_norm, hp_ne_one, hp_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)
rwa :
  ∀ (h_norm : ‖x * y‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * ‖y‖) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
    (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), (x * y).valuation = x.valuation + y.valuation
rwa₁ :
  ∀ (h_norm : ‖x * y‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * HPow.hPow (α := ℝ) (↑p : ℝ) (-y.valuation))
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
    (x * y).valuation = x.valuation + y.valuation
rwa₂ :
  ∀
    (h_norm :
      HPow.hPow (α := ℝ) (↑p : ℝ) (-(x * y).valuation) =
        HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * HPow.hPow (α := ℝ) (↑p : ℝ) (-y.valuation))
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
    (x * y).valuation = x.valuation + y.valuation
rwa₃ :
  ∀
    (h_norm :
      HPow.hPow (α := ℝ) (↑p : ℝ) (-(x * y).valuation) = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation + -y.valuation))
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
    (x * y).valuation = x.valuation + y.valuation
⊢ (x * y).valuation = x.valuation + y.valuation
have rwa₄ : ∀ (h_norm : -(x * y).valuation = -x.valuation + -y.valuation) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
  (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), (x * y).valuation = x.valuation + y.valuation
Tactic: rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation hy,
    norm_eq_zpow_neg_valuation (mul_ne_zero hx hy), ← zpow_add₀ hp_pos.ne',
    zpow_right_inj₀ hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm
Cleared hypotheses: h_norm, hp_ne_one, hp_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)
rwa :
  ∀ (h_norm : ‖x * y‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * ‖y‖) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
    (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), (x * y).valuation = x.valuation + y.valuation
rwa₁ :
  ∀ (h_norm : ‖x * y‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * HPow.hPow (α := ℝ) (↑p : ℝ) (-y.valuation))
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
    (x * y).valuation = x.valuation + y.valuation
rwa₂ :
  ∀
    (h_norm :
      HPow.hPow (α := ℝ) (↑p : ℝ) (-(x * y).valuation) =
        HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * HPow.hPow (α := ℝ) (↑p : ℝ) (-y.valuation))
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
    (x * y).valuation = x.valuation + y.valuation
rwa₃ :
  ∀
    (h_norm :
      HPow.hPow (α := ℝ) (↑p : ℝ) (-(x * y).valuation) = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation + -y.valuation))
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
    (x * y).valuation = x.valuation + y.valuation
rwa₄ :
  ∀ (h_norm : -(x * y).valuation = -x.valuation + -y.valuation) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
    (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), (x * y).valuation = x.valuation + y.valuation
⊢ (x * y).valuation = x.valuation + y.valuation
have rwa₅ : ∀ (h_norm : -(x * y).valuation = -(x.valuation + y.valuation)) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
  (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), (x * y).valuation = x.valuation + y.valuation
Tactic: rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation hy,
    norm_eq_zpow_neg_valuation (mul_ne_zero hx hy), ← zpow_add₀ hp_pos.ne',
    zpow_right_inj₀ hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm
Cleared hypotheses: h_norm, hp_ne_one, hp_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)
rwa :
  ∀ (h_norm : ‖x * y‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * ‖y‖) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
    (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), (x * y).valuation = x.valuation + y.valuation
rwa₁ :
  ∀ (h_norm : ‖x * y‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * HPow.hPow (α := ℝ) (↑p : ℝ) (-y.valuation))
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
    (x * y).valuation = x.valuation + y.valuation
rwa₂ :
  ∀
    (h_norm :
      HPow.hPow (α := ℝ) (↑p : ℝ) (-(x * y).valuation) =
        HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) * HPow.hPow (α := ℝ) (↑p : ℝ) (-y.valuation))
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
    (x * y).valuation = x.valuation + y.valuation
rwa₃ :
  ∀
    (h_norm :
      HPow.hPow (α := ℝ) (↑p : ℝ) (-(x * y).valuation) = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation + -y.valuation))
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
    (x * y).valuation = x.valuation + y.valuation
rwa₄ :
  ∀ (h_norm : -(x * y).valuation = -x.valuation + -y.valuation) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
    (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), (x * y).valuation = x.valuation + y.valuation
rwa₅ :
  ∀ (h_norm : -(x * y).valuation = -(x.valuation + y.valuation)) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
    (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), (x * y).valuation = x.valuation + y.valuation
⊢ (x * y).valuation = x.valuation + y.valuation
have rwa₆ : ∀ (h_norm : (x * y).valuation = x.valuation + y.valuation) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
  (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), (x * y).valuation = x.valuation + y.valuation
Tactic: rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation hy,
    norm_eq_zpow_neg_valuation (mul_ne_zero hx hy), ← zpow_add₀ hp_pos.ne',
    zpow_right_inj₀ hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm
Cleared hypotheses: h_norm, hp_ne_one, hp_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ x⁻¹.valuation = -x.valuation
have inl : valuation (p := p) 0⁻¹ = -valuation (p := p) 0
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
inl : valuation (p := p) 0⁻¹ = -valuation (p := p) 0
⊢ x⁻¹.valuation = -x.valuation
have inr : ∀ (hx : x ≠ 0), x⁻¹.valuation = -x.valuation
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
⊢ x⁻¹.valuation = -x.valuation
have h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
Tactic: have h_norm : ‖x⁻¹‖ = ‖x‖⁻¹ := norm_inv x
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
⊢ x⁻¹.valuation = -x.valuation
have hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
Tactic: have hp_ne_one : (p : ℝ) ≠ 1 := mod_cast (Fact.out : p.Prime).ne_one
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
⊢ x⁻¹.valuation = -x.valuation
have hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)
Tactic: have hp_pos : (0 : ℝ) < p := mod_cast NeZero.pos _
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)
⊢ x⁻¹.valuation = -x.valuation
have inr : ∀ (h_norm : ‖x⁻¹‖ = (HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation))⁻¹) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
  (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), x⁻¹.valuation = -x.valuation
Tactic: rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation <| inv_ne_zero hx,
    ← zpow_neg, zpow_right_inj₀ hp_pos hp_ne_one, neg_inj] at h_norm
Cleared hypotheses: h_norm, hp_ne_one, hp_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)
inr :
  ∀ (h_norm : ‖x⁻¹‖ = (HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation))⁻¹) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
    (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), x⁻¹.valuation = -x.valuation
⊢ x⁻¹.valuation = -x.valuation
have inr₁ : ∀ (h_norm : HPow.hPow (α := ℝ) (↑p : ℝ) (-x⁻¹.valuation) = (HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation))⁻¹)
  (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), x⁻¹.valuation = -x.valuation
Tactic: rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation <| inv_ne_zero hx,
    ← zpow_neg, zpow_right_inj₀ hp_pos hp_ne_one, neg_inj] at h_norm
Cleared hypotheses: h_norm, hp_ne_one, hp_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)
inr :
  ∀ (h_norm : ‖x⁻¹‖ = (HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation))⁻¹) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
    (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), x⁻¹.valuation = -x.valuation
inr₁ :
  ∀ (h_norm : HPow.hPow (α := ℝ) (↑p : ℝ) (-x⁻¹.valuation) = (HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation))⁻¹)
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), x⁻¹.valuation = -x.valuation
⊢ x⁻¹.valuation = -x.valuation
have inr₂ : ∀ (h_norm : HPow.hPow (α := ℝ) (↑p : ℝ) (-x⁻¹.valuation) = HPow.hPow (α := ℝ) (↑p : ℝ) (- -x.valuation))
  (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), x⁻¹.valuation = -x.valuation
Tactic: rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation <| inv_ne_zero hx,
    ← zpow_neg, zpow_right_inj₀ hp_pos hp_ne_one, neg_inj] at h_norm
Cleared hypotheses: h_norm, hp_ne_one, hp_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)
inr :
  ∀ (h_norm : ‖x⁻¹‖ = (HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation))⁻¹) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
    (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), x⁻¹.valuation = -x.valuation
inr₁ :
  ∀ (h_norm : HPow.hPow (α := ℝ) (↑p : ℝ) (-x⁻¹.valuation) = (HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation))⁻¹)
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), x⁻¹.valuation = -x.valuation
inr₂ :
  ∀ (h_norm : HPow.hPow (α := ℝ) (↑p : ℝ) (-x⁻¹.valuation) = HPow.hPow (α := ℝ) (↑p : ℝ) (- -x.valuation))
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), x⁻¹.valuation = -x.valuation
⊢ x⁻¹.valuation = -x.valuation
have inr₃ : ∀ (h_norm : -x⁻¹.valuation = - -x.valuation) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
  x⁻¹.valuation = -x.valuation
Tactic: rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation <| inv_ne_zero hx,
    ← zpow_neg, zpow_right_inj₀ hp_pos hp_ne_one, neg_inj] at h_norm
Cleared hypotheses: h_norm, hp_ne_one, hp_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)
inr :
  ∀ (h_norm : ‖x⁻¹‖ = (HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation))⁻¹) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
    (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), x⁻¹.valuation = -x.valuation
inr₁ :
  ∀ (h_norm : HPow.hPow (α := ℝ) (↑p : ℝ) (-x⁻¹.valuation) = (HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation))⁻¹)
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), x⁻¹.valuation = -x.valuation
inr₂ :
  ∀ (h_norm : HPow.hPow (α := ℝ) (↑p : ℝ) (-x⁻¹.valuation) = HPow.hPow (α := ℝ) (↑p : ℝ) (- -x.valuation))
    (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), x⁻¹.valuation = -x.valuation
inr₃ :
  ∀ (h_norm : -x⁻¹.valuation = - -x.valuation) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1)
    (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)), x⁻¹.valuation = -x.valuation
⊢ x⁻¹.valuation = -x.valuation
have inr₄ : ∀ (h_norm : x⁻¹.valuation = -x.valuation) (hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1) (hp_pos : LT.lt (α := ℝ) 0 (↑p : ℝ)),
  x⁻¹.valuation = -x.valuation
Tactic: rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation <| inv_ne_zero hx,
    ← zpow_neg, zpow_right_inj₀ hp_pos hp_ne_one, neg_inj] at h_norm
Cleared hypotheses: h_norm, hp_ne_one, hp_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
⊢ (x ^ (n + 1)).valuation = (↑(n + 1) : ℤ) * x.valuation
have inl : (HPow.hPow (α := ℚ_[p]) 0 (n + 1)).valuation = (↑(n + 1) : ℤ) * valuation (p := p) 0
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
inl : (HPow.hPow (α := ℚ_[p]) 0 (n + 1)).valuation = (↑(n + 1) : ℤ) * valuation (p := p) 0
⊢ (x ^ (n + 1)).valuation = (↑(n + 1) : ℤ) * x.valuation
have inr : ∀ (hx : x ≠ 0), (x ^ (n + 1)).valuation = (↑(n + 1) : ℤ) * x.valuation
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
⊢ (x ^ Int.negSucc n).valuation = Int.negSucc n * x.valuation
have simp : HAdd.hAdd (α := ℤ) (-1) (-(↑n : ℤ)) = Int.negSucc n ∨ x.valuation = 0
Tactic: simp [← neg_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ addValuationDef (p := p) 0 = ⊤
have rw : (if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : WithTop ℤ)) = ⊤
Tactic: rw [addValuationDef, if_pos rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : (if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : WithTop ℤ)) = ⊤
⊢ addValuationDef (p := p) 0 = ⊤
have rw₁ : Eq (α := WithTop ℤ) ⊤ ⊤
Tactic: rw [addValuationDef, if_pos rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ addValuationDef (p := p) 1 = 0
have rw : (if Eq (α := ℚ_[p]) 1 0 then ⊤ else (↑(valuation (p := p) 1) : WithTop ℤ)) = 0
Tactic: rw [addValuationDef, if_neg one_ne_zero, valuation_one, WithTop.coe_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : (if Eq (α := ℚ_[p]) 1 0 then ⊤ else (↑(valuation (p := p) 1) : WithTop ℤ)) = 0
⊢ addValuationDef (p := p) 1 = 0
have rw₁ : (↑(valuation (p := p) 1) : WithTop ℤ) = 0
Tactic: rw [addValuationDef, if_neg one_ne_zero, valuation_one, WithTop.coe_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : (if Eq (α := ℚ_[p]) 1 0 then ⊤ else (↑(valuation (p := p) 1) : WithTop ℤ)) = 0
rw₁ : (↑(valuation (p := p) 1) : WithTop ℤ) = 0
⊢ addValuationDef (p := p) 1 = 0
have rw₂ : Eq (α := WithTop ℤ) (↑0 : WithTop ℤ) 0
Tactic: rw [addValuationDef, if_neg one_ne_zero, valuation_one, WithTop.coe_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : (if Eq (α := ℚ_[p]) 1 0 then ⊤ else (↑(valuation (p := p) 1) : WithTop ℤ)) = 0
rw₁ : (↑(valuation (p := p) 1) : WithTop ℤ) = 0
rw₂ : Eq (α := WithTop ℤ) (↑0 : WithTop ℤ) 0
⊢ addValuationDef (p := p) 1 = 0
have rw₃ : Eq (α := WithTop ℤ) 0 0
Tactic: rw [addValuationDef, if_neg one_ne_zero, valuation_one, WithTop.coe_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) =
    (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
have pos : ∀ (hx : x = 0),
  (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) =
    (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
pos :
  ∀ (hx : x = 0),
    (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) =
      (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
⊢ (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) =
    (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
have neg : ∀ (hx : ¬x = 0),
  (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) =
    (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x = 0
⊢ (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) =
    (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
have pos : (if 0 * y = 0 then ⊤ else (↑(0 * y).valuation : WithTop ℤ)) =
  (if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : WithTop ℤ)) +
    if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
Tactic: rw [hx, if_pos rfl, zero_mul, if_pos rfl, WithTop.top_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x = 0
pos :
  (if 0 * y = 0 then ⊤ else (↑(0 * y).valuation : WithTop ℤ)) =
    (if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : WithTop ℤ)) +
      if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
⊢ (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) =
    (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
have pos₁ : (if 0 * y = 0 then ⊤ else (↑(0 * y).valuation : WithTop ℤ)) = ⊤ + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
Tactic: rw [hx, if_pos rfl, zero_mul, if_pos rfl, WithTop.top_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x = 0
pos :
  (if 0 * y = 0 then ⊤ else (↑(0 * y).valuation : WithTop ℤ)) =
    (if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : WithTop ℤ)) +
      if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
pos₁ : (if 0 * y = 0 then ⊤ else (↑(0 * y).valuation : WithTop ℤ)) = ⊤ + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
⊢ (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) =
    (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
have pos₂ : (if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : WithTop ℤ)) =
  ⊤ + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
Tactic: rw [hx, if_pos rfl, zero_mul, if_pos rfl, WithTop.top_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x = 0
pos :
  (if 0 * y = 0 then ⊤ else (↑(0 * y).valuation : WithTop ℤ)) =
    (if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : WithTop ℤ)) +
      if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
pos₁ : (if 0 * y = 0 then ⊤ else (↑(0 * y).valuation : WithTop ℤ)) = ⊤ + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
pos₂ :
  (if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : WithTop ℤ)) =
    ⊤ + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
⊢ (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) =
    (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
have pos₃ : ⊤ = ⊤ + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
Tactic: rw [hx, if_pos rfl, zero_mul, if_pos rfl, WithTop.top_add]