Why I <3 tactics sometimes.

tactics.v

Theorem iso_comp_iso
        {C : Category}
        {a b c : @ob C}
        (f : Isomorphism a b)
        (g : Isomorphism b c) :
  Isomorphism a c.
Proof.
  destruct f, g.
  exists (comp to0 to1) (comp from1 from0).
  rewrite assoc.
  rewrite <- (assoc C from1).
  rewrite inv_left0.
  rewrite id_right.
  assumption.
  rewrite assoc.
  rewrite <- (assoc C to0).
  rewrite inv_right1.
  rewrite id_right.
  assumption.
Defined.


(* The above produces:

iso_comp_iso = 
fun (C : Category) (a b c : C) (f : Isomorphism a b) (g : Isomorphism b c)
=>
match f with
| {| to := to0; from := from0; inv_left := inv_left0; inv_right :=
  inv_right0 |} =>
    match g with
    | {| to := to1; from := from1; inv_left := inv_left1; inv_right :=
      inv_right1 |} =>
        {|
        to := comp to0 to1;
        from := comp from1 from0;
        inv_left := eq_ind_r (fun m : mor c c => m = id)
                      (eq_ind (comp from1 (comp from0 to0))
                         (fun m : mor c b => comp m to1 = id)
                         (eq_ind_r
                            (fun m : mor b b =>
                             comp (comp from1 m) to1 = id)
                            (eq_ind_r (fun m : mor c b => comp m to1 = id)
                               inv_left1 (id_right C c b from1)) inv_left0)
                         (comp (comp from1 from0) to0)
                         (assoc C from1 from0 to0))
                      (assoc C (comp from1 from0) to0 to1);
        inv_right := eq_ind_r (fun m : mor a a => m = id)
                       (eq_ind (comp to0 (comp to1 from1))
                          (fun m : mor a b => comp m from0 = id)
                          (eq_ind_r
                             (fun m : mor b b =>
                              comp (comp to0 m) from0 = id)
                             (eq_ind_r
                                (fun m : mor a b => comp m from0 = id)
                                inv_right0 (id_right C a b to0))
                             inv_right1) (comp (comp to0 to1) from1)
                          (assoc C to0 to1 from1))
                       (assoc C (comp to0 to1) from1 from0) |}
    end
end
     : forall (C : Category) (a b c : C),
       Isomorphism a b -> Isomorphism b c -> Isomorphism a c
*)