awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrn : r.num ≠ 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
have hqreq : q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
Tactic: have hqreq : q + r = (q.num * r.den + q.den * r.num) /. (q.den * r.den) := Rat.add_num_den _ _
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrn : r.num ≠ 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
hqreq : q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
⊢ padicValRat p q ≤ padicValRat p (q + r)
have hqrd : q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num ≠ 0
Tactic: have hqrd : q.num * r.den + q.den * r.num ≠ 0 := Rat.mk_num_ne_zero_of_ne_zero hqr hqreq
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrn : r.num ≠ 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
hqreq : q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hqrd : q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num ≠ 0
| padicValRat p q
have rw : padicValRat p (q.num /. (↑q.den : ℤ))
Tactic: rw [← q.num_divInt_den]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrn : r.num ≠ 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
hqreq : q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hqrd : q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
have conv_lhs : padicValRat p (q.num /. (↑q.den : ℤ)) ≤ padicValRat p (q + r)
Tactic: conv_lhs => rw [← q.num_divInt_den]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrn : r.num ≠ 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
hqreq : q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hqrd : q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num ≠ 0
⊢ padicValRat p (q.num /. (↑q.den : ℤ)) ≤ padicValRat p (q + r)
have rw : emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤
  emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ) * (↑q.den : ℤ) + (↑q.den : ℤ) * r.num * (↑q.den : ℤ))
Tactic: rw [hqreq, padicValRat_le_padicValRat_iff hqn hqrd hqd (mul_ne_zero hqd hrd), ←
        emultiplicity_le_emultiplicity_iff, mul_left_comm,
        emultiplicity_mul (Nat.prime_iff_prime_int.1 hp.1), add_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrn : r.num ≠ 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
hqreq : q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hqrd : q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num ≠ 0
⊢ emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤
    emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ) * (↑q.den : ℤ) + (↑q.den : ℤ) * r.num * (↑q.den : ℤ))
have h₁ : emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤ emultiplicity (↑p : ℤ) (r.num * (↑q.den : ℤ))
Tactic: rw [← q.num_divInt_den, ← r.num_divInt_den, padicValRat_le_padicValRat_iff hqn hrn hqd hrd, ←
        emultiplicity_le_emultiplicity_iff] at h
Cleared hypotheses: h, hq, hr, hqn, hqd, hrn, hrd, hqreq, hqrd
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤ emultiplicity (↑p : ℤ) (r.num * (↑q.den : ℤ))
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrn : r.num ≠ 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
hqreq : q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hqrd : q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num ≠ 0
⊢ emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤
    emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ) * (↑q.den : ℤ))
have rw : emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤
  emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) + emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)
Tactic: rw [emultiplicity_mul (a := _ * _) (Nat.prime_iff_prime_int.1 hp.1), add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤ emultiplicity (↑p : ℤ) (r.num * (↑q.den : ℤ))
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrn : r.num ≠ 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
hqreq : q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hqrd : q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num ≠ 0
rw :
  emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤
    emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) + emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)
⊢ emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤
    emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ) * (↑q.den : ℤ))
have rw₁ : emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) + emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) ≤
  emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) + emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)
