simplify bricks with function.injective

Stream: general

[Kenny Lau]

example (α β) (f : α → β) (H : function.injective f) : false :=
by simp [function.injective] at H

trace:

--------------
[simplify] iff: function.injective f
[simplify] eq: function.injective f
[simplify] eq: f
[simplify] eq: function.injective
109. [simplify.rewrite] [function.injective.equations._eqn_1]: function.injective f ==> ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
[simplify] eq: f a₁ = f a₂ → a₁ = a₂
[simplify] eq: f a₁ = f a₂
[simplify] eq: f a₁
[simplify] eq: a₁
[simplify] eq: f
[simplify] eq: f a₂
[simplify] eq: a₂
[simplify] eq: f
[simplify] eq: eq
111. [simplify.rewrite_failure] fail to match 'ite_eq_ff_distrib':
f a₁ = f a₂
=?=
ite ?x_0 ?x_2 ?x_3 = ff
--------------

ad nauseam