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
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 ℤ)
pos₃ : ⊤ = ⊤ + 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₄ : Eq (α := 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
⊢ (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 : ∀ (hy : y = 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 hy : y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
pos :
  ∀ (hy : y = 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 : ∀ (hy : ¬y = 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 hy : y = 0
-- 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
⊢ (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 x * 0 = 0 then ⊤ else (↑(x * 0).valuation : WithTop ℤ)) =
  (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) +
    if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : WithTop ℤ)
Tactic: rw [hy, if_pos rfl, mul_zero, if_pos rfl, WithTop.add_top]
-- 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
pos :
  (if x * 0 = 0 then ⊤ else (↑(x * 0).valuation : WithTop ℤ)) =
    (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) +
      if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : 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 x * 0 = 0 then ⊤ else (↑(x * 0).valuation : WithTop ℤ)) = (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) + ⊤
Tactic: rw [hy, if_pos rfl, mul_zero, if_pos rfl, WithTop.add_top]
-- 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
pos :
  (if x * 0 = 0 then ⊤ else (↑(x * 0).valuation : WithTop ℤ)) =
    (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) +
      if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : WithTop ℤ)
pos₁ :
  (if x * 0 = 0 then ⊤ else (↑(x * 0).valuation : WithTop ℤ)) = (if x = 0 then ⊤ else (↑x.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 x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) + ⊤
Tactic: rw [hy, if_pos rfl, mul_zero, if_pos rfl, WithTop.add_top]
-- 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
pos :
  (if x * 0 = 0 then ⊤ else (↑(x * 0).valuation : WithTop ℤ)) =
    (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) +
      if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : WithTop ℤ)
pos₁ :
  (if x * 0 = 0 then ⊤ else (↑(x * 0).valuation : WithTop ℤ)) = (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) + ⊤
pos₂ :
  (if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : WithTop ℤ)) =
    (if x = 0 then ⊤ else (↑x.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 x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) + ⊤
Tactic: rw [hy, if_pos rfl, mul_zero, if_pos rfl, WithTop.add_top]
-- 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
pos :
  (if x * 0 = 0 then ⊤ else (↑(x * 0).valuation : WithTop ℤ)) =
    (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) +
      if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : WithTop ℤ)
pos₁ :
  (if x * 0 = 0 then ⊤ else (↑(x * 0).valuation : WithTop ℤ)) = (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) + ⊤
pos₂ :
  (if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : WithTop ℤ)) =
    (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) + ⊤
