Comment by lgas

I'm not an expert but I'd say based on my experience with Lean so far, the answer is yes. eg. I have entered some proofs from the Lean guide and then replaced tactics with `apply?` which searches for tactics to meet the goal, and eg. reduced this example from the guide:

    theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
      fun hpq : p ∧ q =>
      have hp : p := And.left hpq
      have hq : q := And.right hpq
      show q ∧ p from And.intro hq hp

To this:

    theorem and_commutative' (p q : Prop) : p ∧ q → q ∧ p := by
       exact fun a ↦ id (And.symm a)

Presumably the same thing could be done for each part of a more complicated proof and could be done so at each step automatically.