awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : (↑n : ℤ) = -x.valuation
a : ℚ_[p] := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha : a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := by
          intro h0
          rw [h0, norm_zero] at hx
          exact hx zero_le_one
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx_1 : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : (↑n : ℤ) = -x.valuation
a : ℚ_[p] := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha : a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
hx : x ≠ 0
rw : Ne (α := ℝ) (↑p : ℝ) 0 ∨ -x.valuation + -(↑n : ℤ) ≠ 0 ∨ -x.valuation = 0 ∧ Eq (α := ℤ) (-(↑n : ℤ)) 0
⊢ ‖a‖ = 1

Tactic:
rw [ha, padicNormE.mul, Padic.norm_p_pow, Padic.norm_eq_zpow_neg_valuation hx,
          ← zpow_add', hn_coe, neg_neg, neg_add_cancel, zpow_zero]

Premises used: zpow_zero, Padic.norm_p_pow, zpow_add', neg_neg, Padic.norm_eq_zpow_neg_valuation, neg_add_cancel, Padic.padicNormE.mul
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx_1 : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : (↑n : ℤ) = -x.valuation
a : ℚ_[p] := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha : a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
hx : x ≠ 0
⊢ Ne (α := ℝ) (↑p : ℝ) 0 ∨ -x.valuation + -(↑n : ℤ) ≠ 0 ∨ -x.valuation = 0 ∧ Eq (α := ℤ) (-(↑n : ℤ)) 0

Tactic:
Or.inl (Nat.cast_ne_zero.mpr (NeZero.ne p))

Premises used: Iff.mpr, Or.inl, Nat.cast_ne_zero, NeZero.ne
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx_1 : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : (↑n : ℤ) = -x.valuation
a : ℚ_[p] := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha : a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
hx : x ≠ 0
⊢ Ne (α := ℝ) (↑p : ℝ) 0 ∨ -x.valuation + -(↑n : ℤ) ≠ 0 ∨ -x.valuation = 0 ∧ Eq (α := ℤ) (-(↑n : ℤ)) 0

Tactic:
exact Or.inl (Nat.cast_ne_zero.mpr (NeZero.ne p))

Premises used: Iff.mpr, Or.inl, Nat.cast_ne_zero, NeZero.ne
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : (↑n : ℤ) = -x.valuation
a : ℚ_[p] := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha : a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
⊢ ‖a‖ = 1

Tactic:
have ha_norm : ‖a‖ = 1 := by
        have hx : x ≠ 0 := by
          intro h0
          rw [h0, norm_zero] at hx
          exact hx zero_le_one
        rw [ha, padicNormE.mul, Padic.norm_p_pow, Padic.norm_eq_zpow_neg_valuation hx,
          ← zpow_add', hn_coe, neg_neg, neg_add_cancel, zpow_zero]
        exact Or.inl (Nat.cast_ne_zero.mpr (NeZero.ne p))
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : (↑n : ℤ) = -x.valuation
a : ℚ_[p] := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha : a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha_norm : ‖a‖ = 1
h :
  HMul.hMul (β := ℚ_[p]) x
      ((algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p])
          (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) a ⋯,
                  Subtype.mk (p := fun (x : ℤ_[p]) ↦ Membership.mem (γ := Submonoid ℤ_[p]) (nonZeroDivisors ℤ_[p]) x)
                    (HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n) ⋯).2 :
            ℤ_[p]) :
        ℚ_[p]) =
    (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p])
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) a ⋯,
          Subtype.mk (p := fun (x : ℤ_[p]) ↦ Membership.mem (γ := Submonoid ℤ_[p]) (nonZeroDivisors ℤ_[p]) x)
            (HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n) ⋯).1
⊢ ∃ (x_2 : ℤ_[p] × ↥(nonZeroDivisors ℤ_[p])),
    HMul.hMul (β := ℚ_[p]) x ((algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) (↑x_2.2 : ℤ_[p]) : ℚ_[p]) =
      (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) x_2.1

Tactic:
use
        (⟨a, le_of_eq ha_norm⟩,
          ⟨(p ^ n : ℤ_[p]), mem_nonZeroDivisors_iff_ne_zero.mpr (NeZero.ne _)⟩)

Premises used: Prod.mk
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : (↑n : ℤ) = -x.valuation
a : ℚ_[p] := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha : a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha_norm : ‖a‖ = 1
⊢ HMul.hMul (β := ℚ_[p]) x
      ((algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p])
          (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) a ⋯,
                  Subtype.mk (p := fun (x : ℤ_[p]) ↦ Membership.mem (γ := Submonoid ℤ_[p]) (nonZeroDivisors ℤ_[p]) x)
                    (HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n) ⋯).2 :
            ℤ_[p]) :
        ℚ_[p]) =
    (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p])
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) a ⋯,
          Subtype.mk (p := fun (x : ℤ_[p]) ↦ Membership.mem (γ := Submonoid ℤ_[p]) (nonZeroDivisors ℤ_[p]) x)
            (HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n) ⋯).1