Tactic: rw [emultiplicity_mul (a := _ * _) (Nat.prime_iff_prime_int.1 hp.1), add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤ emultiplicity (↑p : ℤ) (r.num * (↑q.den : ℤ))
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrn : r.num ≠ 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
hqreq : q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hqrd : q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num ≠ 0
⊢ emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤
    emultiplicity (↑p : ℤ) ((↑q.den : ℤ) * r.num * (↑q.den : ℤ))
have grw : emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤
  emultiplicity (↑p : ℤ) ((↑q.den : ℤ) * (r.num * (↑q.den : ℤ)))
Tactic: grw [mul_assoc, emultiplicity_mul (b := _ * _) (Nat.prime_iff_prime_int.1 hp.1), h]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤ emultiplicity (↑p : ℤ) (r.num * (↑q.den : ℤ))
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrn : r.num ≠ 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
hqreq : q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hqrd : q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num ≠ 0
grw :
  emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤
    emultiplicity (↑p : ℤ) ((↑q.den : ℤ) * (r.num * (↑q.den : ℤ)))
⊢ emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤
    emultiplicity (↑p : ℤ) ((↑q.den : ℤ) * r.num * (↑q.den : ℤ))
have grw₁ : emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤
  emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (r.num * (↑q.den : ℤ))
Tactic: grw [mul_assoc, emultiplicity_mul (b := _ * _) (Nat.prime_iff_prime_int.1 hp.1), h]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤ emultiplicity (↑p : ℤ) (r.num * (↑q.den : ℤ))
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrn : r.num ≠ 0
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
hqreq : q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hqrd : q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num ≠ 0
grw :
  emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤
    emultiplicity (↑p : ℤ) ((↑q.den : ℤ) * (r.num * (↑q.den : ℤ)))
grw₁ :
  emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤
    emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (r.num * (↑q.den : ℤ))
⊢ emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤
    emultiplicity (↑p : ℤ) ((↑q.den : ℤ) * r.num * (↑q.den : ℤ))
have grw₂ : emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (r.num * (↑q.den : ℤ)) ≤
  emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (r.num * (↑q.den : ℤ))
Tactic: grw [mul_assoc, emultiplicity_mul (b := _ * _) (Nat.prime_iff_prime_int.1 hp.1), h]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
⊢ min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
have rw : padicValRat p q ≤ padicValRat p (q + r)
Tactic: rw [min_eq_left h]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
have rw : padicValRat p r ≤ padicValRat p (r + q)
Tactic: rw [min_eq_right h, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
⊢ padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
have h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
Tactic: have h1 := min_le_padicValRat_add (p := p) hqr
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
⊢ padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
have h2 : min (padicValRat p (q + r)) (padicValRat p (-r)) ≤ padicValRat p (q + r + -r)
Tactic: have h2 := min_le_padicValRat_add (p := p) (ne_of_eq_of_ne (add_neg_cancel_right q r) hq)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
h2 : min (padicValRat p (q + r)) (padicValRat p (-r)) ≤ padicValRat p (q + r + -r)
⊢ padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
have h3 : min (padicValRat p (r + q)) (padicValRat p (-q)) ≤ padicValRat p (r + q + -q)
Tactic: have h3 := min_le_padicValRat_add (p := p) (ne_of_eq_of_ne (add_neg_cancel_right r q) hr)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
h2 : min (padicValRat p (q + r)) (padicValRat p (-r)) ≤ padicValRat p (q + r + -r)
h3 : min (padicValRat p (r + q)) (padicValRat p (-q)) ≤ padicValRat p (r + q + -q)
⊢ padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
have h2₁ : min (padicValRat p (q + r)) (padicValRat p r) ≤ padicValRat p q
Tactic: rw [add_neg_cancel_right, padicValRat.neg] at h2 h3
Cleared hypotheses: h2, h3
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
h2 : min (padicValRat p (q + r)) (padicValRat p (-r)) ≤ padicValRat p (q + r + -r)
h3 : min (padicValRat p (r + q)) (padicValRat p (-q)) ≤ padicValRat p (r + q + -q)
h2₁ : min (padicValRat p (q + r)) (padicValRat p r) ≤ padicValRat p q
⊢ padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
have h3₁ : min (padicValRat p (r + q)) (padicValRat p q) ≤ padicValRat p r
Tactic: rw [add_neg_cancel_right, padicValRat.neg] at h2 h3
Cleared hypotheses: h2, h3
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q ≠ padicValRat p r
h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
h2 : min (padicValRat p (q + r)) (padicValRat p r) ≤ padicValRat p q
h3 : min (padicValRat p (r + q)) (padicValRat p q) ≤ padicValRat p r
⊢ padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
have h3₁ : min (padicValRat p (q + r)) (padicValRat p q) ≤ padicValRat p r
Tactic: rw [add_comm] at h3
Cleared hypotheses: h3
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q < padicValRat p r
⊢ padicValRat p (q + r) = padicValRat p q
have rw : min (padicValRat p q) (padicValRat p r) = padicValRat p q
Tactic: rw [add_eq_min hqr hq hr (ne_of_lt hval), min_eq_left (le_of_lt hval)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q < padicValRat p r
rw : min (padicValRat p q) (padicValRat p r) = padicValRat p q
⊢ padicValRat p (q + r) = padicValRat p q
have rw₁ : padicValRat p q = padicValRat p q
Tactic: rw [add_eq_min hqr hq hr (ne_of_lt hval), min_eq_left (le_of_lt hval)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
r : ℕ
⊢ padicValRat p (HPow.hPow (α := ℚ) (↑p : ℚ) r)⁻¹ = -(↑r : ℤ)
have rw : -padicValRat p (HPow.hPow (α := ℚ) (↑p : ℚ) r) = -(↑r : ℤ)
Tactic: rw [padicValRat.inv, neg_inj, padicValRat.pow (Nat.cast_ne_zero.mpr hp.elim.ne_zero),
      padicValRat.self hp.elim.one_lt, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
r : ℕ
rw : -padicValRat p (HPow.hPow (α := ℚ) (↑p : ℚ) r) = -(↑r : ℤ)
⊢ padicValRat p (HPow.hPow (α := ℚ) (↑p : ℚ) r)⁻¹ = -(↑r : ℤ)
have rw₁ : padicValRat p (HPow.hPow (α := ℚ) (↑p : ℚ) r) = (↑r : ℤ)
Tactic: rw [padicValRat.inv, neg_inj, padicValRat.pow (Nat.cast_ne_zero.mpr hp.elim.ne_zero),
      padicValRat.self hp.elim.one_lt, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
r : ℕ
rw : -padicValRat p (HPow.hPow (α := ℚ) (↑p : ℚ) r) = -(↑r : ℤ)
rw₁ : padicValRat p (HPow.hPow (α := ℚ) (↑p : ℚ) r) = (↑r : ℤ)
⊢ padicValRat p (HPow.hPow (α := ℚ) (↑p : ℚ) r)⁻¹ = -(↑r : ℤ)
have rw₂ : (↑r : ℤ) * padicValRat p (↑p : ℚ) = (↑r : ℤ)
Tactic: rw [padicValRat.inv, neg_inj, padicValRat.pow (Nat.cast_ne_zero.mpr hp.elim.ne_zero),
      padicValRat.self hp.elim.one_lt, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
r : ℕ
rw : -padicValRat p (HPow.hPow (α := ℚ) (↑p : ℚ) r) = -(↑r : ℤ)
rw₁ : padicValRat p (HPow.hPow (α := ℚ) (↑p : ℚ) r) = (↑r : ℤ)
rw₂ : (↑r : ℤ) * padicValRat p (↑p : ℚ) = (↑r : ℤ)
⊢ padicValRat p (HPow.hPow (α := ℚ) (↑p : ℚ) r)⁻¹ = -(↑r : ℤ)
have rw₃ : HMul.hMul (α := ℤ) (↑r : ℤ) 1 = (↑r : ℤ)
Tactic: rw [padicValRat.inv, neg_inj, padicValRat.pow (Nat.cast_ne_zero.mpr hp.elim.ne_zero),
      padicValRat.self hp.elim.one_lt, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
r : ℕ
rw : -padicValRat p (HPow.hPow (α := ℚ) (↑p : ℚ) r) = -(↑r : ℤ)
rw₁ : padicValRat p (HPow.hPow (α := ℚ) (↑p : ℚ) r) = (↑r : ℤ)
rw₂ : (↑r : ℤ) * padicValRat p (↑p : ℚ) = (↑r : ℤ)
rw₃ : HMul.hMul (α := ℤ) (↑r : ℤ) 1 = (↑r : ℤ)
⊢ padicValRat p (HPow.hPow (α := ℚ) (↑p : ℚ) r)⁻¹ = -(↑r : ℤ)
have rw₄ : Eq (α := ℤ) (↑r : ℤ) (↑r : ℤ)
Tactic: rw [padicValRat.inv, neg_inj, padicValRat.pow (Nat.cast_ne_zero.mpr hp.elim.ne_zero),
      padicValRat.self hp.elim.one_lt, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd :
  ∀ (hF : ∀ i < d, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range d, F i) 0),
    0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range (d + 1), F i) 0
⊢ 0 < padicValRat p (∑ i ∈ Finset.range (d + 1), F i)
have succ : ∀ (hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0), 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)
Tactic: rw [Finset.sum_range_succ] at hn0 ⊢
Cleared hypotheses: hn0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd :
  ∀ (hF : ∀ i < d, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range d, F i) 0),
    0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)
have pos : ∀ (h : Eq (α := ℚ) (∑ x ∈ Finset.range d, F x) 0), 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)
Tactic: by_cases h : ∑ x ∈ Finset.range d, F x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd :
  ∀ (hF : ∀ i < d, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range d, F i) 0),
    0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
pos : ∀ (h : Eq (α := ℚ) (∑ x ∈ Finset.range d, F x) 0), 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)
have neg : ∀ (h : ¬Eq (α := ℚ) (∑ x ∈ Finset.range d, F x) 0), 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)
Tactic: by_cases h : ∑ x ∈ Finset.range d, F x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd :
  ∀ (hF : ∀ i < d, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range d, F i) 0),
    0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : Eq (α := ℚ) (∑ x ∈ Finset.range d, F x) 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)
