p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖{ val := k, property := property✝ }‖ = 1
hk : k ≠ 0
⊢ { val := k, property := property✝ } * inv { val := k, property := property✝ } = 1
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖{ val := k, property := property✝ }‖ = 1
⊢ { val := k, property := property✝ } * inv { val := k, property := property✝ } = 1
have hk : k ≠ 0 := fun h' => zero_ne_one' ℚ_[p] (by simp [h'] at h)
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖{ val := k, property := property✝ }‖ = 1
hk : k ≠ 0
⊢ ({ val := k, property := property✝ } *
      match { val := k, property := property✝ } with
      | { val := k, property := property } => if h : ‖k‖ = 1 then { val := k⁻¹, property := (_ : ‖k⁻¹‖ ≤ 1) } else 0) =
    1
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖{ val := k, property := property✝ }‖ = 1
hk : k ≠ 0
⊢ { val := k, property := property✝ } * inv { val := k, property := property✝ } = 1
unfold PadicInt.inv
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ ({ val := k, property := property✝ } *
      match { val := k, property := property✝ } with
      | { val := k, property := property } => if h : ‖k‖ = 1 then { val := k⁻¹, property := (_ : ‖k⁻¹‖ ≤ 1) } else 0) =
    1
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖{ val := k, property := property✝ }‖ = 1
hk : k ≠ 0
⊢ ({ val := k, property := property✝ } *
      match { val := k, property := property✝ } with
      | { val := k, property := property } => if h : ‖k‖ = 1 then { val := k⁻¹, property := (_ : ‖k⁻¹‖ ≤ 1) } else 0) =
    1
rw [norm_eq_padic_norm] at h
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ ({ val := k, property := property✝ } * if h : ‖k‖ = 1 then { val := k⁻¹, property := (_ : ‖k⁻¹‖ ≤ 1) } else 0) = 1
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ ({ val := k, property := property✝ } *
      match { val := k, property := property✝ } with
      | { val := k, property := property } => if h : ‖k‖ = 1 then { val := k⁻¹, property := (_ : ‖k⁻¹‖ ≤ 1) } else 0) =
    1
dsimp only
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ { val := k, property := property✝ } * { val := k⁻¹, property := (_ : ‖k⁻¹‖ ≤ 1) } = 1
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ ({ val := k, property := property✝ } * if h : ‖k‖ = 1 then { val := k⁻¹, property := (_ : ‖k⁻¹‖ ≤ 1) } else 0) = 1
rw [dif_pos h]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ ↑({ val := k, property := property✝ } * { val := k⁻¹, property := (_ : ‖k⁻¹‖ ≤ 1) }) = ↑1
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ { val := k, property := property✝ } * { val := k⁻¹, property := (_ : ‖k⁻¹‖ ≤ 1) } = 1
apply Subtype.ext_iff_val.2
no goals
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ ↑({ val := k, property := property✝ } * { val := k⁻¹, property := (_ : ‖k⁻¹‖ ≤ 1) }) = ↑1
simp [mul_inv_cancel hk]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖{ val := k, property := property✝ }‖ = 1
h' : k = 0
⊢ 0 = 1
simp [h'] at h