How to convert subtype and underlying type in Prop

Stream: general

[dannypsnl]

The final theorem in the below code contains the question, in such case, how to replace x with ↑x in Prop, vice versa?

def PReal := { r : Real // 0 < r } deriving
  One, CommMonoid
notation "ℝ>0" => PReal
instance : Add ℝ>0 where
  add x y := ⟨ x.val + y.val , by refine add_pos x.property y.property ⟩
instance : Mul ℝ>0 where
  mul x y := ⟨ x.val * y.val , by refine mul_pos x.property y.property ⟩
noncomputable instance : Div ℝ>0 where
  div x y := ⟨ x.val / y.val , by refine div_pos x.property y.property ⟩

theorem outside_cancel {x : ℝ>0} : (1 / x.val) * x.val = 1 := by
  have h : x.val ≠ 0 := Ne.symm (ne_of_lt x.property)
  exact one_div_mul_cancel h
theorem inside_cancel {x : ℝ>0} : (1 / x) * x = 1 := by
  have h : x.val ≠ 0 := Ne.symm (ne_of_lt x.property)
  have H := one_div_mul_cancel h
  sorry

[Ilmārs Cīrulis]

This worked when I tried it.

import Mathlib

def PReal := { r : Real // 0 < r } deriving
  One, CommMonoid

notation "ℝ>0" => PReal

instance : Add ℝ>0 where
  add x y := ⟨ x.val + y.val , by refine add_pos x.property y.property ⟩

instance : Mul ℝ>0 where
  mul x y := ⟨ x.val * y.val , by refine mul_pos x.property y.property ⟩

noncomputable instance : Div ℝ>0 where
  div x y := ⟨ x.val / y.val , by refine div_pos x.property y.property ⟩

theorem outside_cancel {x : ℝ>0} : (1 / x.val) * x.val = 1 := by
  have h : x.val ≠ 0 := Ne.symm (ne_of_lt x.property)
  exact one_div_mul_cancel h

theorem inside_cancel {x : ℝ>0} : (1 / x) * x = 1 := by
  have h : x.val ≠ 0 := Ne.symm (ne_of_lt x.property)
  have H := one_div_mul_cancel h
  reduce; congr

[Ilmārs Cīrulis]

But I doubt that's good solution... It's better to wait for someone more experienced to comment.

[Etienne Marion]

What I usually do is that I use injectivity of the coercion and then push the coercion inside the expression (using the tactic norm_cast which is your best friend in such cases when it works or lemmas if it doesn't) to get what I want. Here's what it gives in this case:

import Mathlib

def PReal := { r : Real // 0 < r } deriving
  One, CommMonoid
notation "ℝ>0" => PReal
instance : Add ℝ>0 where
  add x y := ⟨ x.val + y.val , by refine add_pos x.property y.property ⟩
instance : Mul ℝ>0 where
  mul x y := ⟨ x.val * y.val , by refine mul_pos x.property y.property ⟩
noncomputable instance : Div ℝ>0 where
  div x y := ⟨ x.val / y.val , by refine div_pos x.property y.property ⟩

theorem outside_cancel {x : ℝ>0} : (1 / x.val) * x.val = 1 := by
  have h : x.val ≠ 0 := Ne.symm (ne_of_lt x.property)
  exact one_div_mul_cancel h
theorem inside_cancel {x : ℝ>0} : (1 / x) * x = 1 := by
  have h : x.val ≠ 0 := Ne.symm (ne_of_lt x.property)
  have H := one_div_mul_cancel h
  rw [← Subtype.val_inj]
  norm_cast

[dannypsnl]

norm_cast is a lot faster, also thanks @Lessness