have pos : 0 < padicValRat p (F d)
Tactic: rw [h, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd :
  ∀ (hF : ∀ i < d, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range d, F i) 0),
    0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬Eq (α := ℚ) (∑ x ∈ Finset.range d, F x) 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)
have neg : 0 < min (padicValRat p (∑ x ∈ Finset.range d, F x)) (padicValRat p (F d))
Tactic: refine lt_of_lt_of_le ?_ (min_le_padicValRat_add hn0)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd :
  ∀ (hF : ∀ i < d, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range d, F i) 0),
    0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬Eq (α := ℚ) (∑ x ∈ Finset.range d, F x) 0
⊢ 0 < min (padicValRat p (∑ x ∈ Finset.range d, F x)) (padicValRat p (F d))
have neg : ∀ (i : ℕ) (hi : i < d), 0 < padicValRat p (F i)
Tactic: refine lt_min (hd (fun i hi => ?_) h) (hF d (lt_add_one _))
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF : ∀ i < n, 0 < padicValRat p (F i)
hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range n, F i) 0
⊢ 0 < padicValRat p (∑ i ∈ Finset.range n, F i)
have zero : ∀ (hF : ∀ i < 0, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range 0, F i) 0),
  0 < padicValRat p (∑ i ∈ Finset.range 0, F i)