Tactic:
simp only [a, map_pow, map_natCast, algebraMap_apply]

Premises used: PadicInt.algebraMap_apply, map_pow, map_natCast
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
simp_rw : ∀ {x y : ℤ_[p]}, x = y → ∃ (c : ↥(nonZeroDivisors ℤ_[p])), (↑c : ℤ_[p]) * x = (↑c : ℤ_[p]) * y
⊢ ∀ {x y : ℤ_[p]},
    Eq (α := ℚ_[p]) ((algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) x : ℚ_[p])
        ((algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) y : ℚ_[p]) →
      ∃ (c : ↥(nonZeroDivisors ℤ_[p])), (↑c : ℤ_[p]) * x = (↑c : ℤ_[p]) * y

Tactic:
simp_rw [algebraMap_apply, Subtype.coe_inj]

Premises used: PadicInt.algebraMap_apply, Subtype.coe_inj
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y x_1 y_1 : ℤ_[p]
h : x_1 = y_1
rw rw₁ : (↑1 : ℤ_[p]) * y_1 = (↑1 : ℤ_[p]) * y_1
⊢ (↑1 : ℤ_[p]) * x_1 = (↑1 : ℤ_[p]) * y_1

Tactic:
rw [h]
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ ∀ {x y : ℤ_[p]}, x = y → ∃ (c : ↥(nonZeroDivisors ℤ_[p])), (↑c : ℤ_[p]) * x = (↑c : ℤ_[p]) * y

Tactic:
exact fun h => ⟨1, by rw [h]⟩
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)

Tactic:
simp [hq, padicNorm]

Premises used: padicNorm
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
q : ℚ
hq : q = 0
⊢ 0 ≤ padicNorm p q

Tactic:
simp [hq, padicNorm]

Premises used: padicNorm
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
q : ℚ
hq : ¬q = 0
split_ifs : 0 ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)
⊢ 0 ≤ if q = 0 then 0 else HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
q : ℚ
hq : ¬q = 0
ha : LE.le (α := ℚ) 0 (↑p : ℚ)
⊢ 0 ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)

Tactic:
apply zpow_nonneg

Premises used: zpow_nonneg
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ LE.le (α := ℚ) 0 (↑p : ℚ)

Tactic:
mod_cast Nat.zero_le _

Premises used: Nat.zero_le, congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, congrFun', Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ LE.le (α := ℚ) 0 (↑p : ℚ)

Tactic:
exact mod_cast Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
⊢ padicNorm p 0 = 0

Tactic:
simp [padicNorm]

Premises used: padicNorm
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
⊢ padicNorm p 1 = 1

Tactic:
simp [padicNorm]

Premises used: padicNorm
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : 1 < p
⊢ padicNorm p (↑p : ℚ) = (↑p : ℚ)⁻¹

Tactic:
simp [padicNorm, (pos_of_gt hp).ne', padicValNat.self hp]

Premises used: pos_of_gt, padicValNat.self, LT.lt.ne', padicNorm
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ padicNorm p (↑p : ℚ) = (↑p : ℚ)⁻¹

Tactic:
padicNorm_p <| Nat.Prime.one_lt Fact.out

Premises used: Nat.Prime.one_lt, padicNorm.padicNorm_p, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p q : ℕ
p_prime : Fact (Nat.Prime p)
q_prime : Fact (Nat.Prime q)
ne : p ≠ q
⊢ padicValRat p (↑q : ℚ) = 0

Tactic:
have p : padicValRat p q = 0 := mod_cast padicValNat_primes ne
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p_1 q : ℕ
p_prime : Fact (Nat.Prime p_1)
q_prime : Fact (Nat.Prime q)
ne : p_1 ≠ q
p : padicValRat p_1 (↑q : ℚ) = 0
rw : (if Eq (α := ℚ) (↑q : ℚ) 0 then 0 else HPow.hPow (α := ℚ) (β := ℤ) (↑p_1 : ℚ) (-0)) = 1
⊢ padicNorm p_1 (↑q : ℚ) = 1

Tactic:
rw [padicNorm, p]

Premises used: padicNorm
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p_1 q : ℕ
p_prime : Fact (Nat.Prime p_1)
q_prime : Fact (Nat.Prime q)
ne : p_1 ≠ q
p : padicValRat p_1 (↑q : ℚ) = 0
⊢ (if Eq (α := ℚ) (↑q : ℚ) 0 then 0 else HPow.hPow (α := ℚ) (β := ℤ) (↑p_1 : ℚ) (-0)) = 1

Tactic:
simp [q_prime.1.ne_zero]

Premises used: Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : 1 < p
rw : LE.le (α := ℚ) (↑p : ℚ) 0 ∨ LT.lt (α := ℚ) 1 (↑p : ℚ)
⊢ padicNorm p (↑p : ℚ) < 1

Tactic:
rw [padicNorm_p hp, inv_lt_one_iff₀]

Premises used: padicNorm.padicNorm_p, inv_lt_one_iff₀
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : 1 < p
⊢ LE.le (α := ℚ) (↑p : ℚ) 0 ∨ LT.lt (α := ℚ) 1 (↑p : ℚ)

Tactic:
mod_cast Or.inr hp

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, congr, LT.lt, congrFun', Or, Nat.cast_zero, Eq.symm, Nat.cast_one, Or.inr, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : 1 < p
⊢ LE.le (α := ℚ) (↑p : ℚ) 0 ∨ LT.lt (α := ℚ) 1 (↑p : ℚ)

Tactic:
exact mod_cast Or.inr hp

Premises used: Or.inr
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ padicNorm p (↑p : ℚ) < 1

Tactic:
padicNorm_p_lt_one <| Nat.Prime.one_lt Fact.out

Premises used: Nat.Prime.one_lt, padicNorm.padicNorm_p_lt_one, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)

