elegant way to unfold instances

Stream: general

[Ira Fesefeldt]

I find myself unfolding a lot of type classes when proving basic theorems about a new operation. Is there a more elegant way to do it? An example for what I mean looks like this:

import Mathlib

open unitInterval

noncomputable instance unitDiv : Div I :=
    ⟨fun i j => if h : i < j then ⟨i/j, sorry⟩ else 1⟩

example (i j : unitInterval) (h_lt : i < j) : ¬ i / j = 1 := by
  intro h_one
  rw [HDiv.hDiv, instHDiv, Div.div, unitDiv] at h_one -- more elegant for this one?
  simp only [dite_eq_ite, ite_eq_right_iff] at h_one
  sorry -- more clever proof

[Yaël Dillies]

Write lemma div_def (i j : I) : i / j = if h : i < j then ⟨i/j, sorry⟩ else 1 := rfl and, more specifically to that case, @[simp, norm_cast] lemma coe_div : ↑(i / j) = if h : i < j then (i / j : ℝ) else 1 := by rw [div_def]; split_ifs <;> rfl

[Kevin Buzzard]

Makes a nice change to have 1/0=1 :-)

[Ira Fesefeldt]

Thats the adjoint of * in the interval [0,1] :shrug: