Don't need to rw definition before use

Changes

1 changed files (+0/-2)

• BinOp.lean
  • @@ -13,13 +13,11 @@ example {α} [Nonempty α] (f : α → α → α) (h : ∀ x y, ∃ z, f x z = y
    intro x y constructor have h₁ x : (f x).Surjective := by - rw [Function.Surjective] intro y specialize h x y grind apply Function.rightInverse_invFun (h₁ x) have h₁ x : (f x).Injective := by - rw [Function.Injective] intro a b specialize h x (f x a) obtain ⟨a', ⟨h₂, h₃⟩⟩ := h