style: replace @f _ _ with f in example (leanprover#69)

* style: replace `@f _ _` with `f` in example

The `@` is necessary before `euclr` in this example, but nowhere else.
The current presentation may mislead readers about the effects of `{{ }}` by
making them think that it's necessary for `th1` and `th2`.

* fix: update text to match updated code

---------

Co-authored-by: David Thrane Christiansen <david@lean-fro.org>

interacting_with_lean.md

@@ -374,7 +374,7 @@ theorem th2 {α : Type u} {r : α → α → Prop}
 theorem th3 {α : Type u} {r : α → α → Prop}
             (reflr : reflexive r) (euclr : euclidean r)
             : transitive r :=
- @th2 _ _ (@th1 _ _ reflr @euclr) @euclr
+ th2 (th1 reflr @euclr) @euclr
 
 variable (r : α → α → Prop)
 variable (euclr : euclidean r)
@@ -386,9 +386,9 @@ The results are broken down into small steps: ``th1`` shows that a
 relation that is reflexive and euclidean is symmetric, and ``th2``
 shows that a relation that is symmetric and euclidean is
 transitive. Then ``th3`` combines the two results. But notice that we
-have to manually disable the implicit arguments in ``th1``, ``th2``,
-and ``euclr``, because otherwise too many implicit arguments are
-inserted. The problem goes away if we use weak implicit arguments:
+have to manually disable the implicit arguments in ``euclr``, because
+otherwise too many implicit arguments are inserted. The problem goes
+away if we use weak implicit arguments:
 
 ```lean
 def reflexive {α : Type u} (r : α → α → Prop) : Prop :=