pos₃ : ⊤ = (if x = 0 then ⊤ else (↑x.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₄ : Eq (α := WithTop ℤ) ⊤ ⊤
Tactic: rw [hy, if_pos rfl, mul_zero, if_pos rfl, WithTop.add_top]
-- 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
⊢ (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 : (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) =
  (↑x.valuation : WithTop ℤ) + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
Tactic: rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
        valuation_mul hx hy]
-- 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
neg :
  (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) =
    (↑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₁ : (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) = (↑x.valuation : WithTop ℤ) + (↑y.valuation : WithTop ℤ)
Tactic: rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
        valuation_mul hx hy]
-- 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
neg :
  (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) =
    (↑x.valuation : WithTop ℤ) + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
neg₁ :
  (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) = (↑x.valuation : WithTop ℤ) + (↑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₂ : (↑(x * y).valuation : WithTop ℤ) = (↑x.valuation : WithTop ℤ) + (↑y.valuation : WithTop ℤ)
Tactic: rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
        valuation_mul hx hy]
-- 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
neg :
  (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) =
    (↑x.valuation : WithTop ℤ) + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
neg₁ :
  (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) = (↑x.valuation : WithTop ℤ) + (↑y.valuation : WithTop ℤ)
neg₂ : (↑(x * y).valuation : WithTop ℤ) = (↑x.valuation : WithTop ℤ) + (↑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₃ : (↑(x * y).valuation : WithTop ℤ) = (↑(x.valuation + y.valuation) : WithTop ℤ)
Tactic: rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
        valuation_mul hx hy]
-- 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
neg :
  (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) =
    (↑x.valuation : WithTop ℤ) + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
neg₁ :
  (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) = (↑x.valuation : WithTop ℤ) + (↑y.valuation : WithTop ℤ)
neg₂ : (↑(x * y).valuation : WithTop ℤ) = (↑x.valuation : WithTop ℤ) + (↑y.valuation : WithTop ℤ)
neg₃ : (↑(x * y).valuation : WithTop ℤ) = (↑(x.valuation + 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₄ : (x * y).valuation = x.valuation + y.valuation
Tactic: rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
        valuation_mul hx hy]
-- 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
neg :
  (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) =
    (↑x.valuation : WithTop ℤ) + if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)
neg₁ :
  (if x * y = 0 then ⊤ else (↑(x * y).valuation : WithTop ℤ)) = (↑x.valuation : WithTop ℤ) + (↑y.valuation : WithTop ℤ)
neg₂ : (↑(x * y).valuation : WithTop ℤ) = (↑x.valuation : WithTop ℤ) + (↑y.valuation : WithTop ℤ)
neg₃ : (↑(x * y).valuation : WithTop ℤ) = (↑(x.valuation + y.valuation) : WithTop ℤ)
neg₄ : (x * y).valuation = x.valuation + y.valuation
⊢ (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₅ : x.valuation + y.valuation = x.valuation + y.valuation
Tactic: rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
        valuation_mul hx hy]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ min (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 ℤ)
have pos : ∀ (hxy : x + y = 0),
  min (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 ℤ)
Tactic: by_cases hxy : x + y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
pos :
  ∀ (hxy : x + y = 0),
    min (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 ℤ)
⊢ min (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 ℤ)
have neg : ∀ (hxy : ¬x + y = 0),
  min (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 ℤ)
Tactic: by_cases hxy : x + y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y = 0
⊢ min (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 ℤ)
have pos : min (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) (if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)) ≤ ⊤
Tactic: rw [hxy, if_pos rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
⊢ min (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 ℤ)
have pos : ∀ (hx : x = 0),
  min (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 ℤ)
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]
hxy : ¬x + y = 0
pos :
  ∀ (hx : x = 0),
    min (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 ℤ)
⊢ min (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 ℤ)
have neg : ∀ (hx : ¬x = 0),
  min (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 ℤ)
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]
hxy : ¬x + y = 0
hx : x = 0
⊢ min (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 ℤ)
have pos : (if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)) ≤ ⊤
Tactic: rw [hx, if_pos rfl, min_eq_right, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
⊢ min (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 ℤ)
have pos : ∀ (hy : y = 0),
  min (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 ℤ)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
pos :
  ∀ (hy : y = 0),
    min (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 ℤ)
⊢ min (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 ℤ)
have neg : ∀ (hy : ¬y = 0),
  min (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 ℤ)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ min (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 ℤ)
have pos : (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) ≤ ⊤
Tactic: rw [hy, if_pos rfl, min_eq_left, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (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 ℤ)
have neg : min x.valuation y.valuation ≤ (x + y).valuation
Tactic: rw [if_neg hx, if_neg hy, if_neg hxy, ← WithTop.coe_min, WithTop.coe_le_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
⊢ (if x * x_1 = 0 then 0 else exp (-(x * x_1).valuation)) =
    (if x = 0 then 0 else exp (-x.valuation)) * if x_1 = 0 then 0 else exp (-x_1.valuation)
have pos : x * x_1 = 0 → x = 0 → x_1 = 0 → 0 = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
pos : x * x_1 = 0 → x = 0 → x_1 = 0 → 0 = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
⊢ (if x * x_1 = 0 then 0 else exp (-(x * x_1).valuation)) =
    (if x = 0 then 0 else exp (-x.valuation)) * if x_1 = 0 then 0 else exp (-x_1.valuation)
have neg : x * x_1 = 0 → x = 0 → ¬x_1 = 0 → 0 = 0 * exp (-x_1.valuation)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
pos : x * x_1 = 0 → x = 0 → x_1 = 0 → 0 = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
neg : x * x_1 = 0 → x = 0 → ¬x_1 = 0 → 0 = 0 * exp (-x_1.valuation)
⊢ (if x * x_1 = 0 then 0 else exp (-(x * x_1).valuation)) =
    (if x = 0 then 0 else exp (-x.valuation)) * if x_1 = 0 then 0 else exp (-x_1.valuation)
have pos₁ : x * x_1 = 0 → ¬x = 0 → x_1 = 0 → 0 = exp (-x.valuation) * 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
pos : x * x_1 = 0 → x = 0 → x_1 = 0 → 0 = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
neg : x * x_1 = 0 → x = 0 → ¬x_1 = 0 → 0 = 0 * exp (-x_1.valuation)
pos₁ : x * x_1 = 0 → ¬x = 0 → x_1 = 0 → 0 = exp (-x.valuation) * 0
⊢ (if x * x_1 = 0 then 0 else exp (-(x * x_1).valuation)) =
    (if x = 0 then 0 else exp (-x.valuation)) * if x_1 = 0 then 0 else exp (-x_1.valuation)
have neg₁ : x * x_1 = 0 → ¬x = 0 → ¬x_1 = 0 → 0 = exp (-x.valuation) * exp (-x_1.valuation)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
pos : x * x_1 = 0 → x = 0 → x_1 = 0 → 0 = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
neg : x * x_1 = 0 → x = 0 → ¬x_1 = 0 → 0 = 0 * exp (-x_1.valuation)
pos₁ : x * x_1 = 0 → ¬x = 0 → x_1 = 0 → 0 = exp (-x.valuation) * 0
neg₁ : x * x_1 = 0 → ¬x = 0 → ¬x_1 = 0 → 0 = exp (-x.valuation) * exp (-x_1.valuation)
⊢ (if x * x_1 = 0 then 0 else exp (-(x * x_1).valuation)) =
    (if x = 0 then 0 else exp (-x.valuation)) * if x_1 = 0 then 0 else exp (-x_1.valuation)
have pos₂ : ¬x * x_1 = 0 → x = 0 → x_1 = 0 → exp (-(x * x_1).valuation) = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
pos : x * x_1 = 0 → x = 0 → x_1 = 0 → 0 = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
neg : x * x_1 = 0 → x = 0 → ¬x_1 = 0 → 0 = 0 * exp (-x_1.valuation)
pos₁ : x * x_1 = 0 → ¬x = 0 → x_1 = 0 → 0 = exp (-x.valuation) * 0
neg₁ : x * x_1 = 0 → ¬x = 0 → ¬x_1 = 0 → 0 = exp (-x.valuation) * exp (-x_1.valuation)
pos₂ : ¬x * x_1 = 0 → x = 0 → x_1 = 0 → exp (-(x * x_1).valuation) = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
⊢ (if x * x_1 = 0 then 0 else exp (-(x * x_1).valuation)) =
    (if x = 0 then 0 else exp (-x.valuation)) * if x_1 = 0 then 0 else exp (-x_1.valuation)
have neg₂ : ¬x * x_1 = 0 → x = 0 → ¬x_1 = 0 → exp (-(x * x_1).valuation) = 0 * exp (-x_1.valuation)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
pos : x * x_1 = 0 → x = 0 → x_1 = 0 → 0 = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
neg : x * x_1 = 0 → x = 0 → ¬x_1 = 0 → 0 = 0 * exp (-x_1.valuation)
pos₁ : x * x_1 = 0 → ¬x = 0 → x_1 = 0 → 0 = exp (-x.valuation) * 0
neg₁ : x * x_1 = 0 → ¬x = 0 → ¬x_1 = 0 → 0 = exp (-x.valuation) * exp (-x_1.valuation)
pos₂ : ¬x * x_1 = 0 → x = 0 → x_1 = 0 → exp (-(x * x_1).valuation) = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
neg₂ : ¬x * x_1 = 0 → x = 0 → ¬x_1 = 0 → exp (-(x * x_1).valuation) = 0 * exp (-x_1.valuation)
⊢ (if x * x_1 = 0 then 0 else exp (-(x * x_1).valuation)) =
    (if x = 0 then 0 else exp (-x.valuation)) * if x_1 = 0 then 0 else exp (-x_1.valuation)
have pos₃ : ¬x * x_1 = 0 → ¬x = 0 → x_1 = 0 → exp (-(x * x_1).valuation) = exp (-x.valuation) * 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
pos : x * x_1 = 0 → x = 0 → x_1 = 0 → 0 = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
neg : x * x_1 = 0 → x = 0 → ¬x_1 = 0 → 0 = 0 * exp (-x_1.valuation)
pos₁ : x * x_1 = 0 → ¬x = 0 → x_1 = 0 → 0 = exp (-x.valuation) * 0
neg₁ : x * x_1 = 0 → ¬x = 0 → ¬x_1 = 0 → 0 = exp (-x.valuation) * exp (-x_1.valuation)
pos₂ : ¬x * x_1 = 0 → x = 0 → x_1 = 0 → exp (-(x * x_1).valuation) = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
neg₂ : ¬x * x_1 = 0 → x = 0 → ¬x_1 = 0 → exp (-(x * x_1).valuation) = 0 * exp (-x_1.valuation)
pos₃ : ¬x * x_1 = 0 → ¬x = 0 → x_1 = 0 → exp (-(x * x_1).valuation) = exp (-x.valuation) * 0
⊢ (if x * x_1 = 0 then 0 else exp (-(x * x_1).valuation)) =
    (if x = 0 then 0 else exp (-x.valuation)) * if x_1 = 0 then 0 else exp (-x_1.valuation)
have neg₃ : ¬x * x_1 = 0 → ¬x = 0 → ¬x_1 = 0 → exp (-(x * x_1).valuation) = exp (-x.valuation) * exp (-x_1.valuation)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
⊢ (if x + x_1 = 0 then 0 else exp (-(x + x_1).valuation)) ≤
    max (if x = 0 then 0 else exp (-x.valuation)) (if x_1 = 0 then 0 else exp (-x_1.valuation))
have pos : x + x_1 = 0 → x = 0 → x_1 = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
pos : x + x_1 = 0 → x = 0 → x_1 = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)
⊢ (if x + x_1 = 0 then 0 else exp (-(x + x_1).valuation)) ≤
    max (if x = 0 then 0 else exp (-x.valuation)) (if x_1 = 0 then 0 else exp (-x_1.valuation))
have neg : x + x_1 = 0 → x = 0 → ¬x_1 = 0 → 0 ≤ max 0 (exp (-x_1.valuation))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
pos : x + x_1 = 0 → x = 0 → x_1 = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)
neg : x + x_1 = 0 → x = 0 → ¬x_1 = 0 → 0 ≤ max 0 (exp (-x_1.valuation))
⊢ (if x + x_1 = 0 then 0 else exp (-(x + x_1).valuation)) ≤
    max (if x = 0 then 0 else exp (-x.valuation)) (if x_1 = 0 then 0 else exp (-x_1.valuation))
have pos₁ : x + x_1 = 0 → ¬x = 0 → x_1 = 0 → 0 ≤ max (exp (-x.valuation)) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
pos : x + x_1 = 0 → x = 0 → x_1 = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)
neg : x + x_1 = 0 → x = 0 → ¬x_1 = 0 → 0 ≤ max 0 (exp (-x_1.valuation))
pos₁ : x + x_1 = 0 → ¬x = 0 → x_1 = 0 → 0 ≤ max (exp (-x.valuation)) 0
⊢ (if x + x_1 = 0 then 0 else exp (-(x + x_1).valuation)) ≤
    max (if x = 0 then 0 else exp (-x.valuation)) (if x_1 = 0 then 0 else exp (-x_1.valuation))
have neg₁ : x + x_1 = 0 → ¬x = 0 → ¬x_1 = 0 → 0 ≤ max (exp (-x.valuation)) (exp (-x_1.valuation))
Tactic: split_ifs