Tactic: induction n with
  | zero => exact False.elim (hn0 rfl)
  | succ d hd =>
    rw [Finset.sum_range_succ] at hn0 ⊢
    by_cases h : ∑ x ∈ Finset.range d, F x = 0
    · rw [h, zero_add]
      exact hF d (lt_add_one _)
    · refine lt_of_lt_of_le ?_ (min_le_padicValRat_add hn0)
      refine lt_min (hd (fun i hi => ?_) h) (hF d (lt_add_one _))
      exact hF _ (lt_trans hi (lt_add_one _))
Cleared hypotheses: n, hF, hn0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF : ∀ i < n, 0 < padicValRat p (F i)
hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range n, F i) 0
zero :
  ∀ (hF : ∀ i < 0, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range 0, F i) 0),
    0 < padicValRat p (∑ i ∈ Finset.range 0, F i)
⊢ 0 < padicValRat p (∑ i ∈ Finset.range n, F i)
have succ : ∀ (d : ℕ)
  (hd :
    ∀ (hF : ∀ i < d, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range d, F i) 0),
      0 < padicValRat p (∑ i ∈ Finset.range d, F i))
  (hF : ∀ i < d + 1, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range (d + 1), F i) 0),
  0 < padicValRat p (∑ i ∈ Finset.range (d + 1), F i)
Tactic: induction n with
  | zero => exact False.elim (hn0 rfl)
  | succ d hd =>
    rw [Finset.sum_range_succ] at hn0 ⊢
    by_cases h : ∑ x ∈ Finset.range d, F x = 0
    · rw [h, zero_add]
      exact hF d (lt_add_one _)
    · refine lt_of_lt_of_le ?_ (min_le_padicValRat_add hn0)
      refine lt_min (hd (fun i hi => ?_) h) (hF d (lt_add_one _))
      exact hF _ (lt_trans hi (lt_add_one _))
Cleared hypotheses: n, hF, hn0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
k : ℕ
hF : ∀ (i : ℕ), Membership.mem (γ := Finset ℕ) {k} i → padicValRat p (F j) < padicValRat p (F i)
⊢ padicValRat p (F j) < padicValRat p (∑ i ∈ {k}, F i)
have singleton : padicValRat p (F j) < padicValRat p (F k)
Tactic: rw [Finset.sum_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
s : ℕ
S' : Finset ℕ
Hnot : s ∉ S'
Hne : S'.Nonempty
Hind : ∀ (hF : ∀ i ∈ S', padicValRat p (F j) < padicValRat p (F i)), padicValRat p (F j) < padicValRat p (∑ i ∈ S', F i)
hF : ∀ i ∈ Finset.cons s S' Hnot, padicValRat p (F j) < padicValRat p (F i)
⊢ padicValRat p (F j) < padicValRat p (∑ i ∈ Finset.cons s S' Hnot, F i)
have cons : padicValRat p (F j) < padicValRat p (F s + ∑ x ∈ S', F x)
Tactic: rw [Finset.cons_eq_insert, Finset.sum_insert Hnot]