awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ valuation (p := p) (↑q : ℚ_[p]) = padicValRat p q

Tactic:
neg_injective ((zpow_right_strictMono₀ (mod_cast hp.out.one_lt)).injective
    <| (norm_eq_zpow_neg_valuation (mod_cast hq)).symm.trans ?_)

Premises used: neg_injective, Padic.norm_eq_zpow_neg_valuation, StrictMono.injective, zpow_right_strictMono₀, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
inr : norm (E := ℚ_[p]) (↑q : ℚ_[p]) = HPow.hPow (α := ℝ) (↑p : ℝ) (-padicValRat p q)
⊢ valuation (p := p) (↑q : ℚ_[p]) = padicValRat p q

Tactic:
refine neg_injective ((zpow_right_strictMono₀ (mod_cast hp.out.one_lt)).injective
    <| (norm_eq_zpow_neg_valuation (mod_cast hq)).symm.trans ?_)

Premises used: neg_injective, Padic.norm_eq_zpow_neg_valuation, StrictMono.injective, zpow_right_strictMono₀, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
inr : padicNorm p q = HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)
⊢ norm (E := ℚ_[p]) (↑q : ℚ_[p]) = HPow.hPow (α := ℝ) (↑p : ℝ) (-padicValRat p q)

Tactic:
rw [eq_padicNorm, ← Rat.cast_natCast, ← Rat.cast_zpow, Rat.cast_inj]

Premises used: Padic.eq_padicNorm, Rat.cast_inj, Rat.cast_natCast, Rat.cast_zpow
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)

Tactic:
padicNorm.eq_zpow_of_nonzero hq

Premises used: padicNorm.eq_zpow_of_nonzero
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)

Tactic:
exact padicNorm.eq_zpow_of_nonzero hq

Premises used: padicNorm.eq_zpow_of_nonzero
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
rw : valuation (p := p) (↑(↑n : ℚ) : ℚ_[p]) = (↑(padicValInt p n) : ℤ)
rw₁ : padicValRat p (↑n : ℚ) = (↑(padicValInt p n) : ℤ)
rw₂ rw₃ : Eq (α := ℤ) (↑(padicValInt p n) : ℤ) (↑(padicValInt p n) : ℤ)
⊢ valuation (p := p) (↑n : ℚ_[p]) = (↑(padicValInt p n) : ℤ)

Tactic:
rw [← Rat.cast_intCast, valuation_ratCast, padicValRat.of_int]

Premises used: Rat.cast_intCast, padicValRat.of_int, Padic.valuation_ratCast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : valuation (p := p) (↑(↑n : ℚ) : ℚ_[p]) = (↑(padicValNat p n) : ℤ)
rw₁ : padicValRat p (↑n : ℚ) = (↑(padicValNat p n) : ℤ)
rw₂ rw₃ : Eq (α := ℤ) (↑(padicValNat p n) : ℤ) (↑(padicValNat p n) : ℤ)
⊢ valuation (p := p) (↑n : ℚ_[p]) = (↑(padicValNat p n) : ℤ)

Tactic:
rw [← Rat.cast_natCast, valuation_ratCast, padicValRat.of_nat]

Premises used: Rat.cast_natCast, padicValRat.of_nat, Padic.valuation_ratCast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
inst : n.AtLeastTwo
⊢ valuation (p := p) (OfNat.ofNat n) = (↑(padicValNat p n) : ℤ)

Tactic:
valuation_natCast n

Premises used: Padic.valuation_natCast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : valuation (p := p) (↑1 : ℚ_[p]) = 0
rw₁ : Eq (α := ℤ) (↑(padicValNat p 1) : ℤ) 0
rw₂ : Eq (α := ℤ) (↑0 : ℤ) 0
rw₃ rw₄ : Eq (α := ℤ) 0 0
⊢ valuation (p := p) 1 = 0

Tactic:
rw [← Nat.cast_one, valuation_natCast, padicValNat_one_right, cast_zero]

Premises used: padicValNat_one_right, Nat.cast_zero, Padic.valuation_natCast, Nat.cast_one
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : Eq (α := ℤ) (↑(padicValNat p p) : ℤ) 1
rw₁ : Eq (α := ℤ) (↑1 : ℤ) 1
rw₂ rw₃ : Eq (α := ℤ) 1 1
⊢ valuation (p := p) (↑p : ℚ_[p]) = 1