Tactic:
simp [padicNorm, hq]

Premises used: padicNorm
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
q : ℚ
hq : q = 0
⊢ padicNorm p (-q) = padicNorm p q

Tactic:
simp [hq]
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ padicNorm p (-q) = padicNorm p q

Tactic:
simp [padicNorm, hq]

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

Tactic:
rw [padicNorm.eq_zpow_of_nonzero hq]

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

Tactic:
apply zpow_ne_zero

Premises used: zpow_ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ Ne (α := ℚ) (↑p : ℚ) 0

Tactic:
mod_cast ne_of_gt hp.1.pos

Premises used: congrArg, cast, ne_of_gt, Nat.Prime.pos, Ne, Nat.cast, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Fact.out, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ Ne (α := ℚ) (↑p : ℚ) 0

Tactic:
exact mod_cast ne_of_gt hp.1.pos

Premises used: ne_of_gt, Nat.Prime.pos, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : padicNorm p q = 0
a : ¬q = 0 → False
⊢ q = 0

Tactic:
apply by_contradiction

Premises used: by_contradiction
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : (if q = 0 then 0 else HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)) = 0
hq : ¬q = 0
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q) = 0

Tactic:
rw [if_neg hq] at h

Premises used: if_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : (if q = 0 then 0 else HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)) = 0
hq : ¬q = 0
h₁ : HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q) = 0
⊢ ¬q = 0

Tactic:
rw [if_neg hq] at h

Premises used: if_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q) = 0
hq : ¬q = 0
a : ¬HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q) = 0
⊢ False

Tactic:
apply absurd h

Premises used: absurd
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q) = 0
hq : ¬q = 0
a : Ne (α := ℚ) (↑p : ℚ) 0
⊢ ¬HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q) = 0

Tactic:
apply zpow_ne_zero

Premises used: zpow_ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q) = 0
hq : ¬q = 0
⊢ Ne (α := ℚ) (↑p : ℚ) 0

Tactic:
mod_cast hp.1.ne_zero

Premises used: congrArg, cast, Ne, Nat.cast, Nat.Prime.ne_zero, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Fact.out, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q) = 0
hq : ¬q = 0
⊢ Ne (α := ℚ) (↑p : ℚ) 0

Tactic:
exact mod_cast hp.1.ne_zero

Premises used: Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r

Tactic:
simp [hq]
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : r = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r

Tactic:
simp [hr]
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
⊢ Ne (α := ℚ) (↑p : ℚ) 0

Tactic:
simp [hp.1.ne_zero]

Premises used: Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
⊢ Ne (α := ℚ) (↑p : ℚ) 0

Tactic:
have : (p : ℚ) ≠ 0 := by simp [hp.1.ne_zero]
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
this : Ne (α := ℚ) (↑p : ℚ) 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r

Tactic:
simp [padicNorm, *, padicValRat.mul, zpow_add₀ this, mul_comm]

Premises used: zpow_add₀, mul_comm, padicNorm, padicValRat.mul
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hr : r = 0
⊢ padicNorm p (q / r) = padicNorm p q / padicNorm p r

Tactic:
simp [hr]
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hr : ¬r = 0
rw : padicNorm p (q / r * r) = padicNorm p q
rw₁ rw₂ : padicNorm p q = padicNorm p q
⊢ padicNorm p (q / r) * padicNorm p r = padicNorm p q

