awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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.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

Premises used: padicValRat.padicValRat_le_padicValRat_iff, Rat.num_divInt_den, emultiplicity_le_emultiplicity_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
h₁ : emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤ emultiplicity (↑p : ℤ) (r.num * (↑q.den : ℤ))
⊢ ¬q = 0

Tactic:
rw [← q.num_divInt_den, ← r.num_divInt_den, padicValRat_le_padicValRat_iff hqn hrn hqd hrd, ←
        emultiplicity_le_emultiplicity_iff] at h

Premises used: padicValRat.padicValRat_le_padicValRat_iff, Rat.num_divInt_den, emultiplicity_le_emultiplicity_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
h₁ : emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤ emultiplicity (↑p : ℤ) (r.num * (↑q.den : ℤ))
hq₁ : ¬q = 0
⊢ ¬r = 0

Tactic:
rw [← q.num_divInt_den, ← r.num_divInt_den, padicValRat_le_padicValRat_iff hqn hrn hqd hrd, ←
        emultiplicity_le_emultiplicity_iff] at h

Premises used: padicValRat.padicValRat_le_padicValRat_iff, Rat.num_divInt_den, emultiplicity_le_emultiplicity_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
h₁ : emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤ emultiplicity (↑p : ℤ) (r.num * (↑q.den : ℤ))
hq₁ : ¬q = 0
hr₁ : ¬r = 0
⊢ q.num ≠ 0

Tactic:
rw [← q.num_divInt_den, ← r.num_divInt_den, padicValRat_le_padicValRat_iff hqn hrn hqd hrd, ←
        emultiplicity_le_emultiplicity_iff] at h

Premises used: padicValRat.padicValRat_le_padicValRat_iff, Rat.num_divInt_den, emultiplicity_le_emultiplicity_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
h₁ : emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤ emultiplicity (↑p : ℤ) (r.num * (↑q.den : ℤ))
hq₁ : ¬q = 0
hr₁ : ¬r = 0
hqn₁ : q.num ≠ 0
⊢ Ne (α := ℤ) (↑q.den : ℤ) 0

Tactic:
rw [← q.num_divInt_den, ← r.num_divInt_den, padicValRat_le_padicValRat_iff hqn hrn hqd hrd, ←
        emultiplicity_le_emultiplicity_iff] at h

Premises used: padicValRat.padicValRat_le_padicValRat_iff, Rat.num_divInt_den, emultiplicity_le_emultiplicity_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
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
⊢ r.num ≠ 0

Tactic:
rw [← q.num_divInt_den, ← r.num_divInt_den, padicValRat_le_padicValRat_iff hqn hrn hqd hrd, ←
        emultiplicity_le_emultiplicity_iff] at h

Premises used: padicValRat.padicValRat_le_padicValRat_iff, Rat.num_divInt_den, emultiplicity_le_emultiplicity_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
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
⊢ Ne (α := ℤ) (↑r.den : ℤ) 0

Tactic:
rw [← q.num_divInt_den, ← r.num_divInt_den, padicValRat_le_padicValRat_iff hqn hrn hqd hrd, ←
        emultiplicity_le_emultiplicity_iff] at h

Premises used: padicValRat.padicValRat_le_padicValRat_iff, Rat.num_divInt_den, emultiplicity_le_emultiplicity_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
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
⊢ q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.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

Premises used: padicValRat.padicValRat_le_padicValRat_iff, Rat.num_divInt_den, emultiplicity_le_emultiplicity_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
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 : ℤ)
⊢ q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num ≠ 0

Tactic:
rw [← q.num_divInt_den, ← r.num_divInt_den, padicValRat_le_padicValRat_iff hqn hrn hqd hrd, ←
        emultiplicity_le_emultiplicity_iff] at h

Premises used: padicValRat.padicValRat_le_padicValRat_iff, Rat.num_divInt_den, emultiplicity_le_emultiplicity_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 : ℤ)
rw₁ rw₂ :
  emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) + emultiplicity (α := ℤ) (↑p : ℤ) (↑q.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 : ℤ))

Tactic:
rw [emultiplicity_mul (a := _ * _) (Nat.prime_iff_prime_int.1 hp.1), add_comm]

Premises used: Nat.prime_iff_prime_int, add_comm, Iff.mp, Fact.out, emultiplicity_mul
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 : ℤ))
grw₂ grw₃ :
  emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (r.num * (↑q.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 : ℤ))

Tactic:
grw [mul_assoc, emultiplicity_mul (b := _ * _) (Nat.prime_iff_prime_int.1 hp.1), h]

Premises used: Nat.prime_iff_prime_int, mul_assoc, Iff.mp, Fact.out, emultiplicity_mul
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
⊢ min (emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ) * (↑q.den : ℤ)))
      (emultiplicity (↑p : ℤ) ((↑q.den : ℤ) * r.num * (↑q.den : ℤ))) ≤
    emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ) * (↑q.den : ℤ) + (↑q.den : ℤ) * r.num * (↑q.den : ℤ))

Tactic:
min_le_emultiplicity_add

Premises used: min_le_emultiplicity_add
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 : ℤ) + (↑q.den : ℤ) * r.num * (↑q.den : ℤ))