Tactic:
rw [valuation_natCast, padicValNat_self, cast_one]

Premises used: padicValNat_self, Padic.valuation_natCast, Nat.cast_one
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
pos : ∀ (hx : x = 0), min x.valuation y.valuation ≤ (x + y).valuation
neg : ∀ (hx : ¬x = 0), min x.valuation y.valuation ≤ (x + y).valuation
⊢ min x.valuation y.valuation ≤ (x + y).valuation

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : x = 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation

Tactic:
simpa only [hx, zero_add] using min_le_right _ _

Premises used: zero_add, min_le_right
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
pos : ∀ (hy : y = 0), min x.valuation y.valuation ≤ (x + y).valuation
neg : ∀ (hy : ¬y = 0), min x.valuation y.valuation ≤ (x + y).valuation
⊢ min x.valuation y.valuation ≤ (x + y).valuation

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation

Tactic:
simpa only [hy, add_zero] using min_le_left _ _

Premises used: min_le_left, add_zero
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ ‖x + y‖ ≤ max ‖x‖ ‖y‖

Tactic:
have : ‖x + y‖ ≤ max ‖x‖ ‖y‖ := nonarchimedean x y
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : ‖x + y‖ ≤ max ‖x‖ ‖y‖
⊢ min x.valuation y.valuation ≤ (x + y).valuation

Tactic:
simpa only [norm_eq_zpow_neg_valuation hxy, norm_eq_zpow_neg_valuation hx,
    norm_eq_zpow_neg_valuation hy, le_max_iff,
    zpow_le_zpow_iff_right₀ (mod_cast hp.out.one_lt : 1 < (p : ℝ)), neg_le_neg_iff, ← min_le_iff]

Premises used: Nat.Prime.one_lt, congrArg, Nat.cast_lt._simp_1, min_le_iff, cast, zpow_le_zpow_iff_right₀, Padic.norm_eq_zpow_neg_valuation, Nat.cast, LT.lt, congrFun', Eq.symm, le_max_iff, Nat.cast_one, Fact.out, Eq.trans, neg_le_neg_iff
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x * y‖ = ‖x‖ * ‖y‖

Tactic:
have h_norm : ‖x * y‖ = ‖x‖ * ‖y‖ := norm_mul x y
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
⊢ Ne (α := ℝ) (↑p : ℝ) 1

Tactic:
have hp_ne_one : (p : ℝ) ≠ 1 := mod_cast (Fact.out : p.Prime).ne_one
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
⊢ LT.lt (α := ℝ) 0 (↑p : ℝ)

Tactic:
have hp_pos : (0 : ℝ) < p := mod_cast NeZero.pos _
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
rwa₆ rwa₇ rwa₈ 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

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

Premises used: zpow_right_inj₀, neg_add, Padic.norm_eq_zpow_neg_valuation, LT.lt.ne', zpow_add₀, neg_inj, mul_ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
inl : valuation (p := p) 0⁻¹ = -valuation (p := p) 0
inr : ∀ (hx : x ≠ 0), x⁻¹.valuation = -x.valuation
⊢ x⁻¹.valuation = -x.valuation

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation (p := p) 0⁻¹ = -valuation (p := p) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
⊢ ‖x⁻¹‖ = ‖x‖⁻¹

Tactic:
have h_norm : ‖x⁻¹‖ = ‖x‖⁻¹ := norm_inv x
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
⊢ Ne (α := ℝ) (↑p : ℝ) 1

Tactic:
have hp_ne_one : (p : ℝ) ≠ 1 := mod_cast (Fact.out : p.Prime).ne_one
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
h_norm : ‖x⁻¹‖ = ‖x‖⁻¹
hp_ne_one : Ne (α := ℝ) (↑p : ℝ) 1
⊢ LT.lt (α := ℝ) 0 (↑p : ℝ)

Tactic:
have hp_pos : (0 : ℝ) < p := mod_cast NeZero.pos _
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
inr₄ inr₅ inr₆ 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

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