Tactic:
rw [← padicNorm.mul, div_mul_cancel₀ _ hr]

Premises used: div_mul_cancel₀, padicNorm.mul
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
inl : padicNorm p (↑0 : ℚ) ≤ 1
inr : ∀ (hz : z ≠ 0), padicNorm p (↑z : ℚ) ≤ 1
⊢ padicNorm p (↑z : ℚ) ≤ 1

Tactic:
obtain rfl | hz := eq_or_ne z 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ padicNorm p (↑0 : ℚ) ≤ 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
inr : HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑z : ℚ)) ≤ 1
⊢ padicNorm p (↑z : ℚ) ≤ 1

Tactic:
rw [padicNorm, if_neg (mod_cast hz)]

Premises used: padicNorm, if_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ -padicValRat p (↑z : ℚ) ≤ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (↑z : ℚ)) ≤ 1

Tactic:
exact zpow_le_one_of_nonpos₀ (mod_cast hp.1.one_le) (by simp)

Premises used: zpow_le_one_of_nonpos₀
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : q = 0
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
simp [hq, max_eq_right hnrp]

Premises used: max_eq_right
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : r = 0
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
simp [hr, max_eq_left hnqp]

Premises used: max_eq_left
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : q + r = 0
⊢ padicNorm p (q + r) ≤ padicNorm p q

Tactic:
simpa [hqr] using hnqp
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
split_ifs :
  HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤
    max (HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)) (HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p r))
⊢ (if q + r = 0 then 0 else HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r))) ≤
    max (if q = 0 then 0 else HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q))
      (if r = 0 then 0 else HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p r))

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
apply :
  HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q) ∨
    HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p r)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤
    max (HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)) (HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p r))

Tactic:
apply le_max_iff.2

Premises used: Iff.mpr, le_max_iff
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
h₁ : HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q) ∨
    HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p r)

Tactic:
left
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
h₁ : LE.le (α := ℚ) 1 (↑p : ℚ)
h₂ : -padicValRat p (q + r) ≤ -padicValRat p q
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p (q + r)) ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (-padicValRat p q)

Tactic:
apply zpow_le_zpow_right₀

Premises used: zpow_le_zpow_right₀
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ LE.le (α := ℚ) 1 (↑p : ℚ)

Tactic:
mod_cast le_of_lt hp.1.one_lt

Premises used: Nat.Prime.one_lt, congrArg, le_of_lt, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, congrFun', Eq.symm, Nat.cast_one, Fact.out, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ LE.le (α := ℚ) 1 (↑p : ℚ)

Tactic:
exact mod_cast le_of_lt hp.1.one_lt

Premises used: Nat.Prime.one_lt, le_of_lt, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
h₁ : padicValRat p q ≤ padicValRat p (q + r)
⊢ -padicValRat p (q + r) ≤ -padicValRat p q

Tactic:
apply neg_le_neg

Premises used: neg_le_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ padicValRat p q = min (padicValRat p q) (padicValRat p r)

Tactic:
have : padicValRat p q = min (padicValRat p q) (padicValRat p r) := (min_eq_left h).symm
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
this : padicValRat p q = min (padicValRat p q) (padicValRat p r)
h₁ : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
⊢ padicValRat p q ≤ padicValRat p (q + r)

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
this : padicValRat p q = min (padicValRat p q) (padicValRat p r)
⊢ min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)

Tactic:
min_le_padicValRat_add hqr

Premises used: padicValRat.min_le_padicValRat_add
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
this : padicValRat p q = min (padicValRat p q) (padicValRat p r)
⊢ min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)

Tactic:
exact min_le_padicValRat_add hqr

Premises used: padicValRat.min_le_padicValRat_add
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
inr :
  ∀
    (this :
      ∀ {q r : ℚ} (hle : padicValRat p q ≤ padicValRat p r), padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r))
    (hle : ¬padicValRat p q ≤ padicValRat p r), padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
wlog : ∀ {q r : ℚ} (hle : padicValRat p q ≤ padicValRat p r), padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
wlog hle : padicValRat p q ≤ padicValRat p r generalizing q r

Premises used: padicValRat
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ} (hle : padicValRat p q ≤ padicValRat p r), padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
inr : padicNorm p (r + q) ≤ max (padicNorm p r) (padicNorm p q)
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
rw [add_comm, max_comm]

Premises used: add_comm, max_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNorm
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ} (hle : padicValRat p q ≤ padicValRat p r), padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (r + q) ≤ max (padicNorm p r) (padicNorm p q)

Tactic:
this (le_of_not_ge hle)

Premises used: le_of_not_ge