example : True := by dsimp? [trivial,]
example : True := by dsimp? only [trivial,]
example : True := by simp? [trivial,]
example : True := by simp? only [trivial,]
example : True := by simpa [trivial,]
example : True := by simpa only [trivial,]
example : True := by simpa [trivial,] using trivial
example : True := by simpa only [trivial,] using trivial