Tactic:
calc
        _ ≤ min (emultiplicity ↑p (q.num * r.den * q.den))
                (emultiplicity ↑p (q.den * r.num * q.den)) :=
          le_min
            (by rw [emultiplicity_mul (a := _ * _) (Nat.prime_iff_prime_int.1 hp.1), add_comm])
            (by grw [mul_assoc, emultiplicity_mul (b := _ * _) (Nat.prime_iff_prime_int.1 hp.1), h])
        _ ≤ _ := min_le_emultiplicity_add

Premises used: Rat.num, HMul.hMul, Rat.den, Nat.cast, le_min, min_le_emultiplicity_add, Min.min, emultiplicity
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
rw : padicValRat p q ≤ padicValRat p (q + r)
⊢ min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)

Tactic:
rw [min_eq_left h]

Premises used: min_eq_left
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
⊢ padicValRat p q ≤ padicValRat p (q + r)

Tactic:
le_padicValRat_add_of_le hqr h

Premises used: padicValRat.le_padicValRat_add_of_le
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
⊢ padicValRat p q ≤ padicValRat p (q + r)

Tactic:
exact le_padicValRat_add_of_le hqr h

Premises used: padicValRat.le_padicValRat_add_of_le
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
rw : padicValRat p r ≤ padicValRat p (r + q)
⊢ min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)

Tactic:
rw [min_eq_right h, add_comm]

Premises used: add_comm, min_eq_right
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
rwa rwa₁ rwa₂ rwa₃ : q + r ≠ 0
⊢ r + q ≠ 0

Tactic:
rwa [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ padicValRat p r ≤ padicValRat p (r + q)

Tactic:
exact le_padicValRat_add_of_le (by rwa [add_comm]) h

Premises used: padicValRat.le_padicValRat_add_of_le
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
⊢ min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)

Tactic:
have h1 := min_le_padicValRat_add (p := p) hqr
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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)
⊢ 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)
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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)
⊢ 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)
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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)
⊢ min (padicValRat p (q + r)) (padicValRat p r) ≤ padicValRat p q

Tactic:
rw [add_neg_cancel_right, padicValRat.neg] at h2 h3

Premises used: padicValRat.neg, add_neg_cancel_right
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
⊢ min (padicValRat p (r + q)) (padicValRat p q) ≤ padicValRat p r

Tactic:
rw [add_neg_cancel_right, padicValRat.neg] at h2 h3

Premises used: padicValRat.neg, add_neg_cancel_right
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
⊢ min (padicValRat p (q + r)) (padicValRat p q) ≤ padicValRat p r

Tactic:
rw [add_comm] at h3

Premises used: add_comm
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 (q + r)) (padicValRat p q) ≤ padicValRat p r
⊢ padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)

Tactic:
omega
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
rw₁ rw₂ : padicValRat p q = padicValRat p q
⊢ padicValRat p (q + r) = padicValRat p q

Tactic:
rw [add_eq_min hqr hq hr (ne_of_lt hval), min_eq_left (le_of_lt hval)]

Premises used: le_of_lt, min_eq_left, padicValRat.add_eq_min, ne_of_lt
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r₁ r₂ : ℚ
hqr : r₁ + r₂ ≠ 0
hval₁ : padicValRat p q < padicValRat p r₁
hval₂ : padicValRat p q < padicValRat p r₂
⊢ padicValRat p q < padicValRat p (r₁ + r₂)

Tactic:
lt_of_lt_of_le (lt_min hval₁ hval₂) (padicValRat.min_le_padicValRat_add hqr)

Premises used: padicValRat.min_le_padicValRat_add, lt_min, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 : ℤ)
rw₄ rw₅ : Eq (α := ℤ) (↑r : ℤ) (↑r : ℤ)
⊢ 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]

Premises used: Iff.mpr, Nat.Prime.one_lt, Fact.elim, Nat.Prime.ne_zero, neg_inj, padicValRat.inv, padicValRat.pow, mul_one, Nat.cast_ne_zero, padicValRat.self
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
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:
False.elim (hn0 rfl)

Premises used: False.elim, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
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:
exact False.elim (hn0 rfl)

Premises used: False.elim, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
succ : ∀ (hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0), 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)
⊢ 0 < padicValRat p (∑ i ∈ Finset.range (d + 1), F i)

Tactic:
rw [Finset.sum_range_succ] at hn0 ⊢

Premises used: Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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)
neg : ∀ (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)

Tactic:
by_cases h : ∑ x ∈ Finset.range d, F x = 0

Premises used: Finset.range
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
pos : 0 < padicValRat p (F d)
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)

Tactic:
rw [h, zero_add]

Premises used: zero_add
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 (F d)

Tactic:
hF d (lt_add_one _)

Premises used: lt_add_one
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 (F d)

Tactic:
exact hF d (lt_add_one _)

Premises used: lt_add_one
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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)

Tactic:
lt_of_lt_of_le ?_ (min_le_padicValRat_add hn0)

Premises used: padicValRat.min_le_padicValRat_add, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
neg : 0 < min (padicValRat p (∑ x ∈ Finset.range d, F x)) (padicValRat p (F d))
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)

Tactic:
refine lt_of_lt_of_le ?_ (min_le_padicValRat_add hn0)

Premises used: padicValRat.min_le_padicValRat_add, lt_of_lt_of_le