Simplify proof slightly

Changes

1 changed files (+1/-3)

• BinOp.lean
  • @@ -23,9 +23,7 @@ example {α} [Nonempty α] (f : α → α → α) (h : ∀ x y, ∃ z, f x z = y
    intro a b specialize h x (f x a) obtain ⟨a', ⟨h₂, h₃⟩⟩ := h - have h₄ : a' = a := by - apply h₃ a h₂ - rw [← h₄] + rw [← h₃ a h₂] exact h₃ b apply Function.leftInverse_invFun (h₁ x)