-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_rat_le_one : ∀ {q : ℚ} (_ : ¬p ∣ q.den), ‖(q : ℚ_[p])‖ ≤ 1
  | ⟨n, d, hn, hd⟩ => fun hq : ¬p ∣ d ↦
    if hnz : n = 0 then by
      have : (⟨n, d, hn, hd⟩ : ℚ) = 0 := Rat.zero_iff_num_zero.mpr hnz
      norm_num [this]
    else by
      have hnz' : (⟨n, d, hn, hd⟩ : ℚ) ≠ 0 := mt Rat.zero_iff_num_zero.1 hnz
      rw [padicNormE.eq_padicNorm]
      norm_cast
      -- Porting note: `Nat.cast_zero` instead of another `norm_cast` call
      rw [padicNorm.eq_zpow_of_nonzero hnz', padicValRat, neg_sub,
        padicValNat.eq_zero_of_not_dvd hq, Nat.cast_zero, zero_sub, zpow_neg, zpow_natCast]
      apply inv_le_one_of_one_le₀
      norm_cast
      apply one_le_pow
      exact hp.1.pos

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
⊢ ‖↑{ num := n, den := d, den_nz := hn, reduced := hd }‖ ≤ 1

Tactic:
have hnz' : (⟨n, d, hn, hd⟩ : ℚ) ≠ 0 := mt Rat.zero_iff_num_zero.1 hnz

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ ‖↑{ num := n, den := d, den_nz := hn, reduced := hd }‖ ≤ 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ (↑p ^ padicValInt p { num := n, den := d, den_nz := hn, reduced := hd }.num)⁻¹ ≤ 1

Tactic:
apply inv_le_one_of_one_le₀

Result:
case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ 1 ≤ ↑p ^ padicValInt p { num := n, den := d, den_nz := hn, reduced := hd }.num

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ ↑(padicNorm p { num := n, den := d, den_nz := hn, reduced := hd }) ≤ 1

Tactic:
norm_cast

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ padicNorm p { num := n, den := d, den_nz := hn, reduced := hd } ≤ 1

Proof state:
case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ 1 ≤ p ^ padicValInt p { num := n, den := d, den_nz := hn, reduced := hd }.num

Tactic:
apply one_le_pow

Result:
case ha.h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ 0 < p

Proof state:
case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ 1 ≤ ↑p ^ padicValInt p { num := n, den := d, den_nz := hn, reduced := hd }.num

Tactic:
norm_cast

Result:
case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ 1 ≤ p ^ padicValInt p { num := n, den := d, den_nz := hn, reduced := hd }.num

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ ‖↑{ num := n, den := d, den_nz := hn, reduced := hd }‖ ≤ 1

Tactic:
rw [padicNormE.eq_padicNorm]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ ↑(padicNorm p { num := n, den := d, den_nz := hn, reduced := hd }) ≤ 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ padicNorm p { num := n, den := d, den_nz := hn, reduced := hd } ≤ 1

Tactic:
rw [padicNorm.eq_zpow_of_nonzero hnz', padicValRat, neg_sub,
  padicValNat.eq_zero_of_not_dvd hq, Nat.cast_zero, zero_sub, zpow_neg, zpow_natCast]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ (↑p ^ padicValInt p { num := n, den := d, den_nz := hn, reduced := hd }.num)⁻¹ ≤ 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : n = 0
this : { num := n, den := d, den_nz := hn, reduced := hd } = 0
⊢ ‖↑{ num := n, den := d, den_nz := hn, reduced := hd }‖ ≤ 1

Tactic:
norm_num [this]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : n = 0
⊢ ‖↑{ num := n, den := d, den_nz := hn, reduced := hd }‖ ≤ 1

Tactic:
have : (⟨n, d, hn, hd⟩ : ℚ) = 0 := Rat.zero_iff_num_zero.mpr hnz

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : n = 0
this : { num := n, den := d, den_nz := hn, reduced := hd } = 0
⊢ ‖↑{ num := n, den := d, den_nz := hn, reduced := hd }‖ ≤ 1

Proof state:
case ha.h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd } ≠ 0
⊢ 0 < p

Tactic:
exact hp.1.pos

Result:
no goals