Premises used: zpow_right_inj₀, Padic.norm_eq_zpow_neg_valuation, zpow_neg, neg_inj, inv_ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ (HPow.hPow (β := ℕ) x 0).valuation = (↑0 : ℤ) * x.valuation

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
inl : (HPow.hPow (α := ℚ_[p]) 0 (n + 1)).valuation = (↑(n + 1) : ℤ) * valuation (p := p) 0
inr : ∀ (hx : x ≠ 0), (x ^ (n + 1)).valuation = (↑(n + 1) : ℤ) * x.valuation
⊢ (x ^ (n + 1)).valuation = (↑(n + 1) : ℤ) * x.valuation

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (HPow.hPow (α := ℚ_[p]) 0 (n + 1)).valuation = (↑(n + 1) : ℤ) * valuation (p := p) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
hx : x ≠ 0
⊢ (x ^ (n + 1)).valuation = (↑(n + 1) : ℤ) * x.valuation

Tactic:
simp [pow_succ, hx, valuation_mul, valuation_pow, _root_.add_one_mul]

Premises used: pow_succ, Padic.valuation_mul, add_one_mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
⊢ (HPow.hPow (β := ℤ) x (↑n : ℤ)).valuation = (↑n : ℤ) * x.valuation

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
simp : HAdd.hAdd (α := ℤ) (-1) (-(↑n : ℤ)) = Int.negSucc n ∨ x.valuation = 0
⊢ (x ^ Int.negSucc n).valuation = Int.negSucc n * x.valuation

Tactic:
simp [← neg_mul]

Premises used: neg_mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
⊢ HAdd.hAdd (α := ℤ) (-1) (-(↑n : ℤ)) = Int.negSucc n ∨ x.valuation = 0

Tactic:
simp [Int.negSucc_eq]

Premises used: Int.negSucc_eq
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : (if Eq (α := ℚ_[p]) 0 0 then ⊤ else (↑(valuation (p := p) 0) : WithTop ℤ)) = ⊤
rw₁ rw₂ : Eq (α := WithTop ℤ) ⊤ ⊤
⊢ addValuationDef (p := p) 0 = ⊤

Tactic:
rw [addValuationDef, if_pos rfl]

Premises used: Padic.addValuationDef, if_pos, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
rw₃ rw₄ : Eq (α := WithTop ℤ) 0 0
⊢ addValuationDef (p := p) 1 = 0

Tactic:
rw [addValuationDef, if_neg one_ne_zero, valuation_one, WithTop.coe_zero]

Premises used: Padic.addValuationDef, Padic.valuation_one, WithTop.coe_zero, one_ne_zero, if_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 ℤ)
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 ℤ)
⊢ (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
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 ℤ)
pos₄ pos₅ : Eq (α := 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 ℤ)

Tactic:
rw [hx, if_pos rfl, zero_mul, if_pos rfl, WithTop.top_add]

Premises used: MulZeroClass.zero_mul, if_pos, WithTop.top_add, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 ℤ)
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 ℤ)
⊢ (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
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 ℤ)) + ⊤
pos₄ pos₅ : Eq (α := 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 ℤ)

Tactic:
rw [hy, if_pos rfl, mul_zero, if_pos rfl, WithTop.add_top]

Premises used: WithTop.add_top, if_pos, MulZeroClass.mul_zero, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
neg₅ neg₆ : x.valuation + 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 ℤ)

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]

Premises used: Padic.valuation_mul, WithTop.coe_eq_coe, mul_ne_zero, WithTop.coe_add, if_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 ℤ)
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 ℤ)
⊢ 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
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y = 0
pos : min (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) (if y = 0 then ⊤ else (↑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 ℤ)

Tactic:
rw [hxy, if_pos rfl]

Premises used: if_pos, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 ℤ)) ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 ℤ)) ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 ℤ)
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 ℤ)
⊢ 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
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
pos : (if y = 0 then ⊤ else (↑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 ℤ)

Tactic:
rw [hx, if_pos rfl, min_eq_right, zero_add]

Premises used: if_pos, zero_add, min_eq_right, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ (if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)) ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ (if y = 0 then ⊤ else (↑y.valuation : WithTop ℤ)) ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 ℤ)
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 ℤ)
⊢ 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
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : y = 0
pos : (if x = 0 then ⊤ else (↑x.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 ℤ)

Tactic:
rw [hy, if_pos rfl, min_eq_left, add_zero]

Premises used: if_pos, min_eq_left, add_zero, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ (if x = 0 then ⊤ else (↑x.valuation : WithTop ℤ)) ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
neg : min x.valuation y.valuation ≤ (x + y).valuation
⊢ 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:
rw [if_neg hx, if_neg hy, if_neg hxy, ← WithTop.coe_min, WithTop.coe_le_coe]

Premises used: WithTop.coe_le_coe, WithTop.coe_min